search

namin / clpsmt-miniKanren

CLP(SMT) on top of miniKanren
MIT License
35 stars 8 forks source link

A quick fix for `z3-driver.scm`. #3

Closed chansey97 closed 3 years ago

chansey97 commented 3 years ago

The following program returns the unexpected result and fails the test

(run* (q)
    (fresh (v1 v2)
      (z/ `(declare-const ,v1 Bool))
      (z/ `(declare-const ,v2 Bool))
      (== v1 v2)
      (== q v1)))

;; => (#f)

This patch fixes the problem, and return (#f #t):

(run* (q)
    (fresh (v1 v2)
      (z/ `(declare-const ,v1 Bool))
      (z/ `(declare-const ,v2 Bool))
      (== v1 v2)
      (== q v1)))

;; => (#f #t)

Note that

  1. This patch still cannot pass the test, because that test expects '(_.0). Nevertheless, returning (#f #t) is still a correct behavior, consider the following program in cKanren, i.e. CLP(FD):

    (run* (q)
   (fresh (v1 v2)
          (infd v1 '(0 1))
          (infd v2 '(0 1))
          (== v1 v2)
          (== q v1)))
;; => (0 1)

  2. This patch only be used for z3-driver.scm. z3-server.scm currently doesn't support boolean at all, since they don't encode #t and #f to smtlib format.

PS. I'm using z3-4.8.7.

namin commented 3 years ago

Thanks!