de.uni_tuebingen.sfb.lichtenstein.formulas
Class UnaryJunctor

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.UnaryJunctor
All Implemented Interfaces:
Formula, Visitable, Serializable
Direct Known Subclasses:
Negation

public abstract class UnaryJunctor
extends ComposedFormula

A class representing a unary junctor, having one argument.

Author:
Hendrik Maryns
See Also:
Serialized Form

Method Summary
 boolean containsVariable(Variable var)
          Returns whether this formula contains the given variable.
 boolean equals(Object other)
          An object is equal to a unary junctor if it has the same class (i.e., not only it is a unary junctor, but it really has the same leaf-level class), and the arguments are equal.
 Formula getArgument()
          Returns the argument.
 int getFirstIndexOf(Variable var)
          Get the first index at which the given variable occurs.
 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.
 int getNbVariables()
          Returns the number of variables in this formula.
 Set<Predicate> getPredicates()
          Return all predicates in this formula.
 Formula getSubformulaAt(int index)
          Returns the indexth subformula of this formula.
 Variable getVariableAt(int index)
          Get the indexth variable (free or bound).
 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, 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

getArgument

public Formula getArgument()
Returns the argument.

Returns:
This is the only subformula.
| result == getSubformulaAt(0)

getNbVariables

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

Returns:
All variables are contained in the argument.
| result == getArgument().getNbVariables()

getNbFreeVariables

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

Returns:
All variables are contained in the argument.
| result == getArgument().getNbFreeVariables()

getNbBoundVariables

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

Returns:
All variables are contained in the argument.
| result == getArgument().getNbBoundVariables()

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.

getVariableAt

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

Parameters:
index - The index of the wanted variable
Returns:
All variables are contained in the argument.
| result == getArgument().getVariableAt(index)

containsVariable

public boolean containsVariable(Variable var)
Returns whether this formula contains the given variable.

Parameters:
var - The variable to check.
Returns:
All variables are contained in the argument.
| result == getArgument().containsVariable(var)

isFreeVariable

public boolean isFreeVariable(Variable variable)
Check whether the given variable is free in this formula.

Parameters:
variable - The variable to check.
Returns:
The argument decides.
| result == getArgument().isFreeVariable(variable)

getPredicates

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


getNbSubformulas

public final int getNbSubformulas()
Returns the number of subformulas.

Specified by:
getNbSubformulas in class ComposedFormula
Returns:
A unary junctor always contains only one subformula.
| result == 1

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.
Returns:
A unary junctor has only one subformula; if the index is different from 0, an error is thrown. Thus, this formula is equivalent to getArgument().

equals

public boolean equals(Object other)
An object is equal to a unary junctor if it has the same class (i.e., not only it is a unary junctor, but it really has the same leaf-level class), and the arguments are equal.

Overrides:
equals in class FormulaImpl
Returns:
If the argument of the other object, viewed as a unary junctor is not equal to the argument of this binary junctor, then false.
| let otherJunctor = (UnaryJunctor) other in | if ( ! getArgument().equals(otherJunctor.getArgument()) ) | then result == false

hashCode

public int hashCode()
Returns a hash code value for the object.

Specified by:
hashCode in class FormulaImpl
Returns:
The hash code is based on the hash codes of the argument and of the characteristic symbol.
| result == getSymbol().hashCode() + getArgument().hashCode()

toString

public String toString()
Returns a string representation of the object.

Specified by:
toString in class FormulaImpl
Returns:
The string representation of a unary junctor is the string representation of its arguments prepended with an appropriate sign.
| result == getSymbol() + getArgument().toString()