<< Back to previous view

[LOGIC-95] disequality Created: 04/Jan/13  Updated: 28/Jul/13  Resolved: 04/Jan/13

Status: Closed
Project: core.logic
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Defect Priority: Blocker
Reporter: Nada Amin Assignee: David Nolen
Resolution: Completed Votes: 0
Labels: None

Attachments: File diseq.diff    


This snippet wrongly succeeds with the result:

(([foo _0] :- (!= (foo _0))))

(run* [q]
      (nom/fresh [a b]
        (fresh [x y]
          (!= x y)
          (== (nom/tie a (nom/tie b [b y])) (nom/tie b (nom/tie a [a x])))
          (== x 'foo)
          (== [x y] q))))

Moving the disequality anywhere further down makes the snippet rightly fail.

Comment by Nada Amin [ 04/Jan/13 5:47 AM ]

An insight: if I remove the -relevant-var? protocol from !=c in core.logic, then this works and all other tests pass. Of course, this probably has performance applications, so thinking of alternatives.

Comment by Nada Amin [ 04/Jan/13 8:00 AM ]

The problem is not specific to nominal disequality. Here is the same bug with only core.logic:

(run* [q]
    (fresh [x y w z]
      (!= x y)
      (!= w z)
      (== z y)
      (== x 'foo)
      (== y 'foo)))

This should fail, because x == y == 'foo, but instead we get:

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

The problem is that var-rands takes the substitution map into account, while -relevant-var doesn't.

Comment by Nada Amin [ 04/Jan/13 8:31 AM ]

Another way disequality is broken:

(run* [q]
  (fresh [x y w z]
    (!= x [y])
    (== x ['foo])
    (== y 'foo)))

This snippet should fail, but instead returns '(_0). This is because y is not returned by recover-vars.

Comment by Nada Amin [ 04/Jan/13 11:18 AM ]

diseq.diff contains detailed commit message explaining the issues, fixes, and tests.

Comment by David Nolen [ 04/Jan/13 11:23 AM ]

fixed, http://github.com/clojure/core.logic/commit/fb489298417c643fdd03efbf6951e998e6821910

Generated at Tue Jan 16 04:14:29 CST 2018 using JIRA 4.4#649-r158309.