|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaTemplate
public class FormulaTemplate
A class that represents a template for a formula, in which certain free variables still have to be filled in to get a real formula.
This is some sort of formula builder. It works with an internal visitor. TODO: check for bound variables in constructor, in replacer, in ...?
Constructor Summary | |
---|---|
FormulaTemplate(Formula template,
Variable... dummies)
Initialize a new formula template, based on a formula and a list of dummy variables that appear in the formula. |
Method Summary | |
---|---|
Class<? extends Variable> |
getDummyClass(int index)
Returns the class of the indexth dummy variable. |
Formula |
getFormula(Variable... inputVariables)
Return the formula that results from replacing the free variables which were supplied during the creation of this template by the variables supplied as arguments to this method. |
int |
getNbDummies()
Returns the number of variables that has to be supplied to this template to create a formula. |
Formula |
getTemplateFormula()
Return the formula that serves as a template. |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public FormulaTemplate(Formula template, Variable... dummies) throws FunctionArgumentsMismatchException
template
- The formula which is to serve as a template.dummies
- The variables in the formula which are dummy variables.FunctionArgumentsMismatchException
- [CAN]
If the formula does not contain any of the given dummy variables. | for one 0 <= i < dummies.length | !
template.contains(dummies[i])Method Detail |
---|
public Formula getTemplateFormula()
public Formula getFormula(Variable... inputVariables) throws FunctionArgumentsMismatchException
inputVariables
- The variables that should be used instead of the dummy variables.FunctionArgumentsMismatchException
- [CAN]
If the number of supplied variables is not the same as the number of dummy variables. |
inputVariables.length != getNbDummies()
FunctionArgumentsMismatchException
- [CAN]
If the type of the supplied variables does not correspond to their respective dummy variable. | for one 0 <=
i < inputVariables.length | inputVariables[i].getClass() != getDummyClass(i)public int getNbDummies()
public Class<? extends Variable> getDummyClass(int index) throws ArrayIndexOutOfBoundsException
index
- The index of the dummy for which the class is wanted. Indices start from zero.ArrayIndexOutOfBoundsException
- [CAN]
If the index is bigger than or equal to the number of dummies or smaller than zero. | index < 0 || index >=
getNbDummies()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |