Constraint logic programming: Difference between revisions

Revision as of 00:23, 5 June 2020

Revision as of 16:49, 29 July 2020

Line 17:

Whether a constraint is satisfied cannot always be determined when the constraint is encountered. In this case, for example, the value of <code>X</code> is not determined when the last clause is evaluated. As a result, the constraint <code>X>0</code> is not satisfied nor violated at this point. Rather than proceeding in the evaluation of <code>B(X,1)</code> and then checking whether the resulting value of <code>X</code> is positive afterwards, the interpreter stores the constraint <code>X>0</code> and then proceeds in the evaluation of <code>B(X,1)</code>; this way, the interpreter can detect violation of the constraint <code>X>0</code> during the evaluation of <code>B(X,1)</code>, and backtrack immediately if this is the case, rather than waiting for the evaluation of <code>B(X,1)</code> to conclude.

In general, the evaluation of a constraint logic program proceeds likeas fordoes a regular logic program. However, but constraints encountered during evaluation are placed in a set called a constraint store. As an example, the evaluation of the goal <code>A(X,1)</code> proceeds by evaluating the body of the first clause with <code>Y=1</code>; this evaluation adds <code>X>0</code> to the constraint store and requires the goal <code>B(X,1)</code> to be provedproven. While trying to prove this goal, the first clause is applicable,applied but its evaluation adds <code>X<0</code> to the constraint store. This addition makes the constraint store unsatisfiable,. andThe theinterpreter interpreterthen backtracks, removing the last addition from the constraint store. The evaluation of the second clause adds <code>X=1</code> and <code>Y>0</code> to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution <code>X=1, Y=1</code>.

==Semantics==