Constraint logic programming: Difference between revisions

Revision as of 00:20, 17 March 2006

Revision as of 13:46, 17 March 2006

Line 88:

However, the constraint store may also contain constraints in the form <code>t1!=t2</code>, if the difference <code>!=</code> between terms is allowed. When constraints over reals or finite domains are allowed, the constraint store may also contain ___domain-specific constraints like <code>X+2=Y/2</code>, etc.

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 the considered constraint language. While the result of a successful evaluation of a regular logic program is the final substitution, the result for a constraint logic program is the final constraint store, which may contain constraint of the form variable=value but in general may contain arbitrary constraints.

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.