I have a SMT problem using weak constraints, but z3opt gives me a result which I don't understand. Here is the problem:
from z3 import *
solver = Optimize()
Inst, (n, x, y, z) = EnumSort('Inst', ['n', 'x', 'y', 'z'])
alive = Function('alive', Inst, BoolSort())
for i in [n, x, y, z]:
Basically, I have four elements n, x, y, z, and a function
determining whether an element is alive or not.
is always dead, and if
is alive, so should
. Then I say "every element should better not be alive", by four software constraints, each weighted 1. Finally I say
should be alive, with a weight 5. (Well, I know I sound twisted, but this is a simplification of our real problem:) ).
Now, I'm expecting a result telling me that
should be alive, with a penalty of 2, but what z3opt tells me is that every element should be not alive, and that has a penalty of 5, as I understand. Apparently, the result of z3opt
is not the optimised one.
I suspect it is the problem of killing
twice (once as hard constraint, and once soft), because if I change line 7 to
for i in [x,y,z]
, then the result becomes the one I expected...
I don't know if there is anything I misunderstood about the weak constraints, or if I should set up some configurations for z3opt (now I'm only using the default settings as you can see from the code above).
Thanks a lot!