Properties related to determinacy, failure, choice-points

These properties are part of the native_props library.

Usage and interface

Documentation on exports

PROPERTYdet/1
det(X)

Calls of the form X are deterministic, i.e., produce exactly one solution (or do not terminate).

Note that it can still leave choice points after its execution, but when backtracking into these, it can only fail or go into an infinite loop.

These properties are inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10,DLGH97,BLGH04].

Usage:det(X)

Calls of the form X are deterministic.

    Meta-predicate with arguments: det(goal).

    PROPERTYsemidet/1
    semidet(X)

    Calls of the form X are semi-deterministic, i.e., produce at most one solution (or do not terminate).

    Note that it can still leave choice points after its execution, but when backtracking into these, it can only fail or go into an infinite loop.

    These properties are inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10,DLGH97,BLGH04].

    Usage:semidet(X)

    Calls of the form X are semi-deterministic.

      Meta-predicate with arguments: semidet(goal).

      PROPERTYmulti/1
      multi(X)

      Calls of the form X are multi-deterministic, i.e., they produce one or more solutions and do not fail.

      Usage:multi(X)

      Calls of the form X are multi-deterministic.

        Meta-predicate with arguments: multi(goal).

        PROPERTYnondet/1
        nondet(X)

        Nothing is ensured about failure and determinacy of calls to X. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

        Usage:nondet(X)

        Calls of the form X are non-deterministic.

        • The following properties should hold globally:
          (basic_props:no_rtcheck/1)nondet(X) is not checked during run-time checking.
        Meta-predicate with arguments: nondet(goal).

        mut_exclusive(X)

        For any call of the form X there is at most one clause whose test (guard) succeeds, i.e., clause tests are pairwise exclusive. Note that determinacy is the transitive closure (to all called predicates) of this property. This property is inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10].

        Usage:mut_exclusive(X)

        For any call of the form X at most one clause test succeeds.

        • The following properties should hold globally:
          (basic_props:rtcheck/2)The runtime check of this property is unimplemented.
        Meta-predicate with arguments: mut_exclusive(goal).

        not_mut_exclusive(X)

        For calls of the form X more than one clause test may succeed. I.e., clause tests are not disjoint for some call.

        Usage:not_mut_exclusive(X)

        For some calls of the form X more than one clause test may succeed.

        • The following properties should hold globally:
          (basic_props:rtcheck/2)The runtime check of this property is unimplemented.
        Meta-predicate with arguments: not_mut_exclusive(goal).

        possibly_not_mut_exclusive(X)

        Mutual exclusion of the clause tests for calls of the form X cannot be ensured. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

        Usage:possibly_not_mut_exclusive(X)

        Mutual exclusion is not ensured for calls of the form X.

        • The following properties should hold globally:
          (basic_props:no_rtcheck/1)possibly_not_mut_exclusive(X) is not checked during run-time checking.
        Meta-predicate with arguments: possibly_not_mut_exclusive(goal).

        PROPERTYcovered/1
        covered(X)

        For any call of the form X there is at least one clause whose test (guard) succeeds (i.e., all the calls of the form X are covered). Note that nonfailure is the transitive closure (to all called predicates) of this property. [DLGH97,BLGH04].

        Usage:covered(X)

        All the calls of the form X are covered.

        • The following properties should hold globally:
          (basic_props:rtcheck/2)The runtime check of this property is unimplemented.
        Meta-predicate with arguments: covered(goal).

        not_covered(X)

        There is some call of the form X for which there is no clause whose test succeeds [DLGH97].

        Usage:not_covered(X)

        Not all of the calls of the form X are covered.

        • The following properties should hold globally:
          (basic_props:rtcheck/2)The runtime check of this property is unimplemented.
        Meta-predicate with arguments: not_covered(goal).

        possibly_not_covered(X)

        Covering is not ensured for any call of the form X. In other words, nothing can be ensured about covering of such calls.

        Usage:possibly_not_covered(X)

        Covering is not ensured for calls of the form X.

        • The following properties should hold globally:
          (basic_props:no_rtcheck/1)possibly_not_covered(X) is not checked during run-time checking.
        Meta-predicate with arguments: possibly_not_covered(goal).

        Usage:no_choicepoints(X)

        A call to X does not leave new choicepoints.

          Meta-predicate with arguments: no_choicepoints(goal).

          Usage:leaves_choicepoints(X)

          A call to X leaves new choicepoints.

            Meta-predicate with arguments: leaves_choicepoints(goal).

            PROPERTYis_det/1
            is_det(X)

            All calls of the form X are deterministic, i.e., produce at most one solution (or do not terminate). In other words, if X succeeds, it can only succeed once. It can still leave choice points after its execution, but when backtracking into these, it can only fail or go into an infinite loop. This property is inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10].

            Usage:is_det(X)

            All calls of the form X are deterministic.

              Meta-predicate with arguments: is_det(goal).

              PROPERTYnon_det/1
              non_det(X)

              All calls of the form X are non-deterministic, i.e., they always produce more than one solution.

              Usage:non_det(X)

              All calls of the form X are non-deterministic.

                Meta-predicate with arguments: non_det(goal).

                possibly_nondet(X)

                Non-determinism is not ensured for calls of the form X. In other words, nothing can be ensured about determinacy of such calls. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

                Usage:possibly_nondet(X)

                Non-determinism is not ensured for calls of the form X.

                • The following properties should hold globally:
                  (basic_props:no_rtcheck/1)possibly_nondet(X) is not checked during run-time checking.
                Meta-predicate with arguments: possibly_nondet(goal).

                PROPERTYnot_fails/1
                not_fails(X)

                Calls of the form X produce at least one solution (succeed), or do not terminate. This property is inferred and checked natively by CiaoPP using the domains and techniques of [DLGH97,BLGH04].

                Usage:not_fails(X)

                All the calls of the form X do not fail.

                • The following properties should hold globally:
                  (basic_props:native/1)This predicate is understood natively by CiaoPP.
                Meta-predicate with arguments: not_fails(goal).

                possibly_fails(X)

                Non-failure is not ensured for any call of the form X. In other words, nothing can be ensured about non-failure nor termination of such calls.

                Usage:possibly_fails(X)

                Non-failure is not ensured for calls of the form X.

                • The following properties should hold globally:
                  (basic_props:no_rtcheck/1)possibly_fails(X) is not checked during run-time checking.
                Meta-predicate with arguments: possibly_fails(goal).

                Documentation on imports

                This module has the following direct dependencies: