Previous: , Up: Determinism   [Contents]

6.5 Committed choice nondeterminism

In addition to the determinism annotations described earlier, there are “committed choice” versions of multi and nondet, called cc_multi and cc_nondet. These can be used instead of multi or nondet if all calls to that mode of the predicate (or function) occur in a context in which only one solution is needed.

Such single-solution contexts are determined as follows.

The compiler will check that all calls to a committed-choice mode of a predicate (or function) do indeed occur in a single-solution context.

You can declare two different modes of a predicate (or function) which differ only in “cc-ness” (i.e. one being ‘multi’ and the other ‘cc_multi’, or one being ‘nondet’ and the other ‘cc_nondet’). In that case, the compiler will select the appropriate one for each call depending on whether the call comes from a single-solution context or not. Calls from single-solution contexts will call the committed choice version, while calls which are not from single-solution contexts will call the backtracking version.

There are several reasons to use committed choice determinism annotations. One reason is for efficiency: committed choice annotations allow the compiler to generate much more efficient code. Another reason is for doing I/O, which is allowed only in ‘det’ or ‘cc_multi’ predicates, not in ‘multi’ predicates. Another is for dealing with types that use non-canonical representations (see User-defined equality and comparison). And there are a variety of other applications.

Previous: , Up: Determinism   [Contents]