de.uni_tuebingen.sfb.lichtenstein.formulas
Class ComposedFormula

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

All Implemented Interfaces:

Formula, Visitable, Serializable

Direct Known Subclasses:

BinaryJunctor, FirstOrderQuantor, NaryJunctor, SecondOrderQuantor, UnaryJunctor

public abstract class ComposedFormula
extends FormulaImpl

A class representing a composed formula, i.e. a formula which consists of other formulas, connected by an operator.

Author:

Hendrik Maryns

See Also:

Serialized Form

Method Summary

List<Formula>	getAllSubformulas() Returns a list containing all subformulas of this formula.
abstract int	getNbSubformulas() Returns the number of subformulas of this formula.
abstract Formula	getSubformulaAt(int index) Returns the indexth subformula of this formula.
abstract String	getSymbol() Return the textual representation of this binary junctor.

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, getNbBoundVariables, getNbFreeVariables, getNbVariables, getNormalForm, getPredicates, getVariableAt, isFreeVariable

Method Detail

getAllSubformulas

public List<Formula> getAllSubformulas()

Returns a list containing all subformulas of this formula. That is, this formula and all the subformulas of its direct subformulas.

Returns:

Recursively generates all subformulas of this formula.

getNbSubformulas

public abstract int getNbSubformulas()

Returns the number of subformulas of this formula.

Returns:

The number of subformulas.

getSubformulaAt

public abstract Formula getSubformulaAt(int index)
                                 throws IndexOutOfBoundsException

Returns the indexth subformula of this formula.

Parameters:

index - The index of the wanted subformula. Indices start from 0.

Returns:

False if the index is bigger than or equal to the number of subformulas of this formula, or less than zero. (I.e. if the index is out of bounds, an error <em>must be thrown.)

| if ( index < 0 || index >=
         getNbSubformulas() )
| then false

Throws:

IndexOutOfBoundsException

The index is bigger than or equal to the number of subformulas of this formula, or less than zero

| index <
         0
|| index >= getNbSubformulas()

getSymbol

public abstract String getSymbol()

Return the textual representation of this binary junctor. This consists of a symbol traditionally used for representing this junctor.