Previous: Interfacing nondeterministic code with the real world, 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: Interfacing nondeterministic code with the real world, Up: Determinism   [Contents]