to_smt2() 用于优化 class
to_smt2() for Optimize class
Optimize class 是否有一个函数 to_smt2() 与 Solver class 中的同名函数做同样的事情，我们创建一个 smt-lib包含优化问题的文件。
谢谢！
以下对我有用：
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 扩展。
Optimize class 是否有一个函数 to_smt2() 与 Solver class 中的同名函数做同样的事情，我们创建一个 smt-lib包含优化问题的文件。 谢谢！
以下对我有用：
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 扩展。