10.34.3.3 Propositional Constraints

Propositional combinators can be used to combine reifiable constraints into propositional formulae over such constraints. Such formulae are goal expanded by the system into sequences of reified constraints and arithmetic constraints. For example,

     X #= 4 #\/ Y #= 6

expresses the disjunction of two equality constraints.

The leaves of propositional formulae can be reifiable constraints, the constants 0 and 1, or 0/1-variables. New primitive, reifiable constraints can be defined with indexicals as described in Defining Primitive Constraints. The following propositional combinators are available:

#\ :Q

True if the constraint Q is false.

:P #/\ :Q

True if the constraints P and Q are both true.

:P #\ :Q

True if exactly one of the constraints P and Q is true.

:P #\/ :Q

True if at least one of the constraints P and Q is true.

:P #=> :Q

:Q #<= :P

True if the constraint Q is true or the constraint P is false.

:P #<=> :Q

True if the constraints P and Q are both true or both false.

Note that the reification scheme introduced in Reified Constraints is a special case of a propositional constraint.