CODEWITHSUNDEEP
z3smtz3py
stklik
stklik

Reputation: 844

z3py: equivalent to (get-objectives)

In Z3 I can call (get-objectives) to have a dump of the resulting weights. (e.g. here)

It prints something like this:

(objectives
 (aaa 1)
 (bbb 0)
)

In z3py however Optimize.objectives() prints a dump of the calculation for the objectives, not however the calculated weights, as seen here:

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

Is there a way how I can get the calculated weights? or the weight of a specific objective as in the standard z3?

Here is my example code:

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

Upvotes: 2

Views: 354

Answers (1)

alias
alias

Reputation: 30428

You can use the model to evaluate the objectives:

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

This yields:

sat
[1, 0]

Upvotes: 2

Related Questions