-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.BVOptimize
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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>.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.BVOptimize (
            -- ** Maximizing bit-vectors
            -- $maxBVEx
              maxBV, maxBVWith
            -- ** Minimizing bit-vectors
            -- $minBVEx
            , minBV, minBVWith
          ) where

import Control.Monad

import Data.SBV
import Data.SBV.Control

-- $setup
-- >>> -- For doctest purposes only:
-- >>> :set -XDataKinds
-- >>> import Data.SBV

{- $maxBVEx

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
-}

-- | Maximize the value of an unsigned bit-vector value, using the default solver.
maxBV :: SFiniteBits a
      => Bool                -- ^ Do we want unsat-cores if unsatisfiable?
      -> SBV a               -- ^ Value to maximize
      -> Symbolic SatResult
maxBV :: forall a. SFiniteBits a => Bool -> SBV a -> Symbolic SatResult
maxBV = SMTConfig -> Bool -> SBV a -> Symbolic SatResult
forall a.
SFiniteBits a =>
SMTConfig -> Bool -> SBV a -> Symbolic SatResult
maxBVWith SMTConfig
defaultSMTCfg

-- | Maximize the value of an unsigned bit-vector value, using the given solver.
maxBVWith :: SFiniteBits a => SMTConfig -> Bool-> SBV a -> Symbolic SatResult
maxBVWith :: forall a.
SFiniteBits a =>
SMTConfig -> Bool -> SBV a -> Symbolic SatResult
maxBVWith = Bool -> SMTConfig -> Bool -> SBV a -> Symbolic SatResult
forall a.
SFiniteBits a =>
Bool -> SMTConfig -> Bool -> SBV a -> Symbolic SatResult
minMaxBV Bool
True

{- $minBVEx

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
-}

-- | Minimize the value of an unsigned bit-vector value, using the default solver.
minBV :: SFiniteBits a
      => Bool                -- ^ Do we want unsat-cores if unsatisfiable?
      -> SBV a               -- ^ Value to minimize
      -> Symbolic SatResult
minBV :: forall a. SFiniteBits a => Bool -> SBV a -> Symbolic SatResult
minBV = SMTConfig -> Bool -> SBV a -> Symbolic SatResult
forall a.
SFiniteBits a =>
SMTConfig -> Bool -> SBV a -> Symbolic SatResult
minBVWith SMTConfig
defaultSMTCfg

-- | Minimize the value of an unsigned bit-vector value, using the given solver.
minBVWith :: SFiniteBits a => SMTConfig -> Bool-> SBV a -> Symbolic SatResult
minBVWith :: forall a.
SFiniteBits a =>
SMTConfig -> Bool -> SBV a -> Symbolic SatResult
minBVWith = Bool -> SMTConfig -> Bool -> SBV a -> Symbolic SatResult
forall a.
SFiniteBits a =>
Bool -> SMTConfig -> Bool -> SBV a -> Symbolic SatResult
minMaxBV Bool
False

-- | min/max a given unsigned bit-vector. We walk down the bits in an incremental
-- fashion. If we are maximizing, we try to make the bits set as we go down, otherwise
-- we try to unset them. We keep adding the constraints so long as they are satisfiable,
-- and at the end, get the optimal value produced.
minMaxBV :: SFiniteBits a => Bool -> SMTConfig -> Bool -> SBV a -> Symbolic SatResult
minMaxBV :: forall a.
SFiniteBits a =>
Bool -> SMTConfig -> Bool -> SBV a -> Symbolic SatResult
minMaxBV Bool
isMax SMTConfig
cfg Bool
getUC SBV a
v
 | SBV a -> Bool
forall a. HasKind a => a -> Bool
hasSign SBV a
v
 = [Char] -> Symbolic SatResult
forall a. HasCallStack => [Char] -> a
error ([Char] -> Symbolic SatResult) -> [Char] -> Symbolic SatResult
forall a b. (a -> b) -> a -> b
$ [Char]
"minMaxBV works on unsigned bitvectors, received: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Kind -> [Char]
forall a. Show a => a -> [Char]
show (SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
v)
 | Bool
True
 = do Bool -> SymbolicT IO () -> SymbolicT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
getUC (SymbolicT IO () -> SymbolicT IO ())
-> SymbolicT IO () -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SMTOption -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> SymbolicT IO ()) -> SMTOption -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> SMTOption
ProduceUnsatCores Bool
True
      Query SatResult -> Symbolic SatResult
