假不等式约束

Question

由 Will Byrd 报告

`
(is (=

 (run* [q]
   (fresh [x y]
     (!= (list x y) q)))
 ;; Simplified answer should just be:
 ;;
 ;; (_0)
 ;;
 ;; There is no way to violate this constraint, since neither
 ;; _1 nor _2 is reified. Both would need to be reified to be
 ;; able to violate the constraint.
 '((_0 :- (!= (_0 (_1 _2)))))))

`

在此处提出了一种修复建议： https://github.com/clojure/core.logic/compare/master...namin:fix-for-meta?expand=1
但是也可能值得确保 mk 中的其他测试用例也按预期工作。

Will Byrd 建议，将此测试文件转换为以下格式
https://github.com/webyrd/faster-miniKanren/blob/master/disequality-tests.scm

Answer 1

评论者：namin

共有 9 个失败的测试用例，分为 4 个类别（按重要性排序）
1. 被包含的约束
(!= (_1 6) (_0 5)) 被包含在 (!= (_0 5)) 中，因此如果在后者存在的情况下，应删除前者。
2. 可简化约束
(!= ((link: _0 1) (link: 5 1))) 应简化为 (!= _0 5)。
3. 冗余对称约束
(!= (_1 _0)) 和 (!= (_0 _1)) 是冗余的，并且只需保留后者。
这是 1 的一个特殊情况。
4. 良性排序
(!= (_1 _0)) 应更规范地表示为
交换操作数的顺序和
(!= (_0 _4)) (!= (_0 3)) 应更规范地表示为
交换约束。
这似乎并不重要。

Answer 2

参考：https://clojure.atlassian.net/browse/LOGIC-186（由 namin 报告）