|
|||||||||
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 |
---|
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public FormulaTemplate(Formula template, Variable... dummies) throws de.uni_tuebingen.sfb.lichtenstein.exceptions.FunctionArgumentsMismatchException
template
- The formula which is to serve as a template.dummies
- The variables in the formula which are dummy variables.| new.getTemplateFormula() == template
| new.getNbDummies() ==
dummies.length
| for 0 <= i <
dummies.length
| dummies[i].getClass() == new.getDummyClass(i)
| for one 0 <= i < dummies.length | !
template.contains(dummies[i])
Method Detail |
---|
public Formula getTemplateFormula()
public Formula getFormula(Variable... inputVariables) throws de.uni_tuebingen.sfb.lichtenstein.exceptions.FunctionArgumentsMismatchException
inputVariables
- The variables that should be used instead of the dummy variables.
|
inputVariables.length != getNbDummies()
| 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.
| index < 0 || index >=
getNbDummies()
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |