Content deleted Content added
rm link to deleted article |
Iridescent (talk | contribs) m →The constraint store: Typo fixing, typo(s) fixed: For example → For example, using AWB |
||
Line 89:
Domain-specific constraints may come to the constraint store both from the body of a clauses and from equating a literal with a clause head: for example, if the interpreter rewrites the literal <code>A(X+2)</code> with a clause whose fresh variant 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 are performed on the constraint store. Which operations are performed depends on the considered ___domain and constraints. For example, [[unification (computing)|unification]] is used for finite tree equalities, [[variable elimination]] for polynomial equations over reals, [[constraint propagation]] to enforce a form of [[local consistency]] for finite domains. These operations are aimed at making the constraint store simpler to be checked for satisfiability and solved.
As a result of these operations, 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'',
| |||