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 body of any procedure declared cc_multi or cc_nondet is in a single-solution context. For example, the program entry point ‘main/2’ may be declared cc_multi, and in that case the clauses for main are in a single-solution context.
• Any goal with no output variables is in a single-solution context.
• If a conjunction is in a single-solution context, then the right-most conjunct is in a single-solution context, and if the right-most conjunct cannot fail, then rest of the conjunction is also in a single-solution context. (“Right-most” here refers to the order after mode reordering.)
• If an if-then-else is in a single-solution context, then the “then” part and the “else” part are in single-solution contexts, and if the “then” part cannot fail, then the condition of the if-then-else is also in a single-solution context.
• For other compound goals, i.e. disjunctions, negations, and (explicitly) existentially quantified goals, if the compound goal is in a single-solution context, then the immediate sub-goals of that compound goal are also in single-solution contexts.

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.