LBJ2.infer
Class FirstOrderConstraint

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

Direct Known Subclasses:

FirstOrderBinaryConstraint, FirstOrderConstant, FirstOrderEquality, FirstOrderNAryConstraint, FirstOrderNegation, QuantifiedConstraintInvocation, Quantifier

public abstract class FirstOrderConstraint
extends Constraint

All classes for representing first order constraints are derived from this base class. A first order constraint is:

• The constant true or the constant false.
• An equality or inequality between a classifier application and a value (which may be specified with an arbitrary java expression) or between two classifier applications. Operators: == !=
• The negation of a first order constraint: ~
• The conjunction of two first order constraints: /\
• The disjunction of two first order constraints: \/
• An implication between two first order constraints: =>
• A double implication between two first order constraints: <=>
• An existential quantification: exists identifier in identifier, first-order-constraint
  The second identifier must refer to a Java Collection. The first identifier is a new Java variable of type Object that appears in the first order constraint.
• A universal quantification: forall identifier in identifier, first-order-constraint
  The second identifier must refer to a Java Collection. The first identifier is a new Java variable of type Object that appears in the first order constraint.
• An at least counting quantification: atleast expression of identifier in identifier, first-order-constraint
  The expression is arbitrary Java that must evaluate to a double. The two identifiers play the same role as in the other quatifications. This quatification is satisfied when the number of objects in the collection that satisfy first-order-constraint is greater than or equal to expression.
• An at most counting quatification: atmost expression of identifier in identifier, first-order-constraint
  The expression is arbitrary Java that must evaluate to a double. The two identifiers play the same role as in the other quatifications. This quatification is satisfied when the number of objects in the collection that satisfy first-order-constraint is less than or equal to expression.

Constructor Summary

FirstOrderConstraint()

Method Summary

abstract PropositionalConstraint	propositionalize() Transforms this first order constraint into a propositional constraint.
abstract 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 FirstOrderEquality children.

Methods inherited from class LBJ2.infer.Constraint

consolidateVariables, evaluate, getChildren, runVisit

Methods inherited from class java.lang.Object

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

Constructor Detail

FirstOrderConstraint

public FirstOrderConstraint()

Method Detail

setQuantificationVariables

public abstract 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 FirstOrderEquality children.

Parameters:

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

propositionalize

public abstract PropositionalConstraint propositionalize()

Transforms this first order constraint into a propositional constraint.

Returns:

The propositionalized constraint.