# core.logic

## pruning of unsatisfiable non-ground disequalities

### Details

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

### Description

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?

### Attachments

1. logic-100.diff
07/Jan/13 7:25 AM
2 kB
2. logic-100-rebase.diff
07/Jan/13 10:50 AM
3 kB

### Activity

Hide
David Nolen added a comment -
Hide

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

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

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

Vote (0)
Watch (0)

• Created:
Updated:
Resolved: