LBJ2.infer
Class QuantifierArgumentReplacer

java.lang.Object
  LBJ2.infer.ArgumentReplacer
      LBJ2.infer.QuantifierArgumentReplacer

public abstract class QuantifierArgumentReplacer
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 Quantifier. Only certain value returning methods are overridden. The others will throw UnsupportedOperationExceptions.

See Also:

FirstOrderConstraint, Quantifier, UnsupportedOperationException

Field Summary

boolean	boundConstant This flag is set if the bound parameter of an AtLeastQuantifier or an AtMostQuantifier is not quantified.
boolean	collectionConstant This flag is set if the collection of the quantifier is not quantified.

Fields inherited from class LBJ2.infer.ArgumentReplacer

context, quantificationVariables

Constructor Summary

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

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

Method Summary

int	getBound() Computes the new value of the bound.
java.util.Collection	getCollection() Computes the new collection.

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

collectionConstant

public boolean collectionConstant

This flag is set if the collection of the quantifier is not quantified.

boundConstant

public boolean boundConstant

This flag is set if the bound parameter of an AtLeastQuantifier or an AtMostQuantifier is not quantified.

Constructor Detail

QuantifierArgumentReplacer

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

Initializing constructor.

Parameters:

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

QuantifierArgumentReplacer

public QuantifierArgumentReplacer(java.lang.Object[] c,
                                  boolean b)

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.

b - Set to false if the unquantified argument is the collection; set to true if the unquantified argument is the bound.

Method Detail

getCollection

public java.util.Collection getCollection()

Computes the new collection. This method needs to be overridden if it is to be called, since by default it simply throws an UnsupportedOperationException.

getBound

public int getBound()

Computes the new value of the bound. This method needs to be overridden if it is to be called, since by default it simply throws an UnsupportedOperationException.