使用多个随机数的一次性约束可能会运行多次

Question

以下是使用 fixc 的两个示例

`
(run* [q]
(fresh [x y]

(fixc [x y]
  (fn [[x y] a _] (!= x 1))
  (fn [[x y] a] (= (walk a x) (walk a y)))
  '...)
(== x y)))

(run* [q]
(fresh [x y c d]

(fixc [x y]
  (fn [[x y] a _] (!= x y))
  (fn [[x y] a] (or (not (lvar? (walk a x))) (not (lvar? (walk a y)))))
  '...)
(== [x y] [[c] [d]])))

`

在每个示例中，约束 != 被特定化两次，表明 fixc 约束确实运行了两次。

Answer 1

评论者：dnolen

对于第一个示例，我在 master 上看到以下结果

((_0 :- (!= (_1 1))))

这是您看到的结果吗？由于 x 并非答案的一部分，我怀疑是否应该显示这些约束？

Answer 2

评论者：namin

我通过将约束集合特定化来更改了复现器，因此现在只有一个结果。因此，我的说明现在已经过时，但问题仍然存在。过滤掉不相关约束是一个单独的问题，我同意应该这样做（我尝试对规范约束这样做）。

Answer 3

参考：[https://clojure.atlassian.net/browse/LOGIC-117](https://clojure.atlassian.net/browse/LOGIC-117)（由 namin 报告）