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

Constructor Summary

protected

BinaryJunctor(Formula first, Formula second) Initialize a new binary junctor, taking two 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.
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	getNbSubformulas() Returns the number of direct subformulas.
Formula	getSecondArgument() Returns the second argument.
Formula	getSubformulaAt(int index) Returns the subformulas this binary junction is built up of.
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, 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

BinaryJunctor

protected BinaryJunctor(Formula first,
                        Formula second)

Initialize a new binary junctor, taking two formulas as arguments.

Parameters:

first - The first argument.

second - The second argument.

Postconditions:

The first argument is set to the given first argument. | new.getFirstArgument() == first

The second argument is set to the given second argument. | new.getSecondArgument() == second

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)

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 either the first or the second argument contains the given variable. | result == getFirstArgument().containsVariable(var) || | getSecondArgument().containsVariable(var)

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 == getFirstArgument().isFreeVariable(variable) || getSecondArgument().isFreeVariable(variable)

computePredicates

protected Set<Predicate> computePredicates()

Compute the set of predicates in this formula.

Specified by:

computePredicates in class FormulaImpl

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()) result.contains(getSymbol()) result.contains(getSecondArgument().toString())