I am trying to optimize an expression that consists of bitvectors in Z3 (the code runs in e.g. https://rise4fun.com/Z3/tutorial/optimization):
(declare-const x (_ BitVec 32))
(assert (bvslt x #x00000008))
(maximize x)
(check-sat)
(get-objectives)
The result I get is:
sat
(objectives
(x 4294967295)
)
which is the maximum int 0xffffffff for 32 bits, which would be signed -1. However, I want to get the signed maximum, i.e. 7. Is there any way to do that in Z3 (apart from making multiple calls to Z3 with different constraints (i.e b&b) as in CVC4 minimize/maximize model optimization)? Does anyone know any other solver (preferably using smtlibv2 input) to do that?
In my experience, the easiest thing to do is to shift the number up appropriately. That is, maximizing (or minimizing) an n-bit signed bit-vector x is equivalent to doing the same on the n-bit unsigned bit-vector x + 2n − 1. That is, just before you call maximize or minimize add 2n-1 to the amount you're trying to optimize, thus making the original value range over [−2n − 1, 2n − 1) instead of what the optimizer will see as [0, 2n).
You can see the discussion in the z3 github tracker from 2017 that concludes the same: https://github.com/Z3Prover/z3/issues/1339