LBJ2.infer
Class AtMostQuantifier

java.lang.Object
  LBJ2.infer.Constraint
      LBJ2.infer.FirstOrderConstraint
          LBJ2.infer.Quantifier
              LBJ2.infer.AtMostQuantifier

public class AtMostQuantifier
extends Quantifier

An "at most" quantifier states that the constraint must hold for no more than m of the objects in the collection.

Field Summary

protected int

m The maximum number of objects for which the constraint must hold.

Fields inherited from class LBJ2.infer.Quantifier

collection, constraint, enclosingQuantificationSettings, quantificationVariable, replacer

Constructor Summary

AtMostQuantifier(java.lang.String q, java.util.Collection col, FirstOrderConstraint con, int m)
Initializing constructor.

AtMostQuantifier(java.lang.String q, java.util.Collection col, FirstOrderConstraint con, int m, QuantifierArgumentReplacer qar)
This constructor specifies a variable setter for when this quantifier is itself quantified.

Method Summary

boolean	equals(java.lang.Object o) Two AtMostQuantifiers are equivalent when their children are equivalent.
boolean	evaluate() Determines whether the constraint is satisfied.
int	hashCode() The hash code of a AtMostQuantifier is the sum of the hash codes of its children.
PropositionalConstraint	propositionalize() Transforms this first order constraint into a propositional constraint.
void	runVisit(Inference infer) Calls the appropriate visit(·) method of the given Inference for this Constraint, as per the visitor pattern.
void	setQuantificationVariables(java.util.Vector o) This method sets the given quantification variables to the given object references and evaluates the expressions involving those variables in this constraint's children.

Methods inherited from class LBJ2.infer.Quantifier

consolidateVariables, getChildren, initialize

Methods inherited from class java.lang.Object

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

Field Detail

m

protected int m

The maximum number of objects for which the constraint must hold.

Constructor Detail

AtMostQuantifier

public AtMostQuantifier(java.lang.String q,
                        java.util.Collection col,
                        FirstOrderConstraint con,
                        int m)

Initializing constructor.

Parameters:

q - The name of the quantification variable.

col - The collection of objects to iterate over.

con - The constraint being quantified.

m - The number of objects for which the constraint must hold.

AtMostQuantifier

public AtMostQuantifier(java.lang.String q,
                        java.util.Collection col,
                        FirstOrderConstraint con,
                        int m,
                        QuantifierArgumentReplacer qar)

This constructor specifies a variable setter for when this quantifier is itself quantified.

Parameters:

q - The name of the quantification variable.

col - The collection of objects to iterate over.

con - The constraint being quantified.

m - The number of objects for which the constraint must hold.

qar - The variable setter.

Method Detail

evaluate

public boolean evaluate()

Determines whether the constraint is satisfied.

Specified by:

evaluate in class Constraint

setQuantificationVariables

public void setQuantificationVariables(java.util.Vector o)

This method sets the given quantification variables to the given object references and evaluates the expressions involving those variables in this constraint's children.

Specified by:

setQuantificationVariables in class FirstOrderConstraint

Parameters:

o - The new object references for the enclosing quantification variables, in order of nesting.

propositionalize

public PropositionalConstraint propositionalize()

Transforms this first order constraint into a propositional constraint.

Specified by:

propositionalize in class FirstOrderConstraint

Returns:

The propositionalized constraint.

hashCode

public int hashCode()

The hash code of a AtMostQuantifier is the sum of the hash codes of its children.

Overrides:

hashCode in class Quantifier

Returns:

The hash code for this AtMostQuantifier.

equals

public boolean equals(java.lang.Object o)

Two AtMostQuantifiers are equivalent when their children are equivalent.

Overrides:

equals in class Quantifier

Returns:

true iff the argument is an equivalent AtMostQuantifier.

runVisit

public void runVisit(Inference infer)

Calls the appropriate visit(·) method of the given Inference for this Constraint, as per the visitor pattern.

Specified by:

runVisit in class Constraint

Parameters:

infer - The inference visiting this constraint.