CODEWITHSUNDEEP
z3z3pysat-solverspysmt
user2754673
user2754673

Reputation: 459

Use different back-end solvers in Z3

I'm using Z3 Python interface to create formulas for my experiments. I'm then sending that formula to a Z3 solver. If I'm correct Z3 uses its own solver!

How to use a different SAT/SMT solver with Z3py?

The way I use to do it in CBMC (C bounded model checker): Run the program and spit an intermediate DIMAC representation (in a file) and then use that file as an input to other SAT solvers. Can I do similar things in Z3. Thank you.

Upvotes: 3

Views: 626

Answers (2)

alias
alias

Reputation: 30418

Sounds like you should really be using a solver agnostic SMT interface instead of Z3py. There have been several attempts to create such interfaces, with varying degrees of support for multiple solvers:

By no means this is an exhaustive list. I'm sure there are others as well, in various host languages, with varying degrees of maturity. Which one you should pick really depends on your host language preference, and the features afforded by each system; which may vary widely.

Upvotes: 4

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

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-compliant strings (some complicated variable declarations, e.g. some datatypes may be missing).

Z3py is a Z3-specific API (as the name indicates) it does not provide a way to use other SMT solvers.

Upvotes: 2

Related Questions