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

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

FormulaImpl

protected FormulaImpl()

Initialize a new Formula. This constructor is made protected to hide it from the end user, but to keep it available for subclasses. Nothing needs to be initialized.

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

computeVariables

protected abstract Set<Variable> computeVariables()

Compute the set of variables in this formula.

Returns:

The set of variables, in the order of occurrence in the formula.

getFreeVariables

public Set<Variable> getFreeVariables()

Return the free variables in this formula. This method should be overridden for efficiency, but this class provides a correct implementation. TODO

Specified by:

getFreeVariables in interface Formula

See Also:

LinkedHashSet

getPredicates

public Set<Predicate> getPredicates()

Return all predicates that occur in this formula. TODO

Specified by:

getPredicates in interface Formula

computePredicates

protected abstract Set<Predicate> computePredicates()

Compute the set of predicates in this formula.

Returns:

The set of predicates, in the order of occurrence in the formula.

isClosed

public boolean isClosed()

Check whether this formula is closed.

Specified by:

isClosed 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