10.10.4.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 propositional combinators maintain domain-consistency and their reified versions detect domain-entailment and -disentailment. The following propositional combinators are available:

#\ :Q   reifiable

True if the constraint Q is false.

:P #/\ :Q   reifiable

True if the constraints P and Q are both true.

:P #\ :Q   reifiable

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

:P #\/ :Q   reifiable

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

:P #=> :Q   reifiable

:Q #<= :P   reifiable

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

:P #<=> :Q   reifiable

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.