Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
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.
Maximizing bit-vectors
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
:: SFiniteBits a | |
=> Bool | Do we want unsat-cores if unsatisfiable? |
-> SBV a | Value to maximize |
-> Symbolic SatResult |
Maximize the value of an unsigned bit-vector value, using the default solver.
maxBVWith :: SFiniteBits a => SMTConfig -> Bool -> SBV a -> Symbolic SatResult Source #
Maximize the value of an unsigned bit-vector value, using the given solver.
Minimizing bit-vectors
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
:: SFiniteBits a | |
=> Bool | Do we want unsat-cores if unsatisfiable? |
-> SBV a | Value to minimize |
-> Symbolic SatResult |
Minimize the value of an unsigned bit-vector value, using the default solver.