forall a. Query a -> Symbolic a
query (Query SatResult -> Symbolic SatResult)
-> Query SatResult -> Symbolic SatResult
forall a b. (a -> b) -> a -> b
$ [SBool] -> Query SatResult
go (SBV a -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV a
v)
 where uc :: QueryT IO (Maybe [[Char]])
uc | Bool
getUC = [[Char]] -> Maybe [[Char]]
forall a. a -> Maybe a
Just ([[Char]] -> Maybe [[Char]])
-> QueryT IO [[Char]] -> QueryT IO (Maybe [[Char]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO [[Char]]
getUnsatCore
          | Bool
True  = Maybe [[Char]] -> QueryT IO (Maybe [[Char]])
forall a. a -> QueryT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [[Char]]
forall a. Maybe a
Nothing

       rSat :: Query SatResult
rSat   = SMTResult -> SatResult
SatResult (SMTResult -> SatResult)
-> (SMTModel -> SMTResult) -> SMTModel -> SatResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> SMTModel -> SMTResult
Satisfiable   SMTConfig
cfg (SMTModel -> SatResult) -> QueryT IO SMTModel -> Query SatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SMTModel
getModel
       rUnk :: Query SatResult
rUnk   = SMTResult -> SatResult
SatResult (SMTResult -> SatResult)
-> (SMTReasonUnknown -> SMTResult) -> SMTReasonUnknown -> SatResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown       SMTConfig
cfg (SMTReasonUnknown -> SatResult)
-> QueryT IO SMTReasonUnknown -> Query SatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SMTReasonUnknown
getUnknownReason
       rUnsat :: Query SatResult
rUnsat = SMTResult -> SatResult
SatResult (SMTResult -> SatResult)
-> (Maybe [[Char]] -> SMTResult) -> Maybe [[Char]] -> SatResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> Maybe [[Char]] -> SMTResult
Unsatisfiable SMTConfig
cfg (Maybe [[Char]] -> SatResult)
-> QueryT IO (Maybe [[Char]]) -> Query SatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO (Maybe [[Char]])
uc

       go :: [SBool] -> Query SatResult
       go :: [SBool] -> Query SatResult
go []     = do r <- Query CheckSatResult
checkSat
                      case r of
                        CheckSatResult
Sat     -> Query SatResult
rSat
                        CheckSatResult
Unsat   -> Query SatResult
rUnsat
                        CheckSatResult
Unk     -> Query SatResult
rUnk
                        DSat {} -> [Char] -> Query SatResult
forall a. HasCallStack => [Char] -> a
error [Char]
"minMaxBV: Unexpected DSat result"
       go (SBool
b:[SBool]
bs) = do Int -> Query ()
push Int
1
                      if Bool
isMax then SBool -> Query ()
forall a. QuantifiedBool a => a -> Query ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain SBool
b
                               else SBool -> Query ()
forall a. QuantifiedBool a => a -> Query ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot SBool
b
                      r <- Query CheckSatResult
checkSat
                      case r of
                        CheckSatResult
Sat    -> [SBool] -> Query SatResult
go [SBool]
bs Query SatResult
-> (SatResult -> Query SatResult) -> Query SatResult
forall a b. QueryT IO a -> (a -> QueryT IO b) -> QueryT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SatResult
res -> Int -> Query ()
pop Int
1 Query () -> Query SatResult -> Query SatResult
forall a b. QueryT IO a -> QueryT IO b -> QueryT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SatResult -> Query SatResult
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SatResult
res
                        CheckSatResult
Unsat  ->                   Int -> Query ()
pop Int
1 Query () -> Query SatResult -> Query SatResult
forall a b. QueryT IO a -> QueryT IO b -> QueryT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [SBool] -> Query SatResult
go [SBool]
bs
                        CheckSatResult
Unk    ->                   Int -> Query ()
pop Int
1 Query () -> Query SatResult -> Query SatResult
forall a b. QueryT IO a -> QueryT IO b -> QueryT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Query SatResult
rUnk
                        DSat{} -> [Char] -> Query SatResult
forall a. HasCallStack => [Char] -> a
error [Char]
"minMaxBV: Unexpected DSat result"