|
|||||||||
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
public abstract class FormulaImpl
A class providing implementations of the formula interface where possible. TODO: make iterators.
Method Summary | |
---|---|
void |
accept(FormulaVisitor visitor)
Accept a formula visitor. |
Conjunction |
and(Formula that)
Return the conjunction of this formula with that formula. |
boolean |
equals(Object other)
Indicates whether some other object is "equal to" this one. |
FirstOrderExistentialQuantification |
exists(FirstOrderVariable var)
Return the existential quantification of this formula over the given first order variable. |
SecondOrderExistentialQuantification |
exists(SecondOrderVariable var)
Return the existential quantification of this formula over the given first order variable. |
FirstOrderUniversalQuantification |
forAll(FirstOrderVariable var)
Return the universal quantification of this formula over the given variable. |
SecondOrderUniversalQuantification |
forAll(SecondOrderVariable var)
Return the universal quantification of this formula over the given variable. |
Set<Variable> |
getFreeVariables()
Return the free variables in this formula. |
Set<Variable> |
getVariables()
Return the variables in this formula. |
abstract int |
hashCode()
Returns a hash code value for the object. |
Equivalence |
iff(Formula that)
Return the equivalence of this formula with that formula. |
Implication |
implies(Formula that)
Return the implication of this formula with that formula. |
boolean |
isClosed()
Check whether this formula is closed. |
Formula |
not()
Return the negation of this formula. |
Disjunction |
or(Formula that)
Return the disjunction of this formula with that formula. |
abstract String |
toString()
Returns a string representation of the object. |
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, getNbBoundVariables, getNbFreeVariables, getNbVariables, getNormalForm, getPredicates, getVariableAt, isFreeVariable |
Method Detail |
---|
public Formula not()
not
in interface Formula
public Conjunction and(Formula that)
and
in interface Formula
that
- The other formula. That is a mnemonic for this.and(that)
.public Disjunction or(Formula that)
or
in interface Formula
that
- The other formula. That is a mnemonic for this.or(that)
.public Implication implies(Formula that)
implies
in interface Formula
that
- The other formula. That is a mnemonic for this.implies(that)
.public Equivalence iff(Formula that)
iff
in interface Formula
that
- The other formula. That is a mnemonic for this.iff(that)
.public FirstOrderUniversalQuantification forAll(FirstOrderVariable var)
forAll
in interface Formula
var
- The variable which is to be quantified.public SecondOrderUniversalQuantification forAll(SecondOrderVariable var)
forAll
in interface Formula
var
- The variable which is to be quantified.public FirstOrderExistentialQuantification exists(FirstOrderVariable var)
exists
in interface Formula
var
- The variable which is to be quantified.public SecondOrderExistentialQuantification exists(SecondOrderVariable var)
exists
in interface Formula
var
- The variable which is to be quantified.public Set<Variable> getVariables()
getVariables
in interface Formula
LinkedHashSet
public boolean isClosed()
isClosed
in interface Formula
public Set<Variable> getFreeVariables()
getFreeVariables
in interface Formula
public boolean equals(Object other)
The equals method of Object should be overriden, as only the semantics of a formula count. Two formulas are the same if each of its subformulas is of the same class, and they act on the same variables.
equals
in class Object
|
if ( other.getClass() != this.getClass() )
| then result == false
public abstract int hashCode()
This method should be overridden along with equals
. For the reason, see Object.hashCode()
.
hashCode
in class Object
public abstract String toString()
formulas have a traditional string representation. No elimination of unnecessary parentheses is performed.
toString
in class Object
public void accept(FormulaVisitor visitor) throws de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException
accept
in interface Visitable
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 |