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

Constructor Summary

protected

ComposedFormula() Initialize a new composed formula.

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

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, getNormalForm, isFree

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

accept

Constructor Detail

ComposedFormula

protected ComposedFormula()

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

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 must be thrown.) | if ( index < 0 || index >= getNbSubformulas() ) | then false

Throws:

IndexOutOfBoundsException - [CAN] 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.

Returns:

A symbol traditionally used for representing this junctor.