### [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: diseq.diff

 Description
 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 ]