    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeOperators #-}

    {-|
    Module           : What4.Utils.ResolveBounds.BV
    Description      : Resolve the lower and upper bounds of a SymBV
    Copyright        : (c) Galois, Inc 2021
    License          : BSD3
    Maintainer       : Ryan Scott <rscott@galois.com>

    A utility for using an 'WPO.OnlineSolver' to query if a 'WI.SymBV' is concrete
    or symbolic, and if it is symbolic, what the lower and upper bounds are.
    -}
    module What4.Utils.ResolveBounds.BV
      ( resolveSymBV
      , SearchStrategy(..)
      , ResolvedSymBV(..)
      ) where

    import           Data.BitVector.Sized ( BV )
    import qualified Data.BitVector.Sized as BV
    import qualified Data.Parameterized.NatRepr as PN
    import qualified Prettyprinter as PP

    import qualified What4.Expr.Builder as WEB
    import qualified What4.Expr.GroundEval as WEG
    import qualified What4.Interface as WI
    import qualified What4.Protocol.Online as WPO
    import qualified What4.Protocol.SMTWriter as WPS
    import qualified What4.SatResult as WSat
    import qualified What4.Utils.BVDomain.Arith as WUBA

    -- | The results of an 'WPO.OnlineSolver' trying to resolve a 'WI.SymBV' as
    -- concrete.
    data ResolvedSymBV w
      = BVConcrete (BV w)
        -- ^ A concrete bitvector, including its value as a 'BV'.
      | BVSymbolic (WUBA.Domain w)
        -- ^ A symbolic 'SymBV', including its lower and upper bounds as a
        --   'WUBA.Domain'.

    instance Show (ResolvedSymBV w) where
      showsPrec :: Int -> ResolvedSymBV w -> ShowS
    showsPrec Int
    _p ResolvedSymBV w
    res =
        case ResolvedSymBV w
    res of
          BVConcrete BV w
    bv ->
            String -> ShowS
    showString String
    "BVConcrete " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> BV w -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    11 BV w
    bv
          BVSymbolic Domain w
    d  ->
            let (Integer
    lb, Integer
    ub) = Domain w -> (Integer, Integer)
    forall (w :: Nat). Domain w -> (Integer, Integer)
    WUBA.ubounds Domain w
    d in
              String -> ShowS
    showString String
    "BVSymbolic ["
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    11 Integer
    lb
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    ", "
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    11 Integer
    ub
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    "]"

    -- | The strategy to use to search for lower and upper bounds in
    -- 'resolveSymBV'.
    data SearchStrategy
      = ExponentialSearch
        -- ^ After making an initial guess for a bound, increase (for upper bounds)
        --   or decrease (for lower bounds) the initial guess by an exponentially
        --   increasing amount (1, 2, 4, 8, ...) until the bound has been exceeded.
        --   At that point, back off from exponential search and use binary search
        --   until the bound has been determined.
        --
        --   For many use cases, this is a reasonable default.
      | BinarySearch
        -- ^ Use binary search to found each bound, using @0@ as the leftmost
        --   bounds of the search and 'BV.maxUnsigned' as the rightmost bounds of
        --   the search.

      -- Some possibilities for additional search strategies include:
      --
      -- - Using Z3's minimize/maximize commands. See
      --   https://github.com/GaloisInc/what4/issues/188
      --
      -- - A custom, user-specified strategy that uses callback(s) to guide the
      --   search at each iteration.

    instance PP.Pretty SearchStrategy where
      pretty :: forall ann. SearchStrategy -> Doc ann
    pretty SearchStrategy
    ExponentialSearch = String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    "exponential search"
      pretty SearchStrategy
    BinarySearch      = String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    "binary search"

    -- | Use an 'WPO.OnlineSolver' to attempt to resolve a 'WI.SymBV' as concrete.
    -- If it cannot, return the lower and upper bounds. This is primarly intended
    -- for compound expressions whose bounds cannot trivially be determined by
    -- using 'WI.signedBVBounds' or 'WI.unsignedBVBounds'.
    resolveSymBV ::
         forall w sym solver scope st fs
       . ( 1 PN.<= w
         , sym ~ WEB.ExprBuilder scope st fs
         , WPO.OnlineSolver solver
         )
      => sym
      -> SearchStrategy
         -- ^ The strategy to use when searching for lower and upper bounds. For
         --   many use cases, 'ExponentialSearch' is a reasonable default.
      -> PN.NatRepr w
         -- ^ The bitvector width
      -> WPO.SolverProcess scope solver
         -- ^ The online solver process to use to search for lower and upper
         --   bounds.
      -> WI.SymBV sym w
         -- ^ The bitvector to resolve.
      -> IO (ResolvedSymBV w)
    resolveSymBV :: forall (w :: Nat) sym solver scope (st :: Type -> Type) fs.
    (1 <= w, sym ~ ExprBuilder scope st fs, OnlineSolver solver) =>
    sym
    -> SearchStrategy
    -> NatRepr w
    -> SolverProcess scope solver
    -> SymBV sym w
    -> IO (ResolvedSymBV w)
    resolveSymBV sym
    sym SearchStrategy
    searchStrat NatRepr w
    w SolverProcess scope solver
    proc SymBV sym w
    symBV =
      -- First check, if the SymBV can be trivially resolved as concrete. If so,
      -- this can avoid the need to call out to the solver at all.
      case Expr scope (BaseBVType w) -> Maybe (BV w)
    forall (w :: Nat). Expr scope (BaseBVType w) -> Maybe (BV w)
    forall (e :: BaseType -> Type) (w :: Nat).
    IsExpr e =>
    e (BaseBVType w) -> Maybe (BV w)
    WI.asBV SymBV sym w
    Expr scope (BaseBVType w)
    symBV of
        Just BV w
    bv -> ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
    -> ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a b. (a -> b) -> a -> b
    $ BV w -> ResolvedSymBV w
    forall (w :: Nat). BV w -> ResolvedSymBV w
    BVConcrete BV w
    bv
        -- Otherwise, we need to consult the solver.
        Maybe (BV w)
    Nothing -> do
          -- First, ask for a particular model of the SymBV...
          BV w
    modelForBV <- SolverProcess scope solver -> IO (BV w) -> IO (BV w)
    forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver -> m a -> m a
    WPO.inNewFrame SolverProcess scope solver
    proc (IO (BV w) -> IO (BV w)) -> IO (BV w) -> IO (BV w)
    forall a b. (a -> b) -> a -> b
    $ do
            SatResult (GroundEvalFn scope) ()
    msat <- SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver
    -> String -> IO (SatResult (GroundEvalFn scope) ())
    WPO.checkAndGetModel SolverProcess scope solver
    proc String
    "resolveSymBV (check with initial assumptions)"
            GroundEvalFn scope
    model <- case SatResult (GroundEvalFn scope) ()
    msat of
              SatResult (GroundEvalFn scope) ()
    WSat.Unknown   -> IO (GroundEvalFn scope)
    forall a. IO a
    failUnknown
              WSat.Unsat{}   -> String -> IO (GroundEvalFn scope)
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "resolveSymBV: Initial assumptions are unsatisfiable"
              WSat.Sat GroundEvalFn scope
    model -> GroundEvalFn scope -> IO (GroundEvalFn scope)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure GroundEvalFn scope
    model
            GroundEvalFn scope
    -> forall (tp :: BaseType). Expr scope tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WEG.groundEval GroundEvalFn scope
    model SymBV sym w
    Expr scope (BaseBVType w)
    symBV
          -- ...next, check if this is the only possible model for this SymBV. We
          -- do this by adding a blocking clause that assumes the SymBV is /not/
          -- equal to the model we found in the previous step. If this is
          -- unsatisfiable, the SymBV can only be equal to that model, so we can
          -- conclude it is concrete. If it is satisfiable, on the other hand, the
          -- SymBV can be multiple values, so it is truly symbolic.
          Bool
    isSymbolic <- SolverProcess scope solver -> IO Bool -> IO Bool
    forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver -> m a -> m a
    WPO.inNewFrame SolverProcess scope solver
    proc (IO Bool -> IO Bool) -> IO Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ do
            BoolExpr scope
    block <- sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    WI.notPred sym
    sym (BoolExpr scope -> IO (BoolExpr scope))
    -> IO (BoolExpr scope) -> IO (BoolExpr scope)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    WI.bvEq sym
    sym SymBV sym w
    symBV (Expr scope (BaseBVType w) -> IO (BoolExpr scope))
    -> IO (Expr scope (BaseBVType w)) -> IO (BoolExpr scope)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    WI.bvLit sym
    sym NatRepr w
    w BV w
    modelForBV
            WriterConn scope solver -> BoolExpr scope -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    WPS.assume WriterConn scope solver
    conn BoolExpr scope
    block
            SatResult () ()
    msat <- SolverProcess scope solver -> String -> IO (SatResult () ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> String -> IO (SatResult () ())
    WPO.check SolverProcess scope solver
    proc String
    "resolveSymBV (check under assumption that model cannot happen)"
            case SatResult () ()
    msat of
              SatResult () ()
    WSat.Unknown -> IO Bool
    forall a. IO a
    failUnknown
              WSat.Sat{}   -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    True  -- Truly symbolic
              WSat.Unsat{} -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    False -- Concrete
          if Bool
    isSymbolic
            then
              -- If we have a truly symbolic SymBV, search for its lower and upper
              -- bounds, using the model from the previous step as a starting point
              -- for the search.
              case SearchStrategy
    searchStrat of
                SearchStrategy
    ExponentialSearch -> do
                  -- Use the model from the previous step as the initial guess for
                  -- each bound
                  BV w
    lowerBound <- BV w -> IO (BV w)
    computeLowerBoundExponential BV w
    modelForBV
                  BV w
    upperBound <- BV w -> IO (BV w)
    computeUpperBoundExponential BV w
    modelForBV
                  ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
    -> ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a b. (a -> b) -> a -> b
    $ Domain w -> ResolvedSymBV w
    forall (w :: Nat). Domain w -> ResolvedSymBV w
    BVSymbolic (Domain w -> ResolvedSymBV w) -> Domain w -> ResolvedSymBV w
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> Integer -> Integer -> Domain w
    forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
    WUBA.range NatRepr w
    w
                    (BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    lowerBound) (BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    upperBound)
                SearchStrategy
    BinarySearch -> do
                  BV w
    lowerBound <- BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary BV w
    bvZero BV w
    bvMaxUnsigned
                  BV w
    upperBound <- BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary BV w
    bvZero BV w
    bvMaxUnsigned
                  ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
    -> ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a b. (a -> b) -> a -> b
    $ Domain w -> ResolvedSymBV w
    forall (w :: Nat). Domain w -> ResolvedSymBV w
    BVSymbolic (Domain w -> ResolvedSymBV w) -> Domain w -> ResolvedSymBV w
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> Integer -> Integer -> Domain w
    forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
    WUBA.range NatRepr w
    w
                    (BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    lowerBound) (BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    upperBound)
            else ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
    -> ResolvedSymBV w -> IO (ResolvedSymBV w)
    forall a b. (a -> b) -> a -> b
    $ BV w -> ResolvedSymBV w
    forall (w :: Nat). BV w -> ResolvedSymBV w
    BVConcrete BV w
    modelForBV
      where
        conn :: WPS.WriterConn scope solver
        conn :: WriterConn scope solver
    conn = SolverProcess scope solver -> WriterConn scope solver
    forall scope solver.
    SolverProcess scope solver -> WriterConn scope solver
    WPO.solverConn SolverProcess scope solver
    proc

        failUnknown :: forall a. IO a
        failUnknown :: forall a. IO a
    failUnknown = String -> IO a
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    "resolveSymBV: Resolving value yielded UNKNOWN"

        bvZero :: BV w
        bvZero :: BV w
    bvZero = NatRepr w -> BV w
    forall (w :: Nat). NatRepr w -> BV w
    BV.zero NatRepr w
    w

        bvOne :: BV w
        bvOne :: BV w
    bvOne = NatRepr w -> BV w
    forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
    BV.one NatRepr w
    w

        bvTwo :: BV w
        bvTwo :: BV w
    bvTwo = NatRepr w -> Integer -> BV w
    forall (w :: Nat). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w Integer
    2

        bvMaxUnsigned :: BV w
        bvMaxUnsigned :: BV w
    bvMaxUnsigned = NatRepr w -> BV w
    forall (w :: Nat). NatRepr w -> BV w
    BV.maxUnsigned NatRepr w
    w

        -- The general strategy for finding a bound is that we start searching
        -- from a particular value known to be within bounds. At each step, we
        -- change this value by exponentially increasing amount, then check if we
        -- have exceeded the bound by using the solver. If so, we then fall back to
        -- binary search to determine an exact bound. If we are within bounds, we
        -- repeat the process.
        --
        -- As an example, let's suppose we having a symbolic value with bounds of
        -- [0, 12], and we start searching for the upper bound at the value 1:
        --
        -- * In the first step, we add 1 to the starting value to get 2. We check
        --   if two has exceeded the upper bound using the solver. This is not the
        --   case, so we continue.
        -- * In the second step, we add 2 to the starting value. The result, 3,
        --   is within bounds.
        -- * We continue like this in the third and fourth steps, except that
        --   we add 4 and 8 to the starting value to get 5 and 9, respectively.
        -- * In the fifth step, we add 16 to the starting value. The result, 17,
        --   has exceeded the upper bound. We will now fall back to binary search,
        --   using the previous result (9) as the leftmost bounds of the search and
        --   the current result (17) as the rightmost bounds of the search.
        -- * Eventually, binary search discovers that 12 is the upper bound.
        --
        -- Note that at each step, we must also check to make sure that the amount
        -- to increase the starting value by does not cause a numeric overflow. If
        -- this would be the case, we fall back to binary search, using
        -- BV.maxUnsigned as the rightmost bounds of the search.
        --
        -- The process for finding a lower bound is quite similar, except that we
        -- /subtract/ an exponentially increasing amount from the starting value
        -- each time rather than adding it.

        computeLowerBoundExponential :: BV w -> IO (BV w)
        computeLowerBoundExponential :: BV w -> IO (BV w)
    computeLowerBoundExponential BV w
    start = BV w -> BV w -> IO (BV w)
    go BV w
    start BV w
    bvOne
          where
            go :: BV w -> BV w -> IO (BV w)
            go :: BV w -> BV w -> IO (BV w)
    go BV w
    previouslyTried BV w
    diff
              | -- If the diff is larger than the starting value, then subtracting
                -- the diff from the starting value would cause underflow. Instead,
                -- just fall back to binary search, using 0 as the leftmost bounds
                -- of the search.
                BV w
    start BV w -> BV w -> Bool
    forall (w :: Nat). BV w -> BV w -> Bool
    `BV.ult` BV w
    diff
              = BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary BV w
    bvZero BV w
    previouslyTried

              | -- Otherwise, check if (start - diff) exceeds the lower bound for
                -- the symBV.
                Bool
    otherwise
              = do let nextToTry :: BV w
    nextToTry = NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
    BV.sub NatRepr w
    w BV w
    start BV w
    diff
                   Bool
    exceedsLB <- BV w -> IO Bool
    checkExceedsLowerBound BV w
    nextToTry
                   if |  -- If we have exceeded the lower bound, fall back to
                         -- binary search.
                         Bool
    exceedsLB
                      -> BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary BV w
    nextToTry BV w
    previouslyTried
                      |  -- Make sure that (diff * 2) doesn't overflow. If it
                         -- would, fall back to binary search.
                         BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    diff Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    2 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    bvMaxUnsigned
                      -> BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary BV w
    bvZero BV w
    nextToTry
                      |  -- Otherwise, keep exponentially searching.
                         Bool
    otherwise
                      -> BV w -> BV w -> IO (BV w)
    go BV w
    nextToTry (BV w -> IO (BV w)) -> BV w -> IO (BV w)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
    BV.mul NatRepr w
    w BV w
    diff BV w
    bvTwo

        -- Search for the upper bound of the SymBV. This function assumes the
        -- following invariants:
        --
        -- * l <= r
        --
        -- * The lower bound of the SymBV is somewhere within the range [l, r].
        computeLowerBoundBinary :: BV w -> BV w -> IO (BV w)
        computeLowerBoundBinary :: BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary BV w
    l BV w
    r
          | -- If the leftmost and rightmost bounds are the same, we are done.
            BV w
    l BV w -> BV w -> Bool
    forall a. Eq a => a -> a -> Bool
    == BV w
    r
          = BV w -> IO (BV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure BV w
    l

          | -- If the leftmost and rightmost bounds of the search are 1 apart, we
            -- only have two possible choices for the lower bound. Consult the
            -- solver to determine which one is the lower bound.
            NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
    BV.sub NatRepr w
    w BV w
    r BV w
    l BV w -> BV w -> Bool
    forall a. Ord a => a -> a -> Bool
    < BV w
    bvTwo
          = do Bool
    lExceedsLB <- BV w -> IO Bool
    checkExceedsLowerBound BV w
    l
               BV w -> IO (BV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (BV w -> IO (BV w)) -> BV w -> IO (BV w)
    forall a b. (a -> b) -> a -> b
    $ if Bool
    lExceedsLB then BV w
    r else BV w
    l

          | -- Otherwise, keep binary searching.
            Bool
    otherwise
          = do let nextToTry :: BV w
    nextToTry = NatRepr w -> Integer -> BV w
    forall (w :: Nat). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w ((BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    l Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    r) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    2)
               Bool
    exceedsLB <- BV w -> IO Bool
    checkExceedsLowerBound BV w
    nextToTry
               if Bool
    exceedsLB
                 then BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary BV w
    nextToTry BV w
    r
                 else BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary BV w
    l BV w
    nextToTry

        checkExceedsLowerBound :: BV w -> IO Bool
        checkExceedsLowerBound :: BV w -> IO Bool
    checkExceedsLowerBound BV w
    bv = SolverProcess scope solver -> IO Bool -> IO Bool
    forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver -> m a -> m a
    WPO.inNewFrame SolverProcess scope solver
    proc (IO Bool -> IO Bool) -> IO Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ do
          BoolExpr scope
    leLowerBound <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    WI.bvUle sym
    sym SymBV sym w
    symBV (Expr scope (BaseBVType w) -> IO (BoolExpr scope))
    -> IO (Expr scope (BaseBVType w)) -> IO (BoolExpr scope)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    WI.bvLit sym
    sym NatRepr w
    w BV w
    bv
          WriterConn scope solver -> BoolExpr scope -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    WPS.assume WriterConn scope solver
    conn BoolExpr scope
    leLowerBound
          SatResult () ()
    msat <- SolverProcess scope solver -> String -> IO (SatResult () ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> String -> IO (SatResult () ())
    WPO.check SolverProcess scope solver
    proc String
    "resolveSymBV (check if lower bound has been exceeded)"
          case SatResult () ()
    msat of
            SatResult () ()
    WSat.Unknown -> IO Bool
    forall a. IO a
    failUnknown
            WSat.Sat{}   -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    False
            WSat.Unsat{} -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    True -- symBV cannot be <= this value,
                                      -- so the value must be strictly
                                      -- less than the lower bound.

        computeUpperBoundExponential :: BV w -> IO (BV w)
        computeUpperBoundExponential :: BV w -> IO (BV w)
    computeUpperBoundExponential BV w
    start = BV w -> BV w -> IO (BV w)
    go BV w
    start BV w
    bvOne
          where
            go :: BV w -> BV w -> IO (BV w)
            go :: BV w -> BV w -> IO (BV w)
    go BV w
    previouslyTried BV w
    diff
              | -- Make sure that adding the diff to the starting value will not
                -- result in overflow. If it would, just fall back to binary
                -- search, using BV.maxUnsigned as the rightmost bounds of the
                -- search.
                BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    start Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    diff Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    bvMaxUnsigned
              = BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary BV w
    previouslyTried BV w
    bvMaxUnsigned

              | Bool
    otherwise
              = do let nextToTry :: BV w
    nextToTry = NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
    BV.add NatRepr w
    w BV w
    start BV w
    diff
                   Bool
    exceedsUB <- BV w -> IO Bool
    checkExceedsUpperBound BV w
    nextToTry
                   if |  -- If we have exceeded the upper bound, fall back to
                         -- binary search.
                         Bool
    exceedsUB
                      -> BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary BV w
    previouslyTried BV w
    nextToTry
                      |  -- Make sure that (diff * 2) doesn't overflow. If it
                         -- would, fall back to binary search.
                         BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    diff Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    2 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    bvMaxUnsigned
                      -> BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary BV w
    nextToTry BV w
    bvMaxUnsigned
                      |  -- Otherwise, keep exponentially searching.
                         Bool
    otherwise
                      -> BV w -> BV w -> IO (BV w)
    go BV w
    nextToTry (BV w -> IO (BV w)) -> BV w -> IO (BV w)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
    BV.mul NatRepr w
    w BV w
    diff BV w
    bvTwo

        -- Search for the upper bound of the SymBV. This function assumes the
        -- following invariants:
        --
        -- * l <= r
        --
        -- * The upper bound of the SymBV is somewhere within the range [l, r].
        computeUpperBoundBinary :: BV w -> BV w -> IO (BV w)
        computeUpperBoundBinary :: BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary BV w
    l BV w
    r
          | -- If the leftmost and rightmost bounds are the same, we are done.
            BV w
    l BV w -> BV w -> Bool
    forall a. Eq a => a -> a -> Bool
    == BV w
    r
          = BV w -> IO (BV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure BV w
    l

          | -- If the leftmost and rightmost bounds of the search are 1 apart, we
            -- only have two possible choices for the upper bound. Consult the
            -- solver to determine which one is the upper bound.
            NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
    BV.sub NatRepr w
    w BV w
    r BV w
    l BV w -> BV w -> Bool
    forall a. Ord a => a -> a -> Bool
    < BV w
    bvTwo
          = do Bool
    rExceedsUB <- BV w -> IO Bool
    checkExceedsUpperBound BV w
    r
               BV w -> IO (BV w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (BV w -> IO (BV w)) -> BV w -> IO (BV w)
    forall a b. (a -> b) -> a -> b
    $ if Bool
    rExceedsUB then BV w
    l else BV w
    r

          | -- Otherwise, keep binary searching.
            Bool
    otherwise
          = do let nextToTry :: BV w
    nextToTry = NatRepr w -> Integer -> BV w
    forall (w :: Nat). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w ((BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    l Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned BV w
    r) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    2)
               Bool
    exceedsUB <- BV w -> IO Bool
    checkExceedsUpperBound BV w
    nextToTry
               if Bool
    exceedsUB
                 then BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary BV w
    l BV w
    nextToTry
                 else BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary BV w
    nextToTry BV w
    r

        checkExceedsUpperBound :: BV w -> IO Bool
        checkExceedsUpperBound :: BV w -> IO Bool
    checkExceedsUpperBound BV w
    bv = SolverProcess scope solver -> IO Bool -> IO Bool
    forall (m :: Type -> Type) solver scope a.
    (MonadIO m, MonadMask m, SMTReadWriter solver) =>
    SolverProcess scope solver -> m a -> m a
    WPO.inNewFrame SolverProcess scope solver
    proc (IO Bool -> IO Bool) -> IO Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ do
          BoolExpr scope
    geUpperBound <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    WI.bvUge sym
    sym SymBV sym w
    symBV (Expr scope (BaseBVType w) -> IO (BoolExpr scope))
    -> IO (Expr scope (BaseBVType w)) -> IO (BoolExpr scope)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    WI.bvLit sym
    sym NatRepr w
    w BV w
    bv
          WriterConn scope solver -> BoolExpr scope -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    WPS.assume WriterConn scope solver
    conn BoolExpr scope
    geUpperBound
          SatResult () ()
    msat <- SolverProcess scope solver -> String -> IO (SatResult () ())
    forall solver scope.
    SMTReadWriter solver =>
    SolverProcess scope solver -> String -> IO (SatResult () ())
    WPO.check SolverProcess scope solver
    proc String
    "resolveSymBV (check if upper bound has been exceeded)"
          case SatResult () ()
    msat of
            SatResult () ()
    WSat.Unknown -> IO Bool
    forall a. IO a
    failUnknown
            WSat.Sat{}   -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    False
            WSat.Unsat{} -> Bool -> IO Bool
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure Bool
    True -- symBV cannot be >= this upper bound,
                                      -- so the value must be strictly
                                      -- greater than the upper bound.