CODEWITHSUNDEEP
z3smtz3py
Madalina Erascu
Madalina Erascu

Reputation: 87

to_smt2() for Optimize class

Is there a function to_smt2() for Optimize class which does the same thing as the function with the same name in Solver class, that us create an smt-lib file with the optimization problem. Thanks!

Upvotes: 0

Views: 307

Answers (1)

alias
alias

Reputation: 30450

The following works for me:

from z3 import *

o = Optimize ()
i = Int('x')
o.add (i > 5)
o.add (i < 10)
o.maximize(i)
print o.sexpr()
print o.check()
print o.model()

This prints:

$ python a.py
(declare-fun x () Int)
(assert (> x 5))
(assert (< x 10))
(maximize x)
(check-sat)

sat
[x = 9]

Note that maximize is not an SMTLib function, but a z3 extension.

Upvotes: 1

Related Questions