Node:Declaring Nondeterminacy, Next:Checker Output, Previous:Using the Determinacy Checker, Up:The Determinacy Checker

Declaring Nondeterminacy

Some predicates are intended to be nondeterminate. By declaring intended nondeterminacy, you avoid warnings about predicates you intend to be nondeterminate. Equally importantly, you also inform the determinacy checker about nondeterminate predicates. It uses this information to identify unwanted nondeterminacy.

Nondeterminacy is declared by putting a declaration of the form

:- nondet name/arity.

in your source file. This is similar to a dynamic or discontiguous declaration. You may have multiple nondet declarations, and a single declaration may mention several predicates, separating them by commas.

Similarly, a predicate P/N may be classified as nondeterminate by the checker, whereas in reality it is determinate. This may happen e.g. if P/N calls a dynamic predicate which in reality never has more than one clause. To prevent false alarms asiring from this, you can inform the checker about determinate predicates by declarations of the form:

:- det name/arity.

If you wish to include det and nondet declarations in your file and you plan to use the stand-alone determinacy checker, you must include the line

:- load_files(library(nondetdecl),
              [when(compile_time), if(changed)]).

near the top of each file that contains such declarations. If you use the integrated determinacy checker, you do not need (and should not have) this line.