#### 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.