Properties related to cardinality and exact solutions

Usage:cardinality(Goal,Lower,Upper)

Goal has a number of solutions between Lower and Upper.

• The following properties should hold globally:
  (basic_props:no_rtcheck/1)cardinality(Goal,Lower,Upper) is not checked during run-time checking.

Usage 1:num_solutions(X,N)

Calls of the form X have N solutions, i.e., N is the cardinality of the solution set of X.

• If the following properties should hold at call time:
  (basic_props:cgoal/1)X is a term which represents a goal, i.e., an atom or a structure.
  (basic_props:int/1)N is an integer.

Usage 2:num_solutions(Goal,Check)

For a call to Goal, Check(X) succeeds, where X is the number of solutions.

• If the following properties should hold at call time:
  (basic_props:cgoal/1)Goal is a term which represents a goal, i.e., an atom or a structure.
  (basic_props:cgoal/1)Check is a term which represents a goal, i.e., an atom or a structure.

Calls of the form X produce N solutions, i.e., N is the cardinality of the solution set of X.

Usage:relations(X,N)

Goal X produces N solutions.

• If the following properties should hold at call time:
  (basic_props:cgoal/1)X is a term which represents a goal, i.e., an atom or a structure.
  (basic_props:int/1)N is an integer.
  then the following properties should hold globally:
  (basic_props:rtcheck/2)The runtime check of this property is unimplemented.

Calls of the form X produce a finite number of solutions [DLGH97].

Usage:finite_solutions(X)

All the calls of the form X have a finite number of solutions.

• The following properties should hold globally:
  (basic_props:no_rtcheck/1)finite_solutions(X) is not checked during run-time checking.

Usage:solutions(Goal,Sols)

Goal Goal produces the solutions listed in Sols.

• If the following properties should hold at call time:
  (basic_props:cgoal/1)Goal is a term which represents a goal, i.e., an atom or a structure.
  (basic_props:list/1)Sols is a list.