Some test cases failed, and which z3 version should I use?

[chansey97]

Hi,

I am trying to use clpsmt-miniKanren for constraint logic programming, it's great work!

But I am not sure which z3 version should I use?

I initially used z3-4.8.12, but failed. The reason is that clpsmt-miniKanren assumes the result model s-exp has a model in the top, but z3-4.8.12 has no this model.

`(model   ; <== z3-4.8.12 no this `model`
   (define-fun ,vars () ,typs ,vals)
   ...)

So I switched to an older version.

I currently use z3-4.8.7, it can pass many test cases, but some of them still failed.

> (load "mk.scm")
> (load "z3-server.scm")
> (load "test-check.scm")

> (load "clpsmt-basic-tests.scm")
Testing "counters"
Testing "declare-idempotent"
Failed: (run* (q) (fresh (v1 v2) (z/ `(declare-const ,v1 Bool)) (z/ `(declare-const ,v2 Bool)) (== v1 v2) (== q v1)))
Expected: (_.0)
Computed: (#f)
Testing "inf-smt-ans-1"
Testing "inf-smt-ans-2"
Testing "1"
Testing "2"
Testing "3"
Testing "4"
Testing "5"
Failed: (run 2 (f) (z/ `(declare-fun ,f (Int) Int)) (z/assert `(= 1 (,f 1))) (z/assert `(= 0 (,f 0))))
Expected: ((lambda (x!0) (ite (= x!0 1) 1 (ite (= x!0 0) 0 1))))
Computed: ((lambda (x!0) (ite (= x!0 0) 0 1)))
Testing "6"

