de.uni_tuebingen.sfb.lichtenstein.formulas
Class FormulaImpl

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
All Implemented Interfaces:
Formula, Visitable, Serializable
Direct Known Subclasses:
AtomicFormula, ComposedFormula

public abstract class FormulaImpl
extends Object
implements Formula, Serializable

A class providing implementations of the formula interface where possible. TODO: make iterators.

Author:
Hendrik Maryns
See Also:
Serialized Form

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

not

public Formula not()
Return the negation of this formula.

Specified by:
not in interface Formula

and

public Conjunction and(Formula that)
Return the conjunction of this formula with that formula.

Specified by:
and in interface Formula
Parameters:
that - The other formula. That is a mnemonic for this.and(that).

or

public Disjunction or(Formula that)
Return the disjunction of this formula with that formula.

Specified by:
or in interface Formula
Parameters:
that - The other formula. That is a mnemonic for this.or(that).

implies

public Implication implies(Formula that)
Return the implication of this formula with that formula.

Specified by:
implies in interface Formula
Parameters:
that - The other formula. That is a mnemonic for this.implies(that).

iff

public Equivalence iff(Formula that)
Return the equivalence of this formula with that formula.

Specified by:
iff in interface Formula
Parameters:
that - The other formula. That is a mnemonic for this.iff(that).

forAll

public FirstOrderUniversalQuantification forAll(FirstOrderVariable var)
Return the universal quantification of this formula over the given variable.

Specified by:
forAll in interface Formula
Parameters:
var - The variable which is to be quantified.

forAll

public SecondOrderUniversalQuantification forAll(SecondOrderVariable var)
Return the universal quantification of this formula over the given variable.

Specified by:
forAll in interface Formula
Parameters:
var - The variable which is to be quantified.

exists

public FirstOrderExistentialQuantification exists(FirstOrderVariable var)
Return the existential quantification of this formula over the given first order variable.

Specified by:
exists in interface Formula
Parameters:
var - The variable which is to be quantified.

exists

public SecondOrderExistentialQuantification exists(SecondOrderVariable var)
Return the existential quantification of this formula over the given first order variable.

Specified by:
exists in interface Formula
Parameters:
var - The variable which is to be quantified.

getVariables

public Set<Variable> getVariables()
Return the variables in this formula. They are guaranteed to be returned by the iterator in the same order as they appear in the formula.

Specified by:
getVariables in interface Formula
See Also:
LinkedHashSet

isClosed

public boolean isClosed()
Check whether this formula is closed.

Specified by:
isClosed in interface Formula

getFreeVariables

public Set<Variable> getFreeVariables()
Return the free variables in this formula.

Specified by:
getFreeVariables in interface Formula

equals

public boolean equals(Object other)
Indicates whether some other object is "equal to" this one.

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.

Overrides:
equals in class Object
Returns:
The classes are compared in this preliminary implementation. This should be overridden by subclasses.
| if ( other.getClass() != this.getClass() ) | then result == false

hashCode

public abstract int hashCode()
Returns a hash code value for the object.

This method should be overridden along with equals. For the reason, see Object.hashCode().

Overrides:
hashCode in class Object

toString

public abstract String toString()
Returns a string representation of the object.

formulas have a traditional string representation. No elimination of unnecessary parentheses is performed.

Overrides:
toString in class Object

accept

public void accept(FormulaVisitor visitor)
            throws de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException
Accept a formula visitor. The iteration is done by the visitor, not by the formula.

Specified by:
accept in interface Visitable
Parameters:
visitor - The visitor that is to be accepted to do its work.