Content deleted Content added
bold constraint store (redirect) + section on the constraint store |
→The constraint store: local consistency, backtracking, trailing |
||
Line 59:
The constraint store extends the concept of current substitution in two ways: first, it does not only contains the constraints derived from equating a literal with the head of a rewritten clause, but also the constraints of the body of clauses; second, it does not only contains constraints of the form <code>variable=value</code> but also constraints on reals or a finite ___domain, depending on the considered ___domain.
Domain-specific constraints may come to the constraint store both from the body of a clauses and from matching of a literals with a clause head: for example, if the interpreter rewrites the literal <code>A(X+2)</code> with a clause whose rewritten head is <code>A(Y/2)</code>, the constraint <code>X+2=Y/2</code> is added to the constraint store. If a variable appears in a real or finite ___domain expression, it can only take a value in the reals or the finite ___domain. Such a variable cannot take a term made of a functor applied to other terms as a value. The constraint store is unsatisfiable if a variable is bound to take both a value of the specific ___domain and a functor applied to terms.
After a constraint is added to the constraint store, some operations may be performed on the constraint store. Depending on the ___domain, these may be arithmetic simplifications for reals or [[constraint propagation]] to enforce a form of [[local consistency]] for finite domains.
As a result, the addition of new constraints may change the old ones. It is essential that the interpreter is able to undo these changes when it backtracks. The simplest case method is for the interpreter to save the complete state of the store every time it makes a choice (it chooses a clause to rewrite a goal). More efficient methods for allowing the constraint store to return to a previous state exist. In particular, one may just save the changes to the constraint store made between two points of choice, including the changes made to the old constraints. This can be done by simply saving the old value of the constraints that have been modified; this method is called ''trailing''. A more advanced method is to save the changes that have been done on the modified constraints. For example, a linear constraint is changed by modifying its coefficient: saving the difference between the old and new coefficient allows reverting a change. This second method is called ''semantic backtracking'', because the semantics of the change is saved rather than the old version of the constraints only.
==Labeling==
| |||