core.logic

pruning of unsatisfiable non-ground disequalities

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • 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

Nada Amin made changes -
Field Original Value New Value
Attachment logic-100.diff [ 11794 ]
Nada Amin made changes -
Attachment logic-100-rebase.diff [ 11796 ]
David Nolen made changes -
Resolution Completed [ 1 ]
Status Open [ 1 ] Resolved [ 5 ]
David Nolen made changes -
Status Resolved [ 5 ] Closed [ 6 ]

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved: