10.35.10.8 Goal Expanded Constraints

The arithmetic, membership, and propositional constraints described earlier are transformed at compile time to conjunctions of library constraints. Although linear in the size of the source code, the expansion of a constraint to library goals can have time and memory overheads. Temporary variables holding intermediate values may have to be introduced, and the grain size of the constraint solver invocations can be rather small. Therefore, an automatic translation by compilation to indexicals is also provided for a selected set of constraints. The syntax for this construction is:

Head +: ConstraintBody.
Head should be a compound term with all arguments being distinct variables. ConstraintBody should be a constraint amenable to compilation to indexicals, and should not contain any variable not mentioned in Head. This clause defines the constraint Head to hold iff ConstraintBody is true.

Roughly, a constraint amenable to such compilation is of one of the following forms, or is a propositional combination of such forms. See Syntax of Indexicals for the exact definition:


Send feedback on this subject.