search

namin / clpsmt-miniKanren

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

Remove duplicate z3-server.rkt and z3-server.scm #7

Closed chansey97 closed 3 years ago

chansey97 commented 3 years ago

See https://github.com/namin/clpsmt-miniKanren/pull/4#issuecomment-890556214

This patch can run clpsmt-basic-tests.rkt normally (not fully pass, because old clpsmt-basic-tests.scm can not fully pass as well).

Other many tests can also run normally, but I do not commit those xx-tests.rkt. Need to review first.

Note: Compatibility both Scheme and Racket may have some problems when involving tabling.scm which redefined many procedures and macros in mk.scm. Racket's module system is not very compatible with Scheme's redefine.

chansey97 commented 3 years ago

mk.rkt now something like a composition root of clpsmt-minikanren and default use z3.

Users who want a different SMT backend (e.g. cvc4) need the following change:

  1. Copy the mk.rkt -> mk-cvc4.rkt
  2. In mk-cvc4.rkt, change (include "z3-driver.scm") to (include "cvc4-driver.scm").
  3. Use (require "mk-cvc4.rkt") instead of (require "mk.rkt") in your file.
namin commented 3 years ago

Thanks, are you using the slow mk instead of the faster mk?

chansey97 commented 3 years ago

Yes, I am using the clpsmt-miniKanren instead of the smt-assumptions of faster-miniKanren.

The smt-assumptions only uses z3-server.rkt which I did not modify. So they should not interfere with each other.

Note that there is a compilation error in the smt-assumptions, when run mk.rkt:

smt.scm:9:3: match: unbound identifier in: match

But that is just an old problem.

I think this patch can also be merged to smt-assumptions, but that's another repo.

BTW, I noticed that the clpsmt-miniKanren started from a canonical miniKanren implementation, which is relatively more gentle to me because there is a paper behind it. The faster-miniKanren started from miniKanren-with-symbolic-constraints which seems more complicated and no docs to explain (what the faster-miniKanren do is also very mysterious). So I haven't read it yet.

Anyway, I guess the enhancement of smt-assumptions can be easily ported to clpsmt-miniKanren and keep clpsmt-miniKanren clean.

Perhaps we can merge smt-assumptions to clpsmt-miniKanren? (May create a new branch? because current SMT hook mechanism may still useful, e.g. for debugging?)

What do you think about it?

namin commented 3 years ago

The changes in smt-assumptions are not so important. You can also use the simpler branch smt. However, using faster-mk is critically better than using the canonical mk, performance-wise. So I think you'd want to migrate to faster-mk eventually. There's no point in porting smt-assumptions back to canonical mk.

Thanks!

chansey97 commented 3 years ago

Yes, I'm reading faster-mk, it's great!

chansey97 commented 3 years ago

The changes in smt-assumptions are not so important.

After reading the smt-assumptions, I observed that the smt-assumptions has an advantage over the clpsmt-miniKanren.

That is the smt-assumptions can promote some miniKanren constraints to SMT assertions:

(== a b) -> (assert (= ,a ,b))
(=/= a b) -> (assert (not (= a b)))

This advantage will changes some behaviors.

For example, the ~diseq-1~ diseq-3 success in smt-assumptions, but diverges in current clpsmt-miniKanren.

I guess this advantage can also be patched to clpsmt-miniKanren or smt of faster-mk.

However, as you said

So I think you'd want to migrate to faster-mk eventually. There's no point in porting smt-assumptions back to canonical mk.

This reminds me of a question:

What is clpsmt-miniKanren current state? (I have created a new issue)

namin commented 3 years ago

Ah, interesting. I didn't think consciously of the promotion.

The main thing smt-assumptions does is not restart the solver as often by encoding assumptions to be switched on and off through check-sat-assuming. It's unclear whether this behavior results in a speed up.

chansey97 commented 3 years ago

Ah, interesting. I didn't think consciously of the promotion.

I'm sorry, the "constraint promotion" is the term that I invented myself. I don’t know whether there is a specific term for that purpose (Perhaps using "constraint conversion" or "constraint reification" is more precise?)

Another sorry is that, the diseq-1 is a wrong example, the correct one is diseq-3.

It was a typo and I have edited.