de.uni_tuebingen.sfb.lichtenstein.formulas
Class Equivalence

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.BinaryJunctor
              de.uni_tuebingen.sfb.lichtenstein.formulas.Equivalence

All Implemented Interfaces:

Formula, Visitable, Serializable

public class Equivalence
extends BinaryJunctor

A class representing the equivalence in logical formulas. TODO: remove this class once the template system works. Then store it as a permanent template?

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

Equivalence(Formula first, Formula second)
Initialize a new equivalence between two formulas.

Method Summary

void	accept(FormulaVisitor visitor) Accept a formula visitor.
Conjunction	getEquivalentFormula() Returns a formula which is equivalent to this equivalence: (first -> second) & (second -> first).
Conjunction	getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
String	getSymbol() Return the textual representation of this binary junctor.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.BinaryJunctor

containsVariable, equals, getFirstArgument, getFirstIndexOf, getNbBoundVariables, getNbFreeVariables, getNbSubformulas, getNbVariables, getPredicates, getSecondArgument, getSubformulaAt, getVariableAt, hashCode, isFreeVariable, toString

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula

getAllSubformulas

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl

and, exists, exists, forAll, forAll, getFreeVariables, getVariables, iff, implies, isClosed, not, or

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

Equivalence

public Equivalence(Formula first,
                   Formula second)

Initialize a new equivalence between two formulas.

Parameters:

first - The first formula.

second - The second formula.

Postcondition:

The first argument is set to the given first argument.

| new.getFirstArgument() == first

Postcondition:

The second argument is set to the given second argument.

| new.getSecondArgument() == second

Method Detail

getEquivalentFormula

public Conjunction getEquivalentFormula()

Returns a formula which is equivalent to this equivalence: (first -> second) & (second -> first).

Returns:

The conjunction of the implications of the arguments in both directions.

| result.getFirstArgument() in
         Implication &&
| result.getSecondArgument() in Implication && |
         result.getFirstArgument().getFirstArgument() == getFirstArgument() &&
|
         result.getFirstArgument().getSecondArgument() == getSecondArgument() &&
|
         result.getSecondArgument().getFirstArgument() == getFirstArgument() &&
|
         result.getSecondArgument().getFirstArgument() == getSecondArgument()

getNormalForm

public Conjunction getNormalForm()

Get a normal form with only conjunction, disjunction, negation and existential quantification.

Returns:

The normal form of the equivalent formula

| result == getEquivalentFormula().getNormalForm()

getSymbol

public String getSymbol()

Return the textual representation of this binary junctor.

Specified by:

getSymbol in class ComposedFormula

Returns:

The unicode symbol LEFT RIGHT ARROW: ↔

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 composed formulas.

Specified by:

accept in interface Visitable

Overrides:

accept in class FormulaImpl

Parameters:

visitor - The visitor that is to be accepted to do its work.

Throws:

VisitorException

A visitor can throw an exception.