de.uni_tuebingen.sfb.lichtenstein.formulas
Class Equivalence

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      extended by de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          extended by de.uni_tuebingen.sfb.lichtenstein.formulas.BinaryJunctor
              extended by 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.