### [LOGIC-100] pruning of unsatisfiable non-ground disequalities Created: 07/Jan/13  Updated: 28/Jul/13  Resolved: 07/Jan/13

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

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

 Attachments: logic-100.diff     logic-100-rebase.diff

 Description
 Not sure whether we actually want to do anything about this. When running this snippet, ```(run* [q] (fresh [a b] (== q [a b]) (!= a q)))``` we get the result: `(([_0 _1] :- (!= (_0 [_0 _1]))))` The reified != constraint is arguably spurious, because of the occurs-check. Even if we instantiate the a: ```(run* [q] (fresh [a b] (== q [a b]) (!= a q) (== a 1)))``` we get the result: `(([1 _0] :- (!= (1 [1 _0]))))` while there is no way the != constraint can be satisfied. Thoughts?

 Comment by Nada Amin [ 07/Jan/13 7:25 AM ] logic-100.diff contains a hackish fix: use unify instead of not= to deal with non-ground terms. Also, don't add the constraint if you know that some pairs cannot be unified upfront (this is needed b/c disunify and unify are not consistent wrt occurs-check). Comment by David Nolen [ 07/Jan/13 8:37 AM ] Well it is possible to disable occurs-check. Why can't we just use the existing occurs-check fn to do this work? Comment by Nada Amin [ 07/Jan/13 9:35 AM ] There are two issues. The first one is that it's too conservative to just prune != constraints by checking that ground term pairs are not=, because [1 w] and [2 z] should also be pruned. Here is an extra test case illustrating this: ```(deftest test-logic-100-disequality-3 (is (= (run* [q] (fresh [x y w z] (== x [1 w]) (== y [2 z]) (!= x y))) '(_0))) (is (= (run* [q] (fresh [x y w z] (!= x y) (== x [1 w]) (== y [2 z]))) '(_0))))``` On master, the second one fails b/c it has the extra constraint `(!= ([1 _1] [2 _2]))` which we ought to prune. The second issue is that disunify does not take the occurs-check into account, so it can create a !=c that is not considered runnable, but if run, would be rightly pruned by the new unify clause (if the occurs-check is enabled). Comment by David Nolen [ 07/Jan/13 10:39 AM ] Ok, makes sense. Can we get a new patch using master. This one doesn't apply anymore. Thanks! Comment by Nada Amin [ 07/Jan/13 10:50 AM ] logic-100-rebase.diff is a new patch against master. I also added the extra tests discussed above. Comment by David Nolen [ 07/Jan/13 11:00 AM ]