Creating a bidirectional rule in CHR and CLPFD

As an example. Suppose that everything which is red has value 5. I write the following:

:- use_module(library(chr)).
:- use_module(library(clpfd)).

:- chr_type color ---> red ; blue.

:- chr_constraint hasColor(?any, ?color).
:- chr_constraint hasValue(?any, ?int).

hasColor(Thing, red) <=> hasValue(Thing, X), X #= 5.
hasColor(Thing, blue) <=> hasValue(Thing, X), X #\= 5.

hasColor(moose, red) correctly produces the inferenced output hasColor(moose, red), hasValue(moose, 5).

However, I would then like the inference to work the other way too; to specify that if something has value 5, it must be red. Currently, hasValue(moose, 5) is accepted as a constraint but produces no inference. But adding the rule:

hasValue(Thing, 5) ==> hasColor(Thing, red).

causes any invocation of hasValue(moose, 5) to lock up completely and stack overflow, apparently causing an infinite loop, even though ==> states that the rule “calls its body exactly once”.

I appreciate that I have not stated that a Thing can have only one color or value (I am not sure how I would do this), but repeatedly adding the constraint that moose is red and has value 5 should surely not change the constraint set.

How can I enable the system to perform this inference correctly in both directions?

The key trick is to add an idempotence rule.

hasColor(A,B) \ hasColor(A,B) <=> true.
hasValue(A,B) \ hasValue(A,B) <=> true.

So if you infer a thing twice, the second one is deleted and the system stops firing rules. Then you should be able to add all your rules.

So to be sure, you mean to code that all red things have value 5, blue things do not have 5, all things valued 5 are red.

To state a thing can’t have more than one value, you can do like this:

hasValue(Thing, A) \ hasValue(Thing, B) ==> A = B.

If A and B are defined and the same, the second will be erased. If two different values are assigned, this will fail and backtrack.

1 Like