在 SWI-Prolog 中，以下查询给出了这个结果：
?- X mod 2 #= 0, X mod 2 #= 0.
X mod 2#=0,
X mod 2#=0.
虽然正确，但显然不需要第二个约束
同样：
?- dif(X,0), dif(X,0).
dif(X, 0),
dif(X, 0).
有没有办法避免这种重复的约束？ （显然，最正确的方法是不编写导致这种情况的代码，但这并不总是那么容易）。
【问题讨论】：
您可以避免发布冗余约束，也可以使用setof/3-like 构造删除它们。两者都是非常具体的实现。 SICStus 提供了用于此目的的最佳界面。 YAP 或 SWI 等其他实现或多或少地复制了该接口，省略了some essential parts。一个克服 SWI 缺陷的recent attempt 被拒绝了。
在 SICStus 中，您可以为此使用 frozen/2：
| ?- dif(X,0), frozen(X,Goal).
Goal = prolog:dif(X,0),
prolog:dif(X,0) ? ;
no
| ?- X mod 2#=0, frozen(X, Goal).
Goal = clpfd:(X in inf..sup,X mod 2#=0),
X mod 2#=0,
X in inf..sup ? ;
no
否则，copy_term/3 可能就足够了，前提是约束彼此之间没有太多的相互关联。
在这里，与call_residue_vars/1 和copy_term/3 一起使用的类似setof 的构造可能是最好的方法。同样，最初的实现是在 SICStus....
【讨论】：
仅对于dif/2，可以在不诉诸任何内部结构的情况下测试蕴涵：
difp(X,Y) :-
( X \= Y -> true
; dif(X, Y)
).
【讨论】：
由于 CLP 标记不是 SMT，因此很少有约束规划系统实现与分解定理证明中的因式分解相关的收缩。收缩是structural rule，它的内容如下，假设约束以否定形式存储在 (|-)/2 之前。
G, A, A |- B
------------ (Left-Contraction)
G, A |- B
我们还可以将其扩展到两个 A 可推导等价的情况。这很可能没有实施，因为它很昂贵。例如，Jekejeke Minlog 已经实现了 CLP(FD) 的收缩，即有限域。我们找到类似于来自 OP 的第一个查询的查询：
?- use_module(library(finite/clpfd)).
% 19 consults and 0 unloads in 829 ms.
Yes
?- Y+X*3 #= 2, 2-Y #= 3*X.
3*X #= -Y+2
?- X #< Y, Y-X #> 0.
X #=< Y-1
基本上我们分别归一化为 A1*X1+..+An*Xn #= B A1*X1+..+An*Xn #=
?- use_module(library(term/herbrand)).
% 2 consults and 0 unloads in 35 ms.
Yes
?- neq(X,0), neq(X,0).
neq(X, 0),
neq(X, 0)
dif/2 的收缩意味着通过在 dif/2 约束中定义的实例化来实现一种 (==)/2。即，我们需要在将 dif/2 约束中定义的变量和术语与约束存储中已经存在的所有其他 dif/2 约束配对之后应用递归测试。测试包容而不是收缩也会更有意义。
可能只有借助一些适当的索引技术来实现 dif/2 的收缩或包含。在Jekejeke Minlog 中，例如对于 CLP(FD)，我们在 X1 上建立索引，但我们还没有实现 CLP(H) 的一些索引。我们首先可能需要弄清楚的是 dif/2 约束的正常形式，另请参阅此问题 here。
【讨论】：