clojure - 具有 -ve 值的 Core.logic 有限域

Question

我不确定为什么使用 -5 作为域值之一时下面的代码不返回任何结果

user=> (run* [q] (infd q (domain -5 5)) (*fd q q 25))
()
user=> (run* [q] (infd q (domain 0 5)) (*fd q q 25))
(5)

注意：此代码指的是 core.logic 0.8.0 beta 中的行为。

Answer 1

目前 core.logic 0.8.0 测试版中根本不支持负值域。如果它起作用，那完全是偶然的。我不打算在不久的将来亲自添加对此的支持，尽管在 0.8.0 获得适当的版本之后会欢迎一个全面的补丁。

Answer 2

看起来*fd约束的实现只适用于所有正值的域。它基于乘积域的下限/上限除以右手因子域的上限/下限来计算左手因子的上限和下限，反之亦然。您可以看到将底片放入混合中将如何导致它不起作用：

 (run* [q]
   (fresh [r]
     (infd q (domain 1 2 3 4 5))
     (infd r (domain 20 25))
     (*fd q q r)))

 Product = [20..25], RHS = [1..5] => LHS = [20/5..25/1] = [4..25]

 (run* [q]
   (fresh [r]
     (infd q (domain -1 0 1 2 3 4 5))
     (infd r (domain 20 25))
     (*fd q q r)))

 Product = [20..25], RHS = [-1..5] => LHS = [20/5..25/-1] = [4..-25]

由于标志已关闭，因此 LHS 的区间最终无法满足，因为下限大于上限。

具有负值的有限域确实适用于+fd约束：

 (run* [q] (fresh [a b] (infd a b (domain -1 0 1)) (+fd a b 0) (== q [a b])))
 => ([-1 1] [0 0] [1 -1])