z3py：相当于（获取目标）

Question

在 Z3 中，我可以调用 (get-objectives) 来转储生成的权重。（例如 here）

它打印出如下内容：

(objectives
 (aaa 1)
 (bbb 0)
)

然而在 z3py 中 Optimize.objectives() 打印 objective 的计算转储，而不是计算的权重，如下所示：

[If(a == 3, 0, 1), If(b == 3, 0, 1)]

有什么方法可以得到计算出的权重？或标准 z3 中特定 objective 的权重？

这是我的示例代码：

from z3 import *
a, b = Ints('a b')
s = Optimize()
s.add(3 <= a, a <= 10)
s.add(3 <= b, b <= 10)
s.add(a >= 2*b)
s.add_soft(a == 3, weight=1, id="aaa")
s.add_soft(b == 3, weight=1, id="bbb")
print(s.check())
print(s.model())
print(s.objectives())

Answer 1

您可以使用模型来评估目标：

m = s.model()
print [m.evaluate(o) for o in s.objectives()]

这产生：

sat
[1, 0]

z3py：相当于（获取目标）

z3py: equivalent to (get-objectives)

smt

z3

z3py