Solver Invocation

A solver invocation call invokes a solver with a list of variables and an optional list of options. For example, the option min(E) minimizes the expression E, and max(E) maximizes E. When the solver succeeds in finding an answer, the call succeeds with a valuation of the variables. When the solver fails to find any answer, the call fails. The following primitives are provided:

A solver invocation call can only succeed once. Unlike the labeling predicates in CLP(FD), execution can never backtrack to the call. Nevertheless, it is possible to program backtracking to search for more answers. The following primitives are provided to return all answers, where Bag is for returning all answers:

The solver is repeatedly invoked, until it fails to return any new answer. After each success, the answer is inserted into the database, and new constraints are added in order to ensure that the next answer that is returned will be different from the existing answers. In the end, all of the answers in the database are collected into a list, and Bag is bound to the list.

Neng-Fa Zhou 2013-01-25