Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

spurious disequality constraints

Description

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

Environment

None

Activity

Show:

Nada Amin January 24, 2018 at 6:58 AM

There are 9 failures, failling into 4 categories (in order of importance):
1. subsumed constraint:
(

= (_0 5)), so the former should be removed if the later is present.
2. simplifiable constraint:
(

= _0 5).
3. redundant symmetric constraint:
(

= (_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 3)) should be shown more canonically as
(

= (_0 4)) switching the constraints.
This does not seem important.

Details

Assignee

Reporter

Approval

Incomplete

Patch

Code and Test

Priority

Created January 24, 2018 at 5:56 AM
Updated January 24, 2018 at 11:16 PM

Flag notifications