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.