# core.logic

## disequality

### Details

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

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

### Attachments

1. diseq.diff
04/Jan/13 11:18 AM
4 kB

### Activity

Hide
David Nolen added a comment -
Hide

diseq.diff contains detailed commit message explaining the issues, fixes, and tests.

Show
Nada Amin added a comment - diseq.diff contains detailed commit message explaining the issues, fixes, and tests.
Hide

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.

Show
```(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.
Hide

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.

Show
Nada Amin added a comment - 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.
Hide

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.

Show
Nada Amin added a comment - 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.

Vote (0)
Watch (0)

• Created:
Updated:
Resolved: