pysmt
Converting PySMT formulas to Z3Py ones
I wanna make use of the MaxSMT capabilities in Z3Py, and most of my codebase is on PySMT. Therefore, it is required that formulas are converted into Z3Py objects. However, I failed to find an approach to do such a conversion. Can this be done with PySMT API?
On the other hand, is it possible to do so with PySMT alone? I saw this issue but the code in optimization branch seems to be undocumented.
Hi @panda2134.
To convert formulae in Z3 is quite simple (also have a look here: https://github.com/pysmt/pysmt/blob/master/pysmt/test/test_solving.py#L290 ):
f = And(x, y) # your pysmt formula
with Solver(name='z3') as s:
z3_f = s.converter.convert(f) # z3_f is a z3 object ...
assert(z3.is_and(z3_f)) # ... and can be used with the Z3 API
The optimization branch provides support for MaxSMT and OMT across solvers (Z3 and MathSAT at the moment), but is still in alpha quality. Let me know if you want to try it out so that I can give you pointers!
To convert formulae in Z3 is quite simple
Thanks for this, I'll definitely give it a try.
The
optimizationbranch provides support for MaxSMT and OMT across solvers (Z3 and MathSAT at the moment), but is still in alpha quality. Let me know if you want to try it out so that I can give you pointers!
I'm looking forward to some hints! Anyway, a solver-agnostic way of calling MaxSMT seems way better than invoking Z3Py directly.
The
optimizationbranch provides support for MaxSMT and OMT across solvers (Z3 and MathSAT at the moment), but is still in alpha quality. Let me know if you want to try it out so that I can give you pointers!
Hi! I wonder if you could provide me some hint on the optimization branch. I'm really looking forward to using PySMT to call MaxSMT solvers.
Hi @panda2134,
sorry for the dealy. Yes, the branch is a bit orphan at the moment, but we worked on MaxSMT here: https://github.com/pysmt/pysmt/pull/678
The status of the code is not great as the base branch advanced a bit and also master is not aligned, but the basic functionalities and interfaces should be there. In particular have a look at goal.py to specify the optimization objective and to the tests to see how to use it.
Should you be willing, feel free to take this code and update/fix/work on the PR! I and @marcogario can assist if you have specific questions/ need directions!