SWI-Prolog中CHR框架的neq约束运行不符合预期如何解决？

问题原因 #

你原有代码的问题出在第二条规则的守卫条件X \= Y不符合CHR约束延迟触发的要求：Prolog原生的\=仅会在调用时判断当前两个项是否不可合一，当两个参数都是未绑定自由变量时，SWI-Prolog的CHR实现对该守卫的判断逻辑会提前触发规则，导致本应保留的neq/2约束被提前移除，最终出现不符合预期的运行结果。

修改方案 #

将第二条规则的守卫替换为CHR标准提供的?=谓词，该谓词仅当两个参数的绑定状态已经可以明确判断是否可合一时才会返回真，确保变量未绑定的情况下neq/2约束会被保留：

:- use_module(library(chr)).

:- chr_constraint neq/2.

neq(X,X) <=> fail.
neq(X,Y) <=> X ?= Y | X \= Y.

运行验证 #

修改后执行测试查询即可得到和教程一致的结果：

?- neq(A,B).
neq(A,B).

?- neq(A,B), A = B.
false.

如果需要兼容更老的CHR实现，也可以把第二条规则的守卫写为显式的ground判断，仅当两个参数都实例化后再执行不等校验：

neq(X,Y) <=> ground(X), ground(Y), X \= Y | true.

内容的提问来源于stack exchange，提问作者chansey