CHR not triggering rules on variable update

[rudihorn]

I've been trying to experiment with constraint handling rules with ELPI, and as far as I can tell the CHR behaviour does not match that of SWI. Specifically the SWI CHR manual (https://www.swi-prolog.org/pldoc/man?section=SyntaxAndSemantics) states:

The other way it may interact again with the rules is when a variable appearing in the constraint becomes bound to either a non-variable or another variable involved in one or more constraints. In that case the constraint is triggered, i.e. it becomes an active constraint and all the rules are tried.

Example

To demonstrate the behaviour I have written a small application in SWI and ELPI.

Correct Behaviour (SWI)

Program:

:- module(simple, [tr/2]).
:- use_module(library(chr)).
:- chr_constraint tr/2.

tr1 @ tr(X,0) <=> X = 0.

Running swipl simple.pl <<< "tr(X, Y), tr(Y, 0).":
Output:

X = Y, Y = 0.

Execution: SWI starts with tr(X,Y) and tries to match it with any rule. As this doesn't happen, tr(X,Y) is suspended and SWI considers the next rule tr(Y,0) as active. This second rule matches the tr1 rule, and updates Y=0. As the variable Y is used by tr(X,Y), this rule becomes active again and tries to match tr(X,0) which matches tr1, setting X=0.

Incorrect Behaviour (ELPI)

Program:

mode (tr i i).
tr X Y :- declare_constraint (tr X Y) [].
constraint tr {
  rule \ (tr X 0) <=> (X = 0).
}

Running elpi simple.elpi <<< "tr X Y, tr Y 0.":
Output:

Success:
  X = X0
  Y = 0

Constraints:
 tr X0 0  /* suspended on  */

Execution: ELPI similarly starts with the rule tr X Y, which does not match any rules, suspending it. It next tries the rule tr Y 0, which matches the equivalent of tr1, setting Y=0. The tr X0 0 rule is left suspended, even though it could be matched with tr1, eliminating it and setting X=0.

Comment

I'm not sure if I've misunderstood Elpi in some form or another. I have also noticed there is a small bug in the GCD example, where the line

gcd A (uvar as Group) :- declare_constraint (gcd A Group) Group.

should be:

gcd A (uvar as Group) :- declare_constraint (gcd A Group) [Group].

[gares]

Thanks for the detailed report.

Constraints are resumed only when any of the variables they are keyd on gets assigned. That would be the list you pass to declare_constraint.
This API is not very nice and high level, since you have to check which arguments of tr are variables, using var for example, and pass them to the constraint API.

I'm sorry the doc is so slim, I'm working on it.

[rudihorn]

Hi gares,

thanks for your help.

I've tried the following example now, which seems to work for the purpose. I assume it woludn't work for variables in predicates though (e.g. updating X for a suspended constraint tr (pre X) Y). Is there a builtin function to recover all the vars / a nicer way to do things or is this WIP? Was thinking of something like tr X Y :- declare_constraint (tr X Y) (fv X ++ fv Y).

mode (tr i i).

type tr int -> int -> prop.

tr X Y :- var X, var Y, declare_constraint (tr X Y) [X, Y].
tr X Y :- var X, declare_constraint (tr X Y) [X].
tr X Y :- var Y, declare_constraint (tr X Y) [Y].
tr X Y :- declare_constraint (tr X Y) [].

constraint tr {
  rule \ (tr X 0) <=> (X = 0).
}

[gares]

Great, I had no time to try it out myself. Glad it works.

No, there is no such a builtin, mainly because it does not work "well" with binders (the higher order case, when a variable is under a binder it is unclear how to pull it out). But what could work is to have declare_constraint take a list of terms (rather than just variables) and key the constraint on all the variables contained in the given terms. In this way the problem above is not visible, since you don't have to represent that "list" of variables.
The CHR part of the language is still a bit rough (see for example #71), I'm very open to suggestions.

In this very specific case I would try something like this, but it is not a general solution (also untested)

tr X Y :- std.filter [X,Y] var VS, declare_constraint (tr X Y) VS.