to_smt2() 用于优化类

Question

Optimize 类是否有一个函数 to_smt2()，它与 ​​Solver 类中的同名函数做同样的事情，我们创建一个包含优化问题的 smt-lib 文件。 谢谢！

Answer 1

以下对我有用：

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()

打印出来：

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

sat
[x = 9]

请注意，maximize 不是 SMTLib 函数，而是 z3 扩展。