LBJ2.infer
Class EqualityArgumentReplacer

java.lang.Object
  LBJ2.infer.ArgumentReplacer
      LBJ2.infer.EqualityArgumentReplacer

public abstract class EqualityArgumentReplacer
extends ArgumentReplacer

Anonymous inner classes extending this class are instantiated by the code generated by the LBJ compiler when creating FirstOrderConstraint representations. The methods of this class are used to compute new values for the arguments of a quantified FirstOrderEquality. Only certain value returning methods are overridden. The others will throw UnsupportedOperationExceptions.

See Also:

FirstOrderConstraint, FirstOrderEquality, UnsupportedOperationException

Field Summary

boolean	leftConstant This flag is set if the left hand side of the equality is not quantified.
boolean	rightConstant This flag is set if the right hand side of the equality is not quantified.

Fields inherited from class LBJ2.infer.ArgumentReplacer

context, quantificationVariables

Constructor Summary

EqualityArgumentReplacer(java.lang.Object[] c)
Initializing constructor.

EqualityArgumentReplacer(java.lang.Object[] c, boolean r)
Use this constructor to indicate which of the two arguments of the equality is in fact not quantified.

Method Summary

java.lang.Object	getLeftObject() Computes the object on the left hand side of the equality.
java.lang.String	getLeftValue() Computes the value on the left hand side of the equality.
java.lang.Object	getRightObject() Computes the object on the right hand side of the equality.
java.lang.String	getRightValue() Computes the value on the right hand side of the equality.

Methods inherited from class LBJ2.infer.ArgumentReplacer

setQuantificationVariables

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

leftConstant

public boolean leftConstant

This flag is set if the left hand side of the equality is not quantified.

rightConstant

public boolean rightConstant

This flag is set if the right hand side of the equality is not quantified.

Constructor Detail

EqualityArgumentReplacer

public EqualityArgumentReplacer(java.lang.Object[] c)

Initializing constructor.

Parameters:

c - The context of the corresponding equality, except for quantification variables.

EqualityArgumentReplacer

public EqualityArgumentReplacer(java.lang.Object[] c,
                                boolean r)

Use this constructor to indicate which of the two arguments of the equality is in fact not quantified.

Parameters:

c - The context of the corresponding equality, except for quantification variables.

r - Set to false if the unquantified argument is the left; set to true if the unquantified argument is the right.

Method Detail

getLeftValue

public java.lang.String getLeftValue()

Computes the value on the left hand side of the equality. This method needs to be overridden if it is to be called, since by default it simply throws an UnsupportedOperationException.

getRightValue

public java.lang.String getRightValue()

Computes the value on the right hand side of the equality. This method needs to be overridden if it is to be called, since by default it simply throws an UnsupportedOperationException.

getLeftObject

public java.lang.Object getLeftObject()

Computes the object on the left hand side of the equality. This method needs to be overridden if it is to be called, since by default it simply throws an UnsupportedOperationException.

getRightObject

public java.lang.Object getRightObject()

Computes the object on the right hand side of the equality. This method needs to be overridden if it is to be called, since by default it simply throws an UnsupportedOperationException.