<< Back to previous view

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

Status: Resolved
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: File logic-100.diff     File 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?

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

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

Generated at Thu Jun 20 00:19:47 CDT 2013 using JIRA 4.4#649-r158309.