

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 