de.uni_tuebingen.sfb.lichtenstein.formulas
Class Conjunction
java.lang.Object
de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
de.uni_tuebingen.sfb.lichtenstein.formulas.NaryJunctor
de.uni_tuebingen.sfb.lichtenstein.formulas.Conjunction
- All Implemented Interfaces:
- Formula, Visitable, Serializable
public final 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. |
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.NaryJunctor |
computePredicates, computeVariables, containsVariable, getArgument, getNbArguments, getNbSubformulas, getSubformulaAt, hasAsArgument, hashCode, isFree, toString |
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl |
and, equals, exists, exists, forAll, forAll, getFreeVariables, getPredicates, getVariables, iff, implies, isClosed, not, or |
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]
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 VisitorException
- Accept a formula visitor. The iteration is done by the visitor, not by the composed formulas.
- Parameters:
visitor
- The visitor that is to be accepted to do its work.
- Throws:
VisitorException
- [CAN]
A visitor can throw an exception.
© Copyright 2008 Hendrik Maryns