de.uni_tuebingen.sfb.lichtenstein.formulas
Class Negation

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.UnaryJunctor
              de.uni_tuebingen.sfb.lichtenstein.formulas.Negation

All Implemented Interfaces:

Formula, Visitable, Serializable

public class Negation
extends UnaryJunctor

A class representing logical negation of a formula.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

Negation(Formula negatedFormula)
Initialize a new negation, given the formula to be negated.

Method Summary

void	accept(FormulaVisitor visitor) Accept a formula visitor.
Formula	getNegatedFormula() Returns the negated formula.
Formula	getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
String	getSymbol() Return the textual representation of this unary junctor.
Formula	not() The negation of a negation is the formula itself.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.UnaryJunctor

containsVariable, equals, getArgument, getFirstIndexOf, getNbBoundVariables, getNbFreeVariables, getNbSubformulas, getNbVariables, getPredicates, 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, or

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

Negation

public Negation(Formula negatedFormula)

Initialize a new negation, given the formula to be negated.

Parameters:

negatedFormula - The formula to be negated.

Postcondition:

The negated formula is set to the given formula.

| new.getNegatedFormula() == negatedFormula

Method Detail

not

public Formula not()

The negation of a negation is the formula itself.

Specified by:

not in interface Formula

Overrides:

not in class FormulaImpl

Returns:

The argument formula.

getNegatedFormula

public Formula getNegatedFormula()

Returns the negated formula.

Returns:

The negated formula is the argument of the negation.

| result == getArgument()

getNormalForm

public Formula getNormalForm()

Get a normal form with only conjunction, disjunction, negation and existential quantification.

Returns:

The negation of the normal form of the argument or an equivalent logical formula.

| result ==
         getArgument().getNormalForm().not() TODO

getSymbol

public String getSymbol()

Return the textual representation of this unary junctor.

Specified by:

getSymbol in class ComposedFormula

Returns:

The unicode symbol NOT SIGN: ¬.

| 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.