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:
Note that the reification scheme introduced in Reified Constraints is a special case of a propositional constraint.