|
||||||||||
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.
Constructor Summary | |
---|---|
protected |
FormulaImpl()
Initialize a new Formula. |
Method Summary | |
---|---|
Conjunction |
and(Formula that)
Return the conjunction of this formula with that formula. |
protected abstract Set<Predicate> |
computePredicates()
Compute the set of predicates in this formula. |
protected abstract Set<Variable> |
computeVariables()
Compute the set of variables in this 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<Predicate> |
getPredicates()
Return all predicates that occur 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 |
---|
clone, finalize, getClass, notify, notifyAll, wait, wait, wait |
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula |
---|
containsVariable, getNormalForm, isFree |
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable |
---|
accept |
Constructor Detail |
---|
protected FormulaImpl()
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
protected abstract Set<Variable> computeVariables()
public Set<Variable> getFreeVariables()
getFreeVariables
in interface Formula
LinkedHashSet
public Set<Predicate> getPredicates()
getPredicates
in interface Formula
protected abstract Set<Predicate> computePredicates()
public boolean isClosed()
isClosed
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
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
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |