de.uni_tuebingen.sfb.lichtenstein.formulas
Class FormulaImpl

java.lang.Object
  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.