de.uni_tuebingen.sfb.lichtenstein.formulas
Class NaryJunctor

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      extended by de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          extended by 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

Method Summary
 boolean containsVariable(Variable var)
          Returns whether this formula contains the given variable.
 Formula getArgument(int index)
          Get the indexth argument.
 int getFirstIndexOf(Variable var)
          Get the first index at which the given variable occurs.
 int getNbArguments()
          Return the number of arguments.
 int getNbBoundVariables()
          Returns the number of bound variables in this formula.
 int getNbFreeVariables()
          Returns the number of free variables in this formula.
 int getNbSubformulas()
          Returns the number of subformulas of this formula.
 int getNbVariables()
          Returns the number of variables in this formula.
 Set<Predicate> getPredicates()
          Return all predicates that occur in this formula.
 Formula getSubformulaAt(int index)
          Returns the indexth subformula of this formula.
 Variable getVariableAt(int index)
          Get the indexth variable.
 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 isFreeVariable(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
accept, and, equals, exists, exists, forAll, forAll, getFreeVariables, getVariables, iff, implies, isClosed, not, or
 
Methods inherited from class java.lang.Object
getClass, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula
getNormalForm
 

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
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.

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.

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

getFirstIndexOf

public int getFirstIndexOf(Variable var)
Get the first index at which the given variable occurs.

Parameters:
var - The variable of which the index is wanted.

getNbBoundVariables

public int getNbBoundVariables()
Returns the number of bound variables in this formula.

Returns:
The sum of the number of bound variables of the arguments.
| result == Sum{getArgument(i).getNbBoundVariables() |for each i in 0..getNbArguments()}

getNbFreeVariables

public int getNbFreeVariables()
Returns the number of free variables in this formula.

Returns:
The sum of the number of free variables of the arguments.
| result == Sum{getArgument(i).getNbFreeVariables() |for each i in 0..getNbArguments()}

getNbVariables

public int getNbVariables()
Returns the number of variables in this formula.

Returns:
The sum of the number of variables of the arguments.
| result == Sum{getArgument(i).getNbVariables()|for each i in 0..getNbArguments()}

getPredicates

public Set<Predicate> getPredicates()
Return all predicates that occur in this formula. TODO


getVariableAt

public Variable getVariableAt(int index)
                       throws IndexOutOfBoundsException
Get the indexth variable.

Parameters:
index - The index of the wanted variable

isFreeVariable

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

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