|
|||||||||
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.ComposedFormula de.uni_tuebingen.sfb.lichtenstein.formulas.FirstOrderQuantor
public abstract class FirstOrderQuantor
A class for representing quantors on first order variables, implementing common methods for existential and universal quantors.
Method Summary | |
---|---|
boolean |
containsVariable(Variable var)
Returns whether this formula contains the given variable. |
boolean |
equals(Object other)
An object is equal to a quantor if it has the same class (i.e., not only it is a quantor, but it really has the same leaf-level class), the arguments are equal and they bind the same variable. |
Formula |
getArgument()
Returns the formula this quantor acts on. |
FirstOrderVariable |
getBoundVariable()
Returns the variable that is bound by this quantor. |
int |
getFirstIndexOf(Variable var)
Get the first index at which the given variable occurs. |
int |
getNbBoundVariables()
Returns the number of bound variables in this formula. |
int |
getNbFreeVariables()
Returns the number of free variables in this formula. |
int |
getNbSubformulas()
Returns the number of subformulas of this formula. |
int |
getNbVariables()
Returns the number of variables in this formula. |
Set<Predicate> |
getPredicates()
Return all predicates that occur in this formula. |
Formula |
getSubformulaAt(int index)
Returns the indexth subformula of this formula. |
Variable |
getVariableAt(int index)
Get the indexth variable. |
int |
hashCode()
Returns a hash code value for the object. |
boolean |
isFreeVariable(Variable variable)
Check whether the given variable is free in this formula. |
String |
toString()
Returns a string representation of the object. |
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula |
---|
getAllSubformulas, getSymbol |
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl |
---|
accept, and, exists, exists, forAll, forAll, getFreeVariables, getVariables, iff, implies, isClosed, not, or |
Methods inherited from class java.lang.Object |
---|
getClass, notify, notifyAll, wait, wait, wait |
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula |
---|
and, exists, exists, forAll, forAll, getFreeVariables, getNormalForm, getVariables, iff, implies, isClosed, not, or |
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable |
---|
accept |
Method Detail |
---|
public FirstOrderVariable getBoundVariable()
getBoundVariable
in interface Quantification
public Formula getArgument()
getArgument
in interface Quantification
public int getNbVariables()
getNbVariables
in interface Formula
public int getNbFreeVariables()
getNbFreeVariables
in interface Formula
public int getNbBoundVariables()
getNbBoundVariables
in interface Formula
public int getFirstIndexOf(Variable var)
getFirstIndexOf
in interface Formula
var
- The variable of which the index is wanted.public Variable getVariableAt(int index) throws IndexOutOfBoundsException
getVariableAt
in interface Formula
index
- The index of the wanted variablepublic boolean containsVariable(Variable var)
containsVariable
in interface Formula
var
- The variable to check.public boolean isFreeVariable(Variable variable)
isFreeVariable
in interface Formula
variable
- The variable to check.public Set<Predicate> getPredicates()
getPredicates
in interface Formula
public int getNbSubformulas()
getNbSubformulas
in class ComposedFormula
public Formula getSubformulaAt(int index) throws IndexOutOfBoundsException
getSubformulaAt
in class ComposedFormula
index
- The index of the wanted subformula. Indices start from 0.public boolean equals(Object other)
equals
in class FormulaImpl
| let otherQuantor = (Quantor) other in | if ( !
getArgument().equals(otherQuantor.getArgument()) )
| then result == false
| let otherQuantor = (Quantor) other in | if ( ! getBoundVariable() ==
otherQuantor.getBoundVariable()) )
| then result == false
public int hashCode()
hashCode
in class FormulaImpl
| result ==
getSymbol().hashCode() + getBoundVariable().hashCode() + getArgument().hashCode()
public String toString()
toString
in class FormulaImpl
| result == "(" + getSymbol() + getBoundVariable().toString() + ")(" +
getArgument().toString() + ")"
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |