de.uni_tuebingen.sfb.lichtenstein.formulas
Class BinaryJunctor

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

All Implemented Interfaces:

Formula, Visitable, Serializable

Direct Known Subclasses:

Equivalence, Implication

public abstract class BinaryJunctor
extends ComposedFormula

A superclass for implication and equivalence, 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.
boolean	equals(Object other) An object is equal to a binary junctor if it has the same class (i.e., not only it is a binary junctor, but it really has the same leaf-level class), and the arguments are both equal, respectively.
Formula	getFirstArgument() Returns the first 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 binary junctor.
int	getNbFreeVariables() Returns the number of free variables in this binary junctor.
int	getNbSubformulas() Returns the number of direct subformulas.
int	getNbVariables() Returns the number of variables in this binary junctor.
Set<Predicate>	getPredicates() Return all predicates that occur in this formula.
Formula	getSecondArgument() Returns the second argument.
Formula	getSubformulaAt(int index) Returns the subformulas this binary junction is built up of.
Variable	getVariableAt(int index) Get the indexth variable.
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

getFirstArgument

public Formula getFirstArgument()

Returns the first argument.

Returns:

This is the first subformula.

| result == getSubformulaAt(0)

getSecondArgument

public Formula getSecondArgument()

Returns the second argument.

Returns:

This is the second subformula.

| result == getSubformulaAt(1)

getNbVariables

public int getNbVariables()

Returns the number of variables in this binary junctor.

Returns:

The sum of the number of variables of the arguments.

| getFirstArgument().getNbVariables() +
         getSecondArgument().getNbVariables()

getNbFreeVariables

public int getNbFreeVariables()

Returns the number of free variables in this binary junctor.

Returns:

The sum of the number of free variables of the arguments.

| result ==
         getFirstArgument().getNbFreeVariables() + getSecondArgument().getNbFreeVariables()

getNbBoundVariables

public int getNbBoundVariables()

Returns the number of bound variables in this binary junctor.

Returns:

The sum of the number of bound variables of the arguments.

| getFirstArgument().getNbBoundVariables() +
         getSecondArgument().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.

Parameters:

index - The index of the wanted variable

Returns:

The indexth variable of the first argument, or, if there are less than index variables in the first argument, the ( index - getFirstArgument().getNbVariables() )th variable of the second argument.

| if (
         getFirstArgument().getNbVariables() > index )
| then result == getFirstArgument().getVariableAt(index) |
         else result == getSecondArgument().getVariableAt(index - getFirstArgument().getNbVariables())

containsVariable

public boolean containsVariable(Variable var)

Returns whether this formula contains the given variable.

Parameters:

var - The variable to check.

Returns:

True if either the first or the second argument contains the given variable.

| result ==
         getFirstArgument().containsVariable(var)
|| | getSecondArgument().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:

True if it is free in either argument.

| result == getFirstArgument().isFreeVariable(variable) ||
         getSecondArgument().isFreeVariable(variable)

getPredicates

public Set<Predicate> getPredicates()

Return all predicates that occur in this formula. TODO

getNbSubformulas

public final int getNbSubformulas()

Returns the number of direct subformulas.

Specified by:

getNbSubformulas in class ComposedFormula

Returns:

A binary junctor always has two subformulas.

| result == 2

getSubformulaAt

public Formula getSubformulaAt(int index)

Returns the subformulas this binary junction is built up of.

Specified by:

getSubformulaAt in class ComposedFormula

Parameters:

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

Returns:

The first or second argument, respectively. If index is different from 0 or 1, an exception is thrown.

equals

public boolean equals(Object other)

An object is equal to a binary junctor if it has the same class (i.e., not only it is a binary junctor, but it really has the same leaf-level class), and the arguments are both equal, respectively.

Overrides:

equals in class FormulaImpl

Returns:

If the arguments of the other object, viewed as a binary junctor are not equal to the arguments of this binary junctor, respectively, then false.

| let otherJunctor = (BinaryJunctor) other in | if ( !
         getFirstArgument().equals(otherJunctor.getFirstArgument())
|| | !
         getSecondArgument().equals(otherJunctor.getSecondArgument()) )
| then result == false

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.

| result ==
         getFirstArgument().hashCode() + getSymbol().hashCode() + getSecondArgument().hashCode()

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 a binary junctor is the string representation of its arguments with an appropriate sign in between.

| result.contains(getFirstArgument().toString() + getSymbol() +
         getSecondArgument().toString())