maximize prefers negative signed integers over positive ones

[andersk]

λ> optimize Lexicographic $ maximize "m" =<< sInt8 "n"
Optimal model:
  n = -1 :: Int8
  m = -1 :: Int8

Expected 127.

[LeventErkok]

Thanks for the report! Indeed there seems to be some corner cases that are problematic. I traced these back to issues with Z3 and reported two issues:

1. How to communicate "signedness" to optimization? Z3Prover/z3#1339
2. Optimization seems to confuse the sign Z3Prover/z3#1340

Based on the resolution to these, we might have to do some modifications to SBV to resolve the issue you reported.

[LeventErkok]

Here's another problematic case:

Prelude Data.SBV> optimize Lexicographic $ \x -> do constrain (x .> (-20));  maximize "x" (x::SInt8)
Optimal model:
  s0 = -1 :: Int8
  x  = -1 :: Int8

which is wrong. Interestingly, the following works:

Prelude Data.SBV> optimize Lexicographic $ \x -> do constrain (x .> 20);  maximize "x" (x::SInt8)
Optimal model:
  s0 = 127 :: Int8
  x  = 127 :: Int8

I'd say SBV is doing the right thing here and Z3 is being confused, but I'd like to see their response first.

[LeventErkok]

Based on the discussion at the Z3 github, we need to fix this by "adjusting" the goal by adding 2^{n-1} when we have a signed type.

Unfortunately this is not as easy as it sounds, since we need to make the objective parser understand this addition as well; but it shouldn't be too hard to implement. Hopefully sometime this weekend.

[LeventErkok]

@andersk The fix is committed. Would be great if you can do some independent testing to make sure all is well, before a new hackage release goes out. Thanks.

[andersk]

Seems to work.

[LeventErkok]

Cool. Thanks for the report.

[LeventErkok]

@andersk SBV 7.4 is now out on hackage, which contains this fix.