de.uni_tuebingen.sfb.lichtenstein.formulas
Class Disjunction

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.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.
 
Method Summary
 void accept(FormulaVisitor visitor)
          Accept a formula visitor.
 Disjunction 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
computePredicates, computeVariables, containsVariable, getArgument, getNbArguments, getNbSubformulas, getSubformulaAt, hasAsArgument, hashCode, isFree, 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, getPredicates, getVariables, iff, implies, isClosed, not, or
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Constructor Detail

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]
Method Detail

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   Creative Commons License