diseq.diff
[LOGIC-95] disequality Created: 04/Jan/13 Updated: 04/Jan/13 Resolved: 04/Jan/13 |
|
| Status: | Resolved |
| 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. |
| Comments |
| 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 |