clpsmt-miniKanren
clpsmt-miniKanren copied to clipboard
Confirm a bug about duplicate answers
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.