clpsmt-miniKanren icon indicating copy to clipboard operation
clpsmt-miniKanren copied to clipboard

Confirm a bug about duplicate answers

Open chansey97 opened this issue 2 years ago • 0 comments

See the following program:

(run* (q)
      (z/ `(declare-const ,q Int))
      (z/assert `(and (>= ,q 1) (<= ,q 2)))
      (fresh (x)
             (z/ `(declare-const ,x Int))
             (z/assert `(and (>= ,x 1) (<= ,x 3)))))

;; '(1 2 2 2 1 1)  <---- returns duplicate answers.

The reason is that the current implementation find alternative answers by negating all the symbols' interpretation in that model, not just the relevant symbols which we want to reify.

cKanren has no this problem:

(run* (q)
      (infd q (range 1 2))
      (fresh (x)
             (infd x (range 1 3))))
'(1 2)

We must confirm that indeed a bug before fix it (or in the next version) because the default miniKanren (no tabling) allows duplicate answers.

chansey97 avatar Aug 22 '21 12:08 chansey97