spurious disequality constraints

Question

As reported by 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)))))))

`

I have a suggested fix here: https://github.com/clojure/core.logic/compare/master...namin:fix-for-meta?expand=1
but might be worth ensuring that other test cases from mk also work as intended.

Will Byrd suggests converting this file of tests:
https://github.com/webyrd/faster-miniKanren/blob/master/disequality-tests.scm

Answer 1

Comment made by: namin

There are 9 failures, failling into 4 categories (in order of importance):
1. subsumed constraint:
(!= (_1 6) (_0 5)) is subsumed by (!= (_0 5)), so the former should be removed if the later is present.
2. simplifiable constraint:
(!= ((link: _0 1) (link: 5 1))) should simplify to (!= _0 5).
3. redundant symmetric constraint:
(!= (_1 _0)) and (!= (_0 _1)) are redundant, and only the later should be kept.
This is a special case of 1.
4. benign reordering:
(!= (_1 _0)) should be shown more canonically as
(!= (_0 _1)) switching the order of operands, and
(!= (_0 _4)) (!= (_0 3)) should be shown more canonically as
(!= (_0 _3)) (!= (_0 4)) switching the constraints.
This does not seem important.

Answer 2

Reference: https://clojure.atlassian.net/browse/LOGIC-186 (reported by namin)