de.uni_tuebingen.sfb.lichtenstein.formulas
Class FirstOrderQuantor

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

Method Summary
 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.
 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 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.
 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
and, exists, exists, forAll, forAll, getFreeVariables, getNormalForm, getVariables, iff, implies, isClosed, not, or
 
Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable
accept
 

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

getNbVariables

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

Specified by:
getNbVariables in interface Formula

getNbFreeVariables

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

Specified by:
getNbFreeVariables in interface Formula

getNbBoundVariables

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

Specified by:
getNbBoundVariables in interface Formula

getFirstIndexOf

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

Specified by:
getFirstIndexOf in interface Formula
Parameters:
var - The variable of which the index is wanted.

getVariableAt

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

Specified by:
getVariableAt in interface Formula
Parameters:
index - The index of the wanted variable

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.

isFreeVariable

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

Specified by:
isFreeVariable in interface Formula
Parameters:
variable - The variable to check.

getPredicates

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

Specified by:
getPredicates in interface Formula

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.

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