|
|||||||||
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 de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderEquality
public class SecondOrderEquality
A class representing the atomic formula that says two variables are equal.
Constructor Summary | |
---|---|
SecondOrderEquality(SetDenotator first,
SetDenotator second)
Initialize a new equality, involving two set denotators. |
Method Summary | |
---|---|
void |
accept(FormulaVisitor visitor)
Accept a formula visitor. |
boolean |
containsVariable(Variable var)
Returns whether this formula contains the given variable. |
boolean |
equals(Object other)
Indicates whether some other object is "equal to" this one. |
int |
getFirstIndexOf(Variable var)
Get the first index at which the given variable occurs. |
SetDenotator |
getFirstVariable()
Returns the first variable. |
int |
getNbVariables()
Returns the number of variables in this formula. |
Set<Predicate> |
getPredicates()
Return all predicates in this formula. |
SetDenotator |
getSecondVariable()
Returns the second variable. |
Variable |
getVariableAt(int index)
Get the indexth variable (free or bound). |
int |
hashCode()
Returns a hash code value for the object. |
String |
toString()
Returns a string representation of the object. |
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula |
---|
getNbBoundVariables, getNbFreeVariables, getNormalForm, isFreeVariable |
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl |
---|
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 |
Constructor Detail |
---|
public SecondOrderEquality(SetDenotator first, SetDenotator second)
first
- The first variable.second
- The second variable.| first != null && second != null
| new.getFirstVariable() == first
| new.getSecondVariable() == second
Method Detail |
---|
public SetDenotator getFirstVariable()
| result == getVariableAt(0)
public SetDenotator getSecondVariable()
| result == getVariableAt(0)
public int getNbVariables()
| result == 2
public int getFirstIndexOf(Variable var)
var
- The variable of which the index is wanted.public Variable getVariableAt(int index) throws IndexOutOfBoundsException
index
- The index of the wanted variablepublic boolean containsVariable(Variable var)
var
- The variable to check.public Set<Predicate> getPredicates()
| if ( getFirstVariable() instanceof Predicate ) | then
result.contains(getFirstVariable())
| if ( getSecondVariable() instanceof Predicate ) | then
result.contains(getSecondVariable())
public boolean equals(Object other)
equals
in class FormulaImpl
| let otherEquals = (SecondOrderEquality)
other in
| if ( otherEquals.getFirstVariable() != getFirstVariable() ) | then result == false | else if (
otherEquals.getSecondVariable() != getSecondVariable() )
| then result == false | else result == true
public int hashCode()
hashCode
in class FormulaImpl
| result ==
getFirstVariable().hashCode() + "=".hashCode() + getSecondVariable().hashCode()
public String toString()
toString
in class FormulaImpl
| result ==
getFirstVariable().toString() + "=" + getSecondVariable().toString()
public void accept(FormulaVisitor visitor) throws de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException
accept
in interface Visitable
accept
in class FormulaImpl
visitor
- The visitor that is to be accepted to do its work.
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |