How can I convert an SMT model with optimization using z3 library to a .smt2 file recognized by different solvers like cvc4?

Question

I want to convert an SMT model written in python using z3 library in a file .smt2 to obtain a file which can be run from different solvers (for instance cvc4-solver). The problem is that my model makes optimization and when there is a conversion from z3 to smt2 file the instruction (maximize x) is not recognized from cvc4 (other SMT solver).
Here there is an example where is possible to understand better the problem:
Model:

o = Optimize()
i = Int('x')
o.add (i > 5)
o.add (i < 10)
o.maximize(i)
to_write= "(set-option :produce-models true)\n(set-info :status unknown)\n(set-logic QF_UFLIA)\n" 
to_write += o.sexpr() 
with open('/content/file1.smt2', "w") as f:   
   f.write(to_write)

Now the output of my file is:

(set-option :produce-models true)
(set-info :status unknown)
(set-logic QF_UFLIA)
(declare-fun x () Int)
(assert (> x 5))
(assert (< x 10))
(maximize x)
(check-sat)

If I run in CMD this file smt2, using z3, the solver returns sat, but instead if I use cvc4 the solver gives me this error

(error "Parse Error: /content/file1.smt2:7.9: expected SMT-LIBv2 command, got `maximize'.
  (maximize x)
   ^
")

cvc4 does not recognize the command (maximize x), there is another way to write this instruction for cvc4 solver ? Which are the SMT solvers that recognized the instructions maximize/minimize in an smt2 file?

I am expecting a file smt2 that can be used for each solver able to make optimization.

Answer 1

Not all SMT solvers do optimization. In fact, as far as I know, the only ones that support optimization are z3 and optimathsat: https://optimathsat.disi.unitn.it

In fact, optimization isn't really standardized by the SMTLib standard at all. (https://smtlib.cs.uiowa.edu)

So, for problems involving optimization, I'd recommend trying optimathsat as an alternative. As far as I know it understands the same optimization directives (i.e., maximize/minimize etc.), so the scripts will probably work out-of-the box. There might be some differences on how results are retrieved though, so feel free to ask specific questions if you run into trouble there.

Answer 2

Because of the fact that Optimisation Class is supported in Z3 and not currently in CVC5(or older versions of CVC), we can not export SMT-LIB2 format constraints for Optimisation and use in CVC SMT solver.

But as per recent comment by one of CVC5 developer, Optimisation Class and addition of softConstraint feature is under development and will be available in 6 months or so.

Link for ref and comment is attached: https://github.com/cvc5/cvc5/issues/10007#issuecomment-1715705938