de.uni_tuebingen.sfb.lichtenstein.formulas
Class SecondOrderEquality

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      extended by de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula
          extended by de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderEquality
All Implemented Interfaces:
Formula, Visitable, Serializable

public final class SecondOrderEquality
extends AtomicFormula

A class representing the atomic formula that says two variables are equal.

Author:
Hendrik Maryns
See Also:
Serialized Form

Constructor Summary
SecondOrderEquality(SetDenotator first, SetDenotator second)
          Initialize a new equality, involving two set denotators.
 
Method Summary
 void accept(FormulaVisitor visitor)
          Accept a formula visitor.
protected  Set<Predicate> computePredicates()
          Return all predicates in this formula.
protected  Set<Variable> computeVariables()
          Simply return the two variables.
 boolean containsVariable(Variable var)
          Returns whether this formula contains the given variable.
 boolean equals(Object other)
          Indicates whether some other object is “equal to” this one.
 SetDenotator getFirstVariable()
          Returns the first variable.
 SetDenotator getSecondVariable()
          Returns the second variable.
 int hashCode()
          Returns a hash code value for the object.
 String toString()
          Returns a string representation of the object.
 
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula
getNormalForm, isFree
 
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
 

Constructor Detail

SecondOrderEquality

public SecondOrderEquality(SetDenotator first,
                           SetDenotator second)
Initialize a new equality, involving two set denotators.

Parameters:
first - The first variable.
second - The second variable.
Precondition:
Both variables have to be effective. | first != null && second != null
Postconditions:
  • The first variable is given to the first given variable. | new.getFirstVariable() == first
  • The second variable is given to the second given variable. | new.getSecondVariable() == second
  • Method Detail

    getFirstVariable

    public SetDenotator getFirstVariable()
    Returns the first variable.

    Returns:
    This is the first second order variable. | result == getVariableAt(0)

    getSecondVariable

    public SetDenotator getSecondVariable()
    Returns the second variable.

    Returns:
    This is the second second order variable. | result == getVariableAt(0)

    computeVariables

    protected Set<Variable> computeVariables()
    Simply return the two variables.

    Specified by:
    computeVariables in class FormulaImpl
    Returns:
    The two variables in the right order. | result.size() == 2 && | result.contains(getFirstVariable()) && | result.contains(getSecondVariable())

    containsVariable

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

    Parameters:
    var - The variable to check.

    computePredicates

    protected Set<Predicate> computePredicates()
    Return all predicates in this formula.

    Specified by:
    computePredicates in class FormulaImpl
    Returns:
    Both variables can be a predicate. | if ( getFirstVariable() instanceof Predicate ) | then result.contains(getFirstVariable()) | if ( getSecondVariable() instanceof Predicate ) | then result.contains(getSecondVariable())

    equals

    public boolean equals(Object other)
    Indicates whether some other object is “equal to” this one.

    Overrides:
    equals in class FormulaImpl
    Returns:
    Two equalities are equal if they compare the same variables. | let otherEquals = (SecondOrderEquality) other in | if ( otherEquals.getFirstVariable() != getFirstVariable() ) | then result == false | else if ( otherEquals.getSecondVariable() != getSecondVariable() ) | then result == false | else result == true

    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 variables and of the characteristic symbol. | result == getFirstVariable().hashCode() + "=".hashCode() + getSecondVariable().hashCode()

    toString

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

    Specified by:
    toString in class FormulaImpl
    Returns:
    The string representations of the variables are given, with the equal sign: = in between them. | result == getFirstVariable().toString() + "=" + getSecondVariable().toString()

    accept

    public void accept(FormulaVisitor visitor)
                throws VisitorException
    Accept a formula visitor. The iteration is done by the visitor, not by the composed formulas.

    Parameters:
    visitor - The visitor that is to be accepted to do its work.
    Throws:
    VisitorException - [CAN] A visitor can throw an exception.


    © Copyright 2008 Hendrik Maryns   Creative Commons License