de.uni_tuebingen.sfb.lichtenstein.formulas
Class FirstOrderQuantor

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

All Implemented Interfaces:

Formula, Quantification, Visitable, Serializable

Direct Known Subclasses:

FirstOrderExistentialQuantification, FirstOrderUniversalQuantification

public abstract class FirstOrderQuantor
extends ComposedFormula
implements Quantification

A class for representing quantors on first order variables, implementing common methods for existential and universal quantors.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

protected

FirstOrderQuantor(FirstOrderVariable var, Formula arg) Initialize a new quantor, given a variable to bind and a formula to act upon.

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 quantor if it has the same class (i.e., not only it is a quantor, but it really has the same leaf-level class), the arguments are equal and they bind the same variable.
Formula	getArgument() Returns the formula this quantor acts on.
FirstOrderVariable	getBoundVariable() Returns the variable that is bound by this quantor.
Set<Variable>	getFreeVariables() Return the free variables in this formula.
int	getNbSubformulas() Returns the number of subformulas of this formula.
Formula	getSubformulaAt(int index) Returns the indexth subformula of this formula.
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, 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

and, exists, exists, forAll, forAll, getNormalForm, getPredicates, getVariables, iff, implies, isClosed, not, or

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

accept

Constructor Detail

FirstOrderQuantor

protected FirstOrderQuantor(FirstOrderVariable var,
                            Formula arg)

Initialize a new quantor, given a variable to bind and a formula to act upon.

Parameters:

var - The variable that is bound by this quantor.

arg - The formula which this quantor acts upon.

Precondition:

The given variable and formula must be effective and the variable must not be bound in the given formula. | var != null && arg != null && (!arg.containsVariable(var) || arg.isFreeVariable(var))

Postconditions:

The bound variable is set to the given variable. | new.getBoundVariable() == var

The formula on which this quantor acts is set to the given formula. | new.getArgument() == arg

Method Detail

getBoundVariable

public FirstOrderVariable getBoundVariable()

Returns the variable that is bound by this quantor.

Specified by:

getBoundVariable in interface Quantification

getArgument

public Formula getArgument()

Returns the formula this quantor acts on.

Specified by:

getArgument in interface Quantification

computeVariables

protected Set<Variable> computeVariables()

Compute the set of variables in this formula. The bound variable is treated as the first variable in a quantification.

Specified by:

computeVariables in class FormulaImpl

getFreeVariables

public Set<Variable> getFreeVariables()

Return the free variables in this formula. This method should be overridden for efficiency, but this class provides a correct implementation. TODO

Specified by:

getFreeVariables in interface Formula

Overrides:

getFreeVariables in class FormulaImpl

See Also:

LinkedHashSet

containsVariable

public boolean containsVariable(Variable var)

Returns whether this formula contains the given variable.

Specified by:

containsVariable in interface Formula

Parameters:

var - The variable to check.

isFree

public boolean isFree(Variable variable)

Check whether the given variable is free in this formula.

Specified by:

isFree in interface Formula

Parameters:

variable - The variable to check.

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

equals

public boolean equals(Object other)

An object is equal to a quantor if it has the same class (i.e., not only it is a quantor, but it really has the same leaf-level class), the arguments are equal and they bind the same variable.

Overrides:

equals in class FormulaImpl

Returns:

If the argument of the other object, viewed as a quantor is not equal to the argument of this quantor, then false. | let otherQuantor = (Quantor) other in | if ( ! getArgument().equals(otherQuantor.getArgument()) ) | then result == false

Returns:

If the bound variable of the other object, viewed as a quantor is not equal to the bound variable of this quantor, then false. | let otherQuantor = (Quantor) other in | if ( ! getBoundVariable() == otherQuantor.getBoundVariable()) ) | 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 bound variable, the argument and the characteristic symbol. This last one is needed to make the difference between the various subclasses. | result == getSymbol().hashCode() + getBoundVariable().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 quantor is the string representation of its arguments with an appropriate sign in between. | result == "(" + getSymbol() + getBoundVariable().toString() + ")(" + getArgument().toString() + ")"