de.uni_tuebingen.sfb.lichtenstein.formulas
Class AtomicFormula

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula

All Implemented Interfaces:

Formula, Visitable, Serializable

Direct Known Subclasses:

Dominance, FirstOrderEquality, ImmediateDominance, ImmediatePrecedence, Inclusion, Precedence, ProperDominance, SecondOrderEquality, Subset

public abstract class AtomicFormula
extends FormulaImpl

A class representing an atomic formula.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

protected

AtomicFormula() Initialize a new atomic formula.

Method Summary

AtomicFormula	getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
boolean	isFree(Variable variable) Check whether the given variable is free in this formula.

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

and, computePredicates, computeVariables, equals, exists, exists, forAll, forAll, getFreeVariables, getPredicates, getVariables, hashCode, iff, implies, isClosed, not, or, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula

containsVariable

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable

accept

Constructor Detail

AtomicFormula

protected AtomicFormula()

Initialize a new atomic formula. Nothing needs to be initialized.

Method Detail

getNormalForm

public AtomicFormula getNormalForm()

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

Returns:

An atomic formula already is in disjunctive normal form. | result == this

isFree

public boolean isFree(Variable variable)

Check whether the given variable is free in this formula.

Parameters:

variable - The variable to check.

Returns:

Variables in atomic formulas are always free. | result == true