Bit-vector optimization based on linear scan of the bits. The optimization engines are usually not incremental, and they perform poorly for optimizing bit-vector values in the presence of complicated constraints. We implement a simple optimizer by scanning the bits from top-to-bottom to minimize/maximize unsigned bit vector quantities, using the regular (i.e., incremental) solver. This can lead to better performance for this class of problems.

This implementation is based on an idea by Nikolaj Bjorner, see https://github.com/Z3Prover/z3/issues/7156.

Here is a simple example of maximizing a bit-vector value:

>>> :{
runSMT $ do x :: SWord 32 <- free "x"
            constrain $ x .> 5
            constrain $ x .< 27
            maxBV False x
:}
Satisfiable. Model:
  x = 26 :: Word32

Here is a simple example of minimizing a bit-vector value:

>>> :{
runSMT $ do x :: SWord 32 <- free "x"
            constrain $ x .> 5
            constrain $ x .< 27
            minBV False x
:}
Satisfiable. Model:
  x = 6 :: Word32