de.uni_tuebingen.sfb.lichtenstein.formulas
Class NaryJunctor

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

All Implemented Interfaces:

Formula, Visitable, Serializable

Direct Known Subclasses:

Conjunction, Disjunction

public abstract class NaryJunctor
extends ComposedFormula

A superclass for conjunction and disjunction, implementing common methods for binary junctors.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

protected

NaryJunctor(Formula... arguments) Initialize a new n-ary junctor, taking an unlimited number of formulas as arguments.

Method Summary

protected Set<Predicate>	computePredicates() Compute the set of predicates in this formula.
protected Set<Variable>	computeVariables() Compute the set of variables in this formula.
boolean	containsVariable(Variable var) Returns whether this formula contains the given variable.
Formula	getArgument(int index) Get the indexth argument.
int	getNbArguments() Return the number of arguments.
int	getNbSubformulas() Returns the number of subformulas of this formula.
Formula	getSubformulaAt(int index) Returns the indexth subformula of this formula.
boolean	hasAsArgument(Formula form) Returns whether this n-ary junctor has the given formula as an argument.
int	hashCode() Returns a hash code value for the object.
boolean	isFree(Variable variable) Check whether the given variable is free in this formula.
String	toString() Returns a string representation of the object.

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

getAllSubformulas, getSymbol

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

and, equals, exists, exists, forAll, forAll, getFreeVariables, getPredicates, getVariables, iff, implies, isClosed, not, or

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

getNormalForm

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

accept

Constructor Detail

NaryJunctor

protected NaryJunctor(Formula... arguments)

Initialize a new n-ary junctor, taking an unlimited number of formulas as arguments.

Parameters:

arguments - The arguments to this n-ary junctor.

Postcondition:

The list of arguments is set to the given arguments. | new.getNbArguments() == arguments.length | for each i in 0..new.getNbArguments() | getArgument(i) == argument[i]

Method Detail

getNbArguments

public int getNbArguments()

Return the number of arguments.

Returns:

The number of arguments. This is the same as the number of subformulas. | result == getNbSubformulas()

getArgument

public Formula getArgument(int index)
                    throws IndexOutOfBoundsException

Get the indexth argument.

Parameters:

index - The index of the argument wanted.

Returns:

The indexth argument. | getSubformulaAt(index)

Throws:

IndexOutOfBoundsException - [CAN] If the index is less than zero or more than the number of outgoing edges. | index < 0 || index >= getNbArguments()

hasAsArgument

public boolean hasAsArgument(Formula form)

Returns whether this n-ary junctor has the given formula as an argument.

Parameters:

form - The formula which has to be checked.

Returns:

Whether the formula is an argument.

computeVariables

protected Set<Variable> computeVariables()

Compute the set of variables in this formula.

Specified by:

computeVariables in class FormulaImpl

containsVariable

public boolean containsVariable(Variable var)

Returns whether this formula contains the given variable.

Parameters:

var - The variable to check.

Returns:

True if any of the arguments contains the given variable, false otherwise. | if ( for one i in 0..getNbArguments(): getArgument(i).containsVariable(var) ) | then result == true | else result == false

isFree

public boolean isFree(Variable variable)

Check whether the given variable is free in this formula.

Parameters:

variable - The variable to check.

Returns:

True if it is free in either argument. | result == for one i in 0..getNbArguments(): getArgument(i).isFreeVariable(variable)

computePredicates

protected Set<Predicate> computePredicates()

Compute the set of predicates in this formula.

Specified by:

computePredicates in class FormulaImpl

getNbSubformulas

public int getNbSubformulas()

Returns the number of subformulas of this formula.

Specified by:

getNbSubformulas in class ComposedFormula

getSubformulaAt

public Formula getSubformulaAt(int index)
                        throws IndexOutOfBoundsException

Returns the indexth subformula of this formula.

Specified by:

getSubformulaAt in class ComposedFormula

Parameters:

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

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()

hashCode

public int hashCode()

Returns a hash code value for the object.

This method should be overridden along with equals. For the reason, see Object.hashCode().

Specified by:

hashCode in class FormulaImpl

Returns:

The hash code is based on the hash codes of the arguments and of the characteristic symbol.

toString

public String toString()

Returns a string representation of the object.

formulas have a traditional string representation. No elimination of unnecessary parentheses is performed.

Specified by:

toString in class FormulaImpl

Returns:

The string representation of an n-ary junctor is the string representation of its arguments with an appropriate sign in between. | for each i in 0..getNbArguments(): result.contains(getArgument(i).toString()) | result.contains(getSymbol())