Use other built-in solvers in Z3
I am using the Z3 Python interface to create formulas for my experiments. Then I send this formula to the Z3 solver. If I'm right, Z3 uses its own solver!
How do I use a different SAT / SMT solver with Z3py?
The way I use it in CBMC (C constrained model validation): Run the program and align the DIMAC intermediate representation (in a file) and then use that file as input for other SAT solvers. Can I do similar things in Z3. Thank.
source to share
It looks like you really should be using the incompatible SMT interface instead of the Z3py interface. Several attempts have been made to create such interfaces with varying degrees of support for multiple solvers:
-
https://github.com/pysmt/pysmt is a crucial Python agnostic API for SMT solvers. I haven't used it myself, but it sounds promising, especially if you want Python to be your top-level API.
-
https://github.com/sosy-lab/java-smt is a similar project that uses Java as the host language.
-
http://leventerkok.github.io/sbv/ is my own attempt to provide a solver agnostic API for using SMT solvers which is written in Haskell.
This is not an exhaustive list. I'm sure there are others, in different languages, with varying degrees of maturity. Which one you should choose really depends on your language preference and the particulars provided by each system; which can vary widely.
source to share
All SMT solvers support the SMT2 input format, so you can do the same with Z3 and other SMT solvers. Z3py can translate Solver and Goal objects to SMT2 compatible strings (some complex variable declarations, for example, some data types may be missing).
Z3py is a Z3 specific API (as the name suggests), it does not provide a way to use other SMT solvers.
source to share