如何动态重写CLP(FD)约束以帮助实现

Question

我的问题与这个(现在已有1年历史)关于CLP(FD)计划中的具体化问题的帖子有关:链接

我提供给SWI引擎的prolog文件是基于用户可以使用另一个应用程序添加/编辑/删除的一些数据(即之后调用引擎的相同数据),即时编写的.

我想检测一些特殊情况来动态重写约束,以帮助"引擎"找到最小的可能域.一个例子 :

 constr(X,Y,Z) :-
   X in {1,2,3,4,5,6,7},
   Y in {3,5,7},
   Z in {1,2},
   ((X #= 3)) #==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)),
   ((Z #= 1)) #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)).

如果我打电话constr(3,Y,Z).,我得到Z #= 1或Z #= 2.

一种解决方案是自动替换最后两行

((X #= 3)) #==> T, 
((Z #= 1)) #<==> T, 
T #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)).

有了这个,我得到了 Z #= 1.

麻烦的是我可以这样:

   ((X #= 3)) #==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)),
   ((Z #= 1)) #<==> ((Y mod 7 #= 0) #\/ (Y mod 3 #= 0)).

怎么检测到这个？Prolog引擎可以帮助我这样做吗？我以为我可以通过编译变量以编程方式替换每个右操作数:

   ((X #= 3)) #==> J,
   ((Z #= 1)) #<==> K,
   J #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)),
   K #<==> ((Y mod 7 #= 0) #\/ (Y mod 3 #= 0)).

但在这种情况下会出现同样的"具体化"问题.

谢谢你的帮助.