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, Inclusion, Precedence, ProperDominance, SecondOrderEquality, Subset

public abstract class AtomicFormula
extends FormulaImpl

A class representing an atomic formula.

Author:

Hendrik Maryns

See Also:

Serialized Form

Method Summary

int	getNbBoundVariables() Returns the number of bound variables in this formula.
int	getNbFreeVariables() Returns the number of free variables in this formula.
AtomicFormula	getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
boolean	isFreeVariable(Variable variable) Check whether the given variable is free in this formula.

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

accept, and, equals, exists, exists, forAll, forAll, getFreeVariables, getVariables, hashCode, iff, implies, isClosed, not, or, toString

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

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

containsVariable, getFirstIndexOf, getNbVariables, getPredicates, getVariableAt

Method Detail

getNbFreeVariables

public final int getNbFreeVariables()

Returns the number of free variables in this formula.

Returns:

All variables in an atomic formula are free.

| result == getNbVariables()

getNbBoundVariables

public final int getNbBoundVariables()

Returns the number of bound variables in this formula.

Returns:

An atomic formula does not have bound variables.

| result == 0

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

isFreeVariable

public boolean isFreeVariable(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