search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
182 stars 46 forks source link

Question about using custom z3 binary #288

Closed bobismijnnaam closed 1 year ago

bobismijnnaam commented 1 year ago

Hi, I have a question. Could java-smt be configured in such a way to use our own Z3 binary? Meaning, a real z3 binary, that you can use to check smt2 files. Because I fear that if we depend on java-smt, as well as its z3 support, we include Z3 into our tool twice; once through the binary we put in anyway (because of dependency requirements), and then once again for the java-smt library (through e.g. maven). I tried looking through the documentation but it seems java-smt only talks with Z3 through other libraries, which in turn seem to use the JNI...? This would imply that it's not possible for java-smt to use some random z3 binary provided by the user.

kfriedberger commented 1 year ago

JavaSMT does not provide support for direct SMTLIB-based interaction to SMT solvers, but only relies on native APIs. The possibilities of SMTLIB are limited and do not allow several operations in efficient manner, e.g., like formula rewriting or model evaluation. A native API is a better solution for these cases.

A user can provide a self-compiled Z3 library and Z3's own JNI bindings (i.e., not the binary executable itself, but libraries ending on ".so" on Linux, ".dll" on Windows, ".dylib" on MacOS) of any newer Git version of Z3. The API of Z3 is very stable (even across several releases of Z3) and should in most cases work well. In JavaSMT, the user needs to override the loading for the solver library, such that it uses the self-provided Z3 library.

bobismijnnaam commented 1 year ago

That clears it up for me, thank you for the concise explanation!