core.logic

pruning of unsatisfiable non-ground disequalities

Details

  • Type: Defect Defect
  • Status: Resolved Resolved
  • Priority: Minor Minor
  • Resolution: Completed
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • Labels:
    None

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?

Activity

Ascending order - Click to sort in descending order
Hide
Permalink
Nada Amin added a comment -

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).

Show
Nada Amin added a comment - 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).
Nada Amin made changes -
Field Original Value New Value
Attachment logic-100.diff [ 11794 ]
Hide
Permalink
David Nolen added a comment - - edited

Well it is possible to disable occurs-check. Why can't we just use the existing occurs-check fn to do this work?

Show
David Nolen added a comment - - edited Well it is possible to disable occurs-check. Why can't we just use the existing occurs-check fn to do this work?
Hide
Permalink
Nada Amin added a comment -

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).

Show
Nada Amin added a comment - 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).
Hide
Permalink
David Nolen added a comment - - edited

Ok, makes sense. Can we get a new patch using master. This one doesn't apply anymore. Thanks!

Show
David Nolen added a comment - - edited Ok, makes sense. Can we get a new patch using master. This one doesn't apply anymore. Thanks!
Hide
Permalink
Nada Amin added a comment -

logic-100-rebase.diff is a new patch against master. I also added the extra tests discussed above.

Show
Nada Amin added a comment - logic-100-rebase.diff is a new patch against master. I also added the extra tests discussed above.
Nada Amin made changes -
Attachment logic-100-rebase.diff [ 11796 ]
David Nolen made changes -
Resolution Completed [ 1 ]
Status Open [ 1 ] Resolved [ 5 ]

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved:
Atlassian JIRA (v4.4#649-r158309) | Report a problem
Powered by a free Atlassian JIRA open source license for Clojure. Try JIRA - bug tracking software for your team.