|
|||||||||
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.FormulaImpl de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula
public abstract class AtomicFormula
A class representing an atomic formula.
Method Summary | |
---|---|
int |
getNbBoundVariables()
Returns the number of bound variables in this formula. |
int |
getNbFreeVariables()
Returns the number of free variables in this formula. |
AtomicFormula |
getNormalForm()
Get a normal form with only conjunction, disjunction, negation and existential quantification. |
boolean |
isFreeVariable(Variable variable)
Check whether the given variable is free in this formula. |
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl |
---|
accept, and, equals, exists, exists, forAll, forAll, getFreeVariables, getVariables, hashCode, iff, implies, isClosed, not, or, toString |
Methods inherited from class java.lang.Object |
---|
getClass, notify, notifyAll, wait, wait, wait |
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula |
---|
containsVariable, getFirstIndexOf, getNbVariables, getPredicates, getVariableAt |
Method Detail |
---|
public final int getNbFreeVariables()
| result == getNbVariables()
public final int getNbBoundVariables()
| result == 0
public AtomicFormula getNormalForm()
| result == this
public boolean isFreeVariable(Variable variable)
variable
- The variable to check.| result == true
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |