z3py：相当于（get-objectives）

Question

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

它会打印如下内容：

(objectives
 (aaa 1)
 (bbb 0)
)

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

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

有没有办法获得计算出的权重？还是标准 z3 中特定目标的权重？

这是我的示例代码：

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]