de.uni_tuebingen.sfb.lichtenstein.formulas
Class Conjunction

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.NaryJunctor
              extended by de.uni_tuebingen.sfb.lichtenstein.formulas.Conjunction
All Implemented Interfaces:
Formula, Visitable, Serializable

public class Conjunction
extends NaryJunctor

A class representing the conjunction of formulas.

Author:
Hendrik Maryns
See Also:
Serialized Form

Constructor Summary
Conjunction(Formula... arguments)
          Initialize a new conjunction, taking formulas as conjuncts.
 
Method Summary
 void accept(FormulaVisitor visitor)
          Accept a formula visitor.
 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.NaryJunctor
containsVariable, getArgument, getFirstIndexOf, getNbArguments, getNbBoundVariables, getNbFreeVariables, getNbSubformulas, getNbVariables, getPredicates, getSubformulaAt, getVariableAt, hasAsArgument, 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, equals, 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

Conjunction

public Conjunction(Formula... arguments)
Initialize a new conjunction, taking formulas as conjuncts.

Parameters:
arguments - The conjuncts.
Postcondition:
The list of conjuncts is set to the given arguments.
| new.getNbArguments() == arguments.length | for each i in 0..new.getNbArguments() | getArgument(i) == argument[i]
Method Detail

getNormalForm

public Conjunction getNormalForm()
Get a normal form with only conjunction, disjunction, negation and existential quantification.

Returns:
The conjunction of the normal form of the conjuncts.
| TODO

getSymbol

public String getSymbol()
Return the textual representation of this binary junctor.

Specified by:
getSymbol in class ComposedFormula
Returns:
The unicode symbol LOGICAL AND: ∧.
| result == "∧"

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.