> (load "clpsmt-tests.scm")
Testing "faco-7"
Testing "faco-backwards-2"
Testing "faco-backwards-720"
Testing "evalo-1"
Testing "evalo-backwards-1"
Testing "evalo-bop-1"
Testing "evalo-2"
Testing "evalo-fac-6"
Testing "evalo-fac-9"
Testing "evalo-backwards-fac-6"
Testing "evalo-backwards-fac-quoted-6"
Testing "evalo-backwards-fac-9"
Testing "evalo-backwards-fac-quoted-9"
Testing "evalo-fac-table"
Testing "evalo-fac-synthesis-hole-0"
Testing "evalo-fac-synthesis-hole-1"
read-sat: unknown
read-sat: unknown
Testing "evalo-fac-synthesis-hole-1-reversed-examples"
read-sat: unknown
read-sat: unknown
Testing "evalo-fac-synthesis-hole-2"
Testing "evalo-fac-synthesis-hole-3"
Testing "evalo-fac-synthesis-hole-4"
read-sat: unknown
read-sat: unknown
Testing "evalo-division-using-multiplication-0"
Testing "evalo-division-using-multiplication-1"
Testing "evalo-division-using-multiplication-2"
Testing "evalo-many-0"
Failed: (run* (q) (fresh (x y) (evalo `(* ',x ',y) 6) (== q (list x y))))
Expected: ((6 1) (1 6) (-1 -6) (-2 -3) (-3 -2) (-6 -1) (2 3) (3 2))
Computed: ((6 1) (2 3) (1 6) (3 2) (-2 -3) (-6 -1) (-1 -6) (-3 -2))
Testing "many-1"
Failed: (run* (q) (fresh (x y) (evalo `(+ (* ',x ',y) (* ',x ',y)) 6) (== q (list x y))))
Expected: ((3 1) (1 3) (-1 -3) (-3 -1))
Computed: ((3 1) (1 3) (-3 -1) (-1 -3))
Testing "many-2"
Failed: (run* (q) (fresh (x y) (evalo `(* (* ',x ',y) 2) 6) (== q (list x y))))
Expected: ((3 1) (1 3) (-1 -3) (-3 -1))
Computed: ((3 1) (1 3) (-3 -1) (-1 -3))

It seems that there are two kinds of failure:

1. z3 version relevant
   clpsmt-basic-tests.scm - Testing "5"
   clpsmt-tests.scm - Testing "evalo-many-0"
   clpsmt-tests.scm - Testing "many-1"
   clpsmt-tests.scm - Testing "many-2"
   clpsmt-tests.scm - all other read-sat: unknown cases.

2. z3 version irrelevant
   clpsmt-basic-tests.scm - Testing "declare-idempotent"

Could you tell me which z3 version should I use?

Thanks.

My environment:

Windows 7,
Chez Scheme Version 9.5,
z3-4.8.7,
clpsmt-miniKanren-master (4fa74fb)

PS. I used z3-server.scm instead of z3-driver.scm, becasue z3-driver.scm doesn't work in windows 7. Is there way to workaround? BTW, does clpsmt-miniKanren support Racket? I saw the source code mixed .scm and .rkt, but all the test cases use .scm and load. So I don't know whether clpsmt-miniKanren is currently compatible with Racket.

[namin]

Hi Siyuan,

Thanks for your interest and kind words.

I can't reproduce the issue with model not being there anymore, I am using Z3 version 4.8.12.

Some of the tests might not have been updated with the latest version of Z3.

You can also get a much faster experience if you use a branch of faster-miniKanren. For example: https://github.com/namin/faster-miniKanren/blob/smt-assumptions/smt-tests.scm

At some point, we had a version compatible with Racket. It shouldn't be too hard to revive it and have a common base for both the Scheme and Racket version as is the case in faster-miniKanren.

I am curious to hear more about how you plan to use clpsmt-miniKanren.

[chansey97]

I can't reproduce the issue with model not being there anymore, I am using Z3 version 4.8.12.

It's very strange.

You can reproduce this issue as following:

1. z3-4.8.12
   

2. z3-4.8.7
   

You can see that z3-4.8.7 has a model at the top of the result of (get-model) and this is consistent with z3-server.scm#L66, (cdr m). So the current clpsmt-miniKanren can run well in z3-4.8.7 (at least pass many tests) .

However, z3-4.8.12 lacks this model, so it fails.

[chansey97]

At some point, we had a version compatible with Racket. It shouldn't be too hard to revive it and have a common base for both the Scheme and Racket version as is the case in faster-miniKanren.

I tried z3-server.rkt in Racket. It complained:

?: literal data is not allowed;
 no #%datum syntax transformer is bound in: 0

at the (eval r).

I can workaround this issue by replacing (eval r) with r, but I am not sure whether it will affect the result?

Racket version v8.0 [bc].

[chansey97]

I am curious to hear more about how you plan to use clpsmt-miniKanren.

Mainly to learn how logic programming combines with SMT solver.

I am self-learning Constraint Logic Programming and Satisfiability Modulo Theories. In Constraint Logic Programming, it is a bit tricky to implement an common efficient domain-specific constraint, e.g. CLP(FD), CLP(Z), CLP(R), CLP(Set), etc. But if we can use an SMT solver as backend, they will be out of the box. It seems that CLP and SMT are very similar, even though they use different theoretical frameworks (Consider CLP(X) vs DPLL(T)).

Another reason is that I'd like to collect some applications for miniKanren variants (especially about program synthesis).

miniKanren has a lot of variants. Different variants have different features and restrictions. (Unfortunately, there is no all-in-one package.) clpsmt-miniKanren is one of such variants. For example, we can use miniKanren to do symbolic execution, but standard miniKanren with symbolic constraints does not support Integer arithmetic. By clpsmt-miniKanren, we can get CLP(Z) out of the box. That is why I said it is great! (Oleg numeral can be extended to negative, but it is another story).

PS. I am also learning rosette. Comparing rosette and miniKanren for program synthesis is an interesting experience as well.

[namin]

I can't reproduce the issue with model not being there anymore, I am using Z3 version 4.8.12.

It's very strange.

You can reproduce this issue as following:

1. z3-4.8.12
   
2. z3-4.8.7
   

You can see that z3-4.8.7 has a model at the top of the result of (get-model) and this is consistent with z3-server.scm#L66, (cdr m). So the current clpsmt-miniKanren can run well in z3-4.8.7 (at least pass many tests) .

However, z3-4.8.12 lacks this model, so it fails.

OK, I guess the code will ignore the first constraint in the model.
You can change that behavior by removing the cdr here: https://github.com/namin/clpsmt-miniKanren/blob/master/z3-server.scm#L66

[namin]

Sorry, the codebase is a bit rotted. We'll try to find some time to clean it up and bring it up to date. If you'd like to help, that would be great.

[chansey97]

Hi Nada,

There is test case that I am not sure whether the current clpsmt-miniKanren's behavior correct:

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

;; => (#f)

The computed value is (#f), but the expected value (_.0).

Does this mean that there is a bug in the current clpsmt-miniKanren? (BTW, I think the 3rd possible candidate result is (#t #f).)

I don't know which one should be the correct behavior when we combine with SMT solver?

Thanks.

[namin]

Hi Nada,

There is test case that I am not sure whether the current clpsmt-miniKanren's behavior correct:

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

;; => (#f)

The computed value is (#f), but the expected value (_.0).

Does this mean that there is a bug in the current clpsmt-miniKanren? (BTW, I think the 3rd possible candidate result is (#t #f).)

I don't know which one should be the correct behavior when we combine with SMT solver?

Thanks.

Thanks, this is strange. You can enable logging here: https://github.com/namin/clpsmt-miniKanren/blob/master/z3-server.scm#L4 to see what's going on. If you can debug this, that would be great. If not, I'll take a look next month when I'll have more time.

[chansey97]

It would be nice, if you can write a paper explains how clpsmt-miniKanren be implemented, e.g. how == promoted to (z/assert (= ,a ,b)), compatible with old symbolic-constraints, constraints subsumption, how SMT combined with minikanren's interleave complete search, etc : )

BTW, You have searched the internet for "SMT and constraint logic programming". There are very few resources about how SMT and CLP connect. It seems that clpsmt-miniKanren is the first opensource project done this idea (bring SMT to CLP). That's a really cool stuff.

[namin]

I just added you to an old repo with work in progress about the project and its implementation. Eventually, we could turn this into a paper.

[chansey97]

I just added you to an old repo with work in progress about the project and its implementation.

Hi, Nada,

I'm sorry...

I don't quite understand the meaning of this sentence.

What do you mean by "old repo" ? Could you explain further?

Thanks.

[namin]

You should have gotten access to the smt-pearl repo.

[chansey97]

Thank you.

But is the smt-pearl under your github account? Or just a branch?

I can't find this repo. Is there a link for it?

[namin]

I just emailed you the repo URL.