de.uni_tuebingen.sfb.lichtenstein.formulas
Class Disjunction
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.Disjunction
- All Implemented Interfaces:
- Formula, Visitable, Serializable
public final class Disjunction
- extends NaryJunctor
A class representing the disjunction of formulas.
- Author:
- Hendrik Maryns
- See Also:
- Serialized Form
Constructor Summary |
Disjunction(Formula... arguments)
Initialize a new disjunction, taking formulas as disjuncts. |
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 |
Disjunction
public Disjunction(Formula... arguments)
- Initialize a new disjunction, taking formulas as disjuncts.
- Parameters:
arguments
- The disjuncts.- Postcondition:
- The list of disjuncts is set to the given arguments. | new.getNbArguments() == arguments.length | for each
i in 0..new.getNbArguments() | getArgument(i) == argument[i]
getNormalForm
public Disjunction getNormalForm()
- Get a normal form with only conjunction, disjunction, negation and existential quantification.
- Returns:
- The disjunction of the normal form of the disjuncts. | TODO
getSymbol
public String getSymbol()
- Return the textual representation of this binary junctor.
- Specified by:
getSymbol
in class ComposedFormula
- Returns:
- The unicode symbol LOGICAL OR: ∨ | result == "∨"
accept
public void accept(FormulaVisitor visitor)
throws VisitorException
- Accept a formula visitor. The iteration is done by the visitor, not by the formula.
- 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