Unexpected behavior when trying to minimize bitvector

[danielrainer]

I have code which builds up some constraints over bitvectors and then tries to minimize the value of one of them. Code to reproduce the issue can be found at https://github.com/danielrainer/z3_rust_minimize_repro

What I expected my code to do:

• Set up some constraints over bitvectors (in this case read from a SMT-LIB string)
• Add the requirement to minimize the value of one of the bitvectors
• Find a model where the bitvector which should be minimized has minimal value
• The loop at the end should not be necessary, but when present, it should have the same effect as automatic minimization

What happens:

• The first model found has a non-minimized value of #x0000d72b44f15e6d for the relevant bitvector.
• The model found by decreasing the upper limit on the bitvector until the constraints become unsatisfiable finds the minimized value #x0000d72b44b15e6d (which is different at bit index 22, f vs b)

Am I misusing the API, do I misunderstand some semantics, or is this a bug?

For reference, the version of Z3 installed on my system is

Z3 version 4.13.0 - 64 bit - build hashcode 3049f578a8f98a0b0992eca193afe57a73b30ca3

When I extend the constraints file by appending

(minimize initial_a)
(check-sat)
(get-model)

and directly invoking Z3 from the command line, the resulting model has the expected value of #x0000d72b44b15e6d.

[toolCHAINZ]

Looking over this, I think I see the issue. You are using both Solver and Optimize, but these two types are independent of each other: using Optimize::minimize has no effect on the Solver::check and Solver::from_string has no effect on Optimize::minimize. Optimize itself is essentially a flavor of Solver, which also supports minimization/maximization. It has its own from_string and its own check. So for your code to work as intended, you should be doing the assertions and checking in the Optimize itself.

[danielrainer]

Ah yes, using Optimize for everything makes it work as expected, thank you for the explanation.

Solver::new() and Optimize::new() (and BV::new_const()) have been changed to no longer take a context since I opened the issue, which helps with indicating that there is no connection between the solver and the optimizer.

Maybe it would even work to unify the interface of Solver and Optimize into one shared struct, but I don't know nearly enough about the implementation to judge if that is realistic.

[toolCHAINZ]

Excellent! Ah yes, I removed the Context argument because it was annoying to force users to track it but I hadn't thought of the drawback that it makes things look connected that really aren't (especially when approaching Z3 for the first time). Glad to hear that's clearer!

I like the idea of combining them, will have to think on that. It would definitely be an "opinionated" change: Optimize and Solver are separate types in the exposed Z3 API. I could maybe see an implementation that uses Solver in the background and switches it out for an Optimize if you use minimize or maximize? I could also see users wanting to keep explicit control over which Z3 API they're using: subtle changes in API usage can cause surprisingly large performance diffs in Z3, so having full control is nice for cases when you know exactly what the "happy path" is.