# spurious disequality constraints

0 votes

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

## 2 Answers

0 votes
by

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.

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