    -- |
    -- Module      :  Cryptol.Backend.SBV
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeSynonymInstances #-}
    {-# LANGUAGE ViewPatterns #-}
    module Cryptol.Backend.SBV
      ( SBV(..), SBVEval(..), SBVResult(..)
      , literalSWord
      , freshSBool_
      , freshBV_
      , freshSInteger_
      , addDefEqn
      , ashr
      , lshr
      , shl
      , evalPanic
      , svFromInteger
      , svToInteger
      ) where

    import qualified Control.Exception as X
    import           Control.Concurrent.MVar
    import           Control.Monad.IO.Class (MonadIO(..))
    import           Data.Bits (bit, complement)
    import           Data.List (foldl')

    import qualified GHC.Num.Compat as Integer

    import Data.SBV.Dynamic as SBV
    import qualified Data.SBV.Internals as SBV

    import Cryptol.Backend
    import Cryptol.Backend.Concrete ( integerToChar )
    import Cryptol.Backend.Monad
      ( Eval(..), blackhole, delayFill, evalSpark
      , EvalError(..), EvalErrorEx(..), Unsupported(..)
      , modifyCallStack, getCallStack, maybeReady
      )

    import Cryptol.Utils.Panic (panic)

    data SBV =
      SBV
      { SBV -> MVar State
    sbvStateVar     :: MVar (SBV.State)
      , SBV -> MVar SVal
    sbvDefRelations :: MVar SVal
      }

    -- Utility operations -------------------------------------------------------------

    fromBitsLE :: [SBit SBV] -> SWord SBV
    fromBitsLE :: [SBit SBV] -> SWord SBV
    fromBitsLE [SBit SBV]
    bs = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' SVal -> SVal -> SVal
    f (Int -> Integer -> SWord SBV
    literalSWord Int
    0 Integer
    0) [SVal]
    [SBit SBV]
    bs
      where f :: SVal -> SVal -> SVal
    f SVal
    w SVal
    b = SVal -> SVal -> SVal
    svJoin (SVal -> SVal
    svToWord1 SVal
    b) SVal
    w

    packSBV :: [SBit SBV] -> SWord SBV
    packSBV :: [SBit SBV] -> SWord SBV
    packSBV [SBit SBV]
    bs = [SBit SBV] -> SWord SBV
    fromBitsLE ([SVal] -> [SVal]
    forall a. [a] -> [a]
    reverse [SVal]
    [SBit SBV]
    bs)

    unpackSBV :: SWord SBV -> [SBit SBV]
    unpackSBV :: SWord SBV -> [SBit SBV]
    unpackSBV SWord SBV
    x = [ SVal -> Int -> SVal
    svTestBit SVal
    SWord SBV
    x Int
    i | Int
    i <- [Int] -> [Int]
    forall a. [a] -> [a]
    reverse [Int
    0 .. SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1] ]

    literalSWord :: Int -> Integer -> SWord SBV
    literalSWord :: Int -> Integer -> SWord SBV
    literalSWord Int
    w Integer
    i = Kind -> Integer -> SVal
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    False Int
    w) Integer
    i

    svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> SBV.State -> IO SVal
    #if MIN_VERSION_sbv(8,8,0)
    svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar_ = VarContext -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar (VarContext -> Kind -> Maybe String -> State -> IO SVal)
    -> (Maybe Quantifier -> VarContext)
    -> Maybe Quantifier
    -> Kind
    -> Maybe String
    -> State
    -> IO SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> VarContext
    SBV.NonQueryVar
    #else
    svMkSymVar_ = svMkSymVar
    #endif

    freshBV_ :: SBV -> Int -> IO (SWord SBV)
    freshBV_ :: SBV -> Int -> IO (SWord SBV)
    freshBV_ (SBV MVar State
    stateVar MVar SVal
    _) Int
    w =
      MVar State -> (State -> IO SVal) -> IO SVal
    forall a b. MVar a -> (a -> IO b) -> IO b
    withMVar MVar State
    stateVar (Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar_ Maybe Quantifier
    forall a. Maybe a
    Nothing (Bool -> Int -> Kind
    KBounded Bool
    False Int
    w) Maybe String
    forall a. Maybe a
    Nothing)

    freshSBool_ :: SBV -> IO (SBit SBV)
    freshSBool_ :: SBV -> IO (SBit SBV)
    freshSBool_ (SBV MVar State
    stateVar MVar SVal
    _) =
      MVar State -> (State -> IO SVal) -> IO SVal
    forall a b. MVar a -> (a -> IO b) -> IO b
    withMVar MVar State
    stateVar (Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar_ Maybe Quantifier
    forall a. Maybe a
    Nothing Kind
    KBool Maybe String
    forall a. Maybe a
    Nothing)

    freshSInteger_ :: SBV -> IO (SInteger SBV)
    freshSInteger_ :: SBV -> IO (SInteger SBV)
    freshSInteger_ (SBV MVar State
    stateVar MVar SVal
    _) =
      MVar State -> (State -> IO SVal) -> IO SVal
    forall a b. MVar a -> (a -> IO b) -> IO b
    withMVar MVar State
    stateVar (Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar_ Maybe Quantifier
    forall a. Maybe a
    Nothing Kind
    KUnbounded Maybe String
    forall a. Maybe a
    Nothing)

    -- SBV Evaluation monad -------------------------------------------------------

    data SBVResult a
      = SBVError !EvalErrorEx
      | SBVResult !SVal !a -- safety predicate and result

    instance Functor SBVResult where
      fmap :: forall a b. (a -> b) -> SBVResult a -> SBVResult b
    fmap a -> b
    _ (SBVError EvalErrorEx
    err) = EvalErrorEx -> SBVResult b
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err
      fmap a -> b
    f (SBVResult SVal
    p a
    x) = SVal -> b -> SBVResult b
    forall a. SVal -> a -> SBVResult a
    SBVResult SVal
    p (a -> b
    f a
    x)

    instance Applicative SBVResult where
      pure :: forall a. a -> SBVResult a
    pure = SVal -> a -> SBVResult a
    forall a. SVal -> a -> SBVResult a
    SBVResult SVal
    svTrue
      SBVError EvalErrorEx
    err <*> :: forall a b. SBVResult (a -> b) -> SBVResult a -> SBVResult b
    <*> SBVResult a
    _ = EvalErrorEx -> SBVResult b
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err
      SBVResult (a -> b)
    _ <*> SBVError EvalErrorEx
    err = EvalErrorEx -> SBVResult b
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err
      SBVResult SVal
    p1 a -> b
    f <*> SBVResult SVal
    p2 a
    x = SVal -> b -> SBVResult b
    forall a. SVal -> a -> SBVResult a
    SBVResult (SVal -> SVal -> SVal
    svAnd SVal
    p1 SVal
    p2) (a -> b
    f a
    x)

    instance Monad SBVResult where
      return :: forall a. a -> SBVResult a
    return = a -> SBVResult a
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      SBVError EvalErrorEx
    err >>= :: forall a b. SBVResult a -> (a -> SBVResult b) -> SBVResult b
    >>= a -> SBVResult b
    _ = EvalErrorEx -> SBVResult b
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err
      SBVResult SVal
    px a
    x >>= a -> SBVResult b
    m =
        case a -> SBVResult b
    m a
    x of
          SBVError EvalErrorEx
    err   -> EvalErrorEx -> SBVResult b
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err
          SBVResult SVal
    pm b
    z -> SVal -> b -> SBVResult b
    forall a. SVal -> a -> SBVResult a
    SBVResult (SVal -> SVal -> SVal
    svAnd SVal
    px SVal
    pm) b
    z

    newtype SBVEval a = SBVEval{ forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval :: Eval (SBVResult a) }
      deriving ((forall a b. (a -> b) -> SBVEval a -> SBVEval b)
    -> (forall a b. a -> SBVEval b -> SBVEval a) -> Functor SBVEval
    forall a b. a -> SBVEval b -> SBVEval a
    forall a b. (a -> b) -> SBVEval a -> SBVEval b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> SBVEval a -> SBVEval b
    fmap :: forall a b. (a -> b) -> SBVEval a -> SBVEval b
    $c<$ :: forall a b. a -> SBVEval b -> SBVEval a
    <$ :: forall a b. a -> SBVEval b -> SBVEval a
    Functor)

    instance Applicative SBVEval where
      pure :: forall a. a -> SBVEval a
    pure = Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult a) -> SBVEval a)
    -> (a -> Eval (SBVResult a)) -> a -> SBVEval a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBVResult a -> Eval (SBVResult a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVResult a -> Eval (SBVResult a))
    -> (a -> SBVResult a) -> a -> Eval (SBVResult a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBVResult a
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      SBVEval (a -> b)
    f <*> :: forall a b. SBVEval (a -> b) -> SBVEval a -> SBVEval b
    <*> SBVEval a
    x = Eval (SBVResult b) -> SBVEval b
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult b) -> SBVEval b)
    -> Eval (SBVResult b) -> SBVEval b
    forall a b. (a -> b) -> a -> b
    $
        do SBVResult (a -> b)
    f' <- SBVEval (a -> b) -> Eval (SBVResult (a -> b))
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SBVEval (a -> b)
    f
           SBVResult a
    x' <- SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SBVEval a
    x
           SBVResult b -> Eval (SBVResult b)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVResult (a -> b)
    f' SBVResult (a -> b) -> SBVResult a -> SBVResult b
    forall a b. SBVResult (a -> b) -> SBVResult a -> SBVResult b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBVResult a
    x')

    instance Monad SBVEval where
      return :: forall a. a -> SBVEval a
    return = a -> SBVEval a
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      SBVEval a
    x >>= :: forall a b. SBVEval a -> (a -> SBVEval b) -> SBVEval b
    >>= a -> SBVEval b
    f = Eval (SBVResult b) -> SBVEval b
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult b) -> SBVEval b)
    -> Eval (SBVResult b) -> SBVEval b
    forall a b. (a -> b) -> a -> b
    $
        SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SBVEval a
    x Eval (SBVResult a)
    -> (SBVResult a -> Eval (SBVResult b)) -> Eval (SBVResult b)
    forall a b. Eval a -> (a -> Eval b) -> Eval b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          SBVError EvalErrorEx
    err -> SBVResult b -> Eval (SBVResult b)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (EvalErrorEx -> SBVResult b
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err)
          SBVResult SVal
    px a
    x' ->
            SBVEval b -> Eval (SBVResult b)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval (a -> SBVEval b
    f a
    x') Eval (SBVResult b)
    -> (SBVResult b -> Eval (SBVResult b)) -> Eval (SBVResult b)
    forall a b. Eval a -> (a -> Eval b) -> Eval b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              SBVError EvalErrorEx
    err -> SBVResult b -> Eval (SBVResult b)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (EvalErrorEx -> SBVResult b
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err)
              SBVResult SVal
    pz b
    z -> SBVResult b -> Eval (SBVResult b)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> b -> SBVResult b
    forall a. SVal -> a -> SBVResult a
    SBVResult (SVal -> SVal -> SVal
    svAnd SVal
    px SVal
    pz) b
    z)

    instance MonadIO SBVEval where
      liftIO :: forall a. IO a -> SBVEval a
    liftIO IO a
    m = Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult a) -> SBVEval a)
    -> Eval (SBVResult a) -> SBVEval a
    forall a b. (a -> b) -> a -> b
    $ (a -> SBVResult a) -> Eval a -> Eval (SBVResult a)
    forall a b. (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> SBVResult a
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (IO a -> Eval a
    forall a. IO a -> Eval a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO a
    m)

    addDefEqn :: SBV -> SVal -> IO ()
    addDefEqn :: SBV -> SVal -> IO ()
    addDefEqn (SBV MVar State
    _ MVar SVal
    relsVar) SVal
    b = MVar SVal -> (SVal -> IO SVal) -> IO ()
    forall a. MVar a -> (a -> IO a) -> IO ()
    modifyMVar_ MVar SVal
    relsVar (SVal -> IO SVal
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> IO SVal) -> (SVal -> SVal) -> SVal -> IO SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> SVal -> SVal
    svAnd SVal
    b)

    -- Symbolic Big-endian Words -------------------------------------------------------

    instance Backend SBV where
      type SBit SBV = SVal
      type SWord SBV = SVal
      type SInteger SBV = SVal
      type SFloat SBV = ()        -- XXX: not implemented
      type SEval SBV = SBVEval

      raiseError :: forall a. SBV -> EvalError -> SEval SBV a
    raiseError SBV
    _ EvalError
    err = Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult a) -> SBVEval a)
    -> Eval (SBVResult a) -> SBVEval a
    forall a b. (a -> b) -> a -> b
    $
        do CallStack
    stk <- Eval CallStack
    getCallStack
           SBVResult a -> Eval (SBVResult a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (EvalErrorEx -> SBVResult a
    forall a. EvalErrorEx -> SBVResult a
    SBVError (CallStack -> EvalError -> EvalErrorEx
    EvalErrorEx CallStack
    stk EvalError
    err))

      assertSideCondition :: SBV -> SBit SBV -> EvalError -> SEval SBV ()
    assertSideCondition SBV
    sym SBit SBV
    cond EvalError
    err
        | Just Bool
    False <- SVal -> Maybe Bool
    svAsBool SVal
    SBit SBV
    cond = SBV -> EvalError -> SEval SBV ()
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. SBV -> EvalError -> SEval SBV a
    raiseError SBV
    sym EvalError
    err
        | Bool
    otherwise = Eval (SBVResult ()) -> SBVEval ()
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (SBVResult () -> Eval (SBVResult ())
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> () -> SBVResult ()
    forall a. SVal -> a -> SBVResult a
    SBVResult SVal
    SBit SBV
    cond ()))

      isReady :: forall a. SBV -> SEval SBV a -> SEval SBV (Maybe a)
    isReady SBV
    _ (SBVEval Eval (SBVResult a)
    m) = Eval (SBVResult (Maybe a)) -> SBVEval (Maybe a)
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult (Maybe a)) -> SBVEval (Maybe a))
    -> Eval (SBVResult (Maybe a)) -> SBVEval (Maybe a)
    forall a b. (a -> b) -> a -> b
    $
        Eval (SBVResult a) -> Eval (Maybe (SBVResult a))
    forall a. Eval a -> Eval (Maybe a)
    maybeReady Eval (SBVResult a)
    m Eval (Maybe (SBVResult a))
    -> (Maybe (SBVResult a) -> Eval (SBVResult (Maybe a)))
    -> Eval (SBVResult (Maybe a))
    forall a b. Eval a -> (a -> Eval b) -> Eval b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just SBVResult a
    x  -> SBVResult (Maybe a) -> Eval (SBVResult (Maybe a))
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> SBVResult a -> SBVResult (Maybe a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SBVResult a
    x)
          Maybe (SBVResult a)
    Nothing -> SBVResult (Maybe a) -> Eval (SBVResult (Maybe a))
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe a -> SBVResult (Maybe a)
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe a
    forall a. Maybe a
    Nothing)

      sDelayFill :: forall a.
    SBV
    -> SEval SBV a
    -> Maybe (SEval SBV a)
    -> String
    -> SEval SBV (SEval SBV a)
    sDelayFill SBV
    _ SEval SBV a
    m Maybe (SEval SBV a)
    retry String
    msg = Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a))
    -> Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
    forall a b. (a -> b) -> a -> b
    $
        do Eval (SBVResult a)
    m' <- Eval (SBVResult a)
    -> Maybe (Eval (SBVResult a))
    -> String
    -> Eval (Eval (SBVResult a))
    forall a. Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
    delayFill (SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SEval SBV a
    SBVEval a
    m) (SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval (SBVEval a -> Eval (SBVResult a))
    -> Maybe (SBVEval a) -> Maybe (Eval (SBVResult a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (SEval SBV a)
    Maybe (SBVEval a)
    retry) String
    msg
           SBVResult (SBVEval a) -> Eval (SBVResult (SBVEval a))
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVEval a -> SBVResult (SBVEval a)
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval Eval (SBVResult a)
    m'))

      sSpark :: forall a. SBV -> SEval SBV a -> SEval SBV (SEval SBV a)
    sSpark SBV
    _ SEval SBV a
    m = Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a))
    -> Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
    forall a b. (a -> b) -> a -> b
    $
        do Eval (SBVResult a)
    m' <- Eval (SBVResult a) -> Eval (Eval (SBVResult a))
    forall a. Eval a -> Eval (Eval a)
    evalSpark (SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SEval SBV a
    SBVEval a
    m)
           SBVResult (SBVEval a) -> Eval (SBVResult (SBVEval a))
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVEval a -> SBVResult (SBVEval a)
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval Eval (SBVResult a)
    m'))

      sDeclareHole :: forall a.
    SBV
    -> String -> SEval SBV (SEval SBV a, SEval SBV a -> SEval SBV ())
    sDeclareHole SBV
    _ String
    msg = Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
    -> SBVEval (SBVEval a, SBVEval a -> SBVEval ())
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
     -> SBVEval (SBVEval a, SBVEval a -> SBVEval ()))
    -> Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
    -> SBVEval (SBVEval a, SBVEval a -> SBVEval ())
    forall a b. (a -> b) -> a -> b
    $
        do (Eval (SBVResult a)
    hole, Eval (SBVResult a) -> Eval ()
    fill) <- String -> Eval (Eval (SBVResult a), Eval (SBVResult a) -> Eval ())
    forall a. String -> Eval (Eval a, Eval a -> Eval ())
    blackhole String
    msg
           SBVResult (SBVEval a, SBVEval a -> SBVEval ())
    -> Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((SBVEval a, SBVEval a -> SBVEval ())
    -> SBVResult (SBVEval a, SBVEval a -> SBVEval ())
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval Eval (SBVResult a)
    hole, \SBVEval a
    m -> Eval (SBVResult ()) -> SBVEval ()
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval ((() -> SBVResult ()) -> Eval () -> Eval (SBVResult ())
    forall a b. (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap () -> SBVResult ()
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Eval () -> Eval (SBVResult ())) -> Eval () -> Eval (SBVResult ())
    forall a b. (a -> b) -> a -> b
    $ Eval (SBVResult a) -> Eval ()
    fill (SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SBVEval a
    m))))

      sModifyCallStack :: forall a.
    SBV -> (CallStack -> CallStack) -> SEval SBV a -> SEval SBV a
    sModifyCallStack SBV
    _ CallStack -> CallStack
    f (SBVEval Eval (SBVResult a)
    m) = Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult a) -> SBVEval a)
    -> Eval (SBVResult a) -> SBVEval a
    forall a b. (a -> b) -> a -> b
    $
        (CallStack -> CallStack)
    -> Eval (SBVResult a) -> Eval (SBVResult a)
    forall a. (CallStack -> CallStack) -> Eval a -> Eval a
    modifyCallStack CallStack -> CallStack
    f Eval (SBVResult a)
    m

      sGetCallStack :: SBV -> SEval SBV CallStack
    sGetCallStack SBV
    _ = Eval (SBVResult CallStack) -> SBVEval CallStack
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (CallStack -> SBVResult CallStack
    forall a. a -> SBVResult a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CallStack -> SBVResult CallStack)
    -> Eval CallStack -> Eval (SBVResult CallStack)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval CallStack
    getCallStack)

      mergeEval :: forall a.
    SBV
    -> (SBit SBV -> a -> a -> SEval SBV a)
    -> SBit SBV
    -> SEval SBV a
    -> SEval SBV a
    -> SEval SBV a
    mergeEval SBV
    _sym SBit SBV -> a -> a -> SEval SBV a
    f SBit SBV
    c SEval SBV a
    mx SEval SBV a
    my = Eval (SBVResult a) -> SBVEval a
    forall a. Eval (SBVResult a) -> SBVEval a
    SBVEval (Eval (SBVResult a) -> SBVEval a)
    -> Eval (SBVResult a) -> SBVEval a
    forall a b. (a -> b) -> a -> b
    $
        do SBVResult a
    rx <- SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SEval SBV a
    SBVEval a
    mx
           SBVResult a
    ry <- SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval SEval SBV a
    SBVEval a
    my
           case (SBVResult a
    rx, SBVResult a
    ry) of
             (SBVError EvalErrorEx
    err, SBVError EvalErrorEx
    _) ->
               SBVResult a -> Eval (SBVResult a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVResult a -> Eval (SBVResult a))
    -> SBVResult a -> Eval (SBVResult a)
    forall a b. (a -> b) -> a -> b
    $ EvalErrorEx -> SBVResult a
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err -- arbitrarily choose left error to report
             (SBVError EvalErrorEx
    _, SBVResult SVal
    p a
    y) ->
               SBVResult a -> Eval (SBVResult a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVResult a -> Eval (SBVResult a))
    -> SBVResult a -> Eval (SBVResult a)
    forall a b. (a -> b) -> a -> b
    $ SVal -> a -> SBVResult a
    forall a. SVal -> a -> SBVResult a
    SBVResult (SVal -> SVal -> SVal
    svAnd (SVal -> SVal
    svNot SVal
    SBit SBV
    c) SVal
    p) a
    y
             (SBVResult SVal
    p a
    x, SBVError EvalErrorEx
    _) ->
               SBVResult a -> Eval (SBVResult a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVResult a -> Eval (SBVResult a))
    -> SBVResult a -> Eval (SBVResult a)
    forall a b. (a -> b) -> a -> b
    $ SVal -> a -> SBVResult a
    forall a. SVal -> a -> SBVResult a
    SBVResult (SVal -> SVal -> SVal
    svAnd SVal
    SBit SBV
    c SVal
    p) a
    x
             (SBVResult SVal
    px a
    x, SBVResult SVal
    py a
    y) ->
               do SBVResult a
    zr <- SBVEval a -> Eval (SBVResult a)
    forall a. SBVEval a -> Eval (SBVResult a)
    sbvEval (SBit SBV -> a -> a -> SEval SBV a
    f SBit SBV
    c a
    x a
    y)
                  case SBVResult a
    zr of
                    SBVError EvalErrorEx
    err -> SBVResult a -> Eval (SBVResult a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVResult a -> Eval (SBVResult a))
    -> SBVResult a -> Eval (SBVResult a)
    forall a b. (a -> b) -> a -> b
    $ EvalErrorEx -> SBVResult a
    forall a. EvalErrorEx -> SBVResult a
    SBVError EvalErrorEx
    err
                    SBVResult SVal
    pz a
    z ->
                      SBVResult a -> Eval (SBVResult a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBVResult a -> Eval (SBVResult a))
    -> SBVResult a -> Eval (SBVResult a)
    forall a b. (a -> b) -> a -> b
    $ SVal -> a -> SBVResult a
    forall a. SVal -> a -> SBVResult a
    SBVResult (SVal -> SVal -> SVal
    svAnd (SVal -> SVal -> SVal -> SVal
    svIte SVal
    SBit SBV
    c SVal
    px SVal
    py) SVal
    pz) a
    z

      wordLen :: SBV -> SWord SBV -> Integer
    wordLen SBV
    _ SWord SBV
    v = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    v)
      wordAsChar :: SBV -> SWord SBV -> Maybe Char
    wordAsChar SBV
    _ SWord SBV
    v = Integer -> Char
    integerToChar (Integer -> Char) -> Maybe Integer -> Maybe Char
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SVal -> Maybe Integer
    svAsInteger SVal
    SWord SBV
    v

      iteBit :: SBV -> SBit SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
    iteBit SBV
    _ SBit SBV
    b SBit SBV
    x SBit SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge Kind
    KBool Bool
    True SVal
    SBit SBV
    b SVal
    SBit SBV
    x SVal
    SBit SBV
    y
      iteWord :: SBV -> SBit SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    iteWord SBV
    _ SBit SBV
    b SWord SBV
    x SWord SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    SWord SBV
    x) Bool
    True SVal
    SBit SBV
    b SVal
    SWord SBV
    x SVal
    SWord SBV
    y
      iteInteger :: SBV
    -> SBit SBV
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    iteInteger SBV
    _ SBit SBV
    b SInteger SBV
    x SInteger SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge Kind
    KUnbounded Bool
    True SVal
    SBit SBV
    b SVal
    SInteger SBV
    x SVal
    SInteger SBV
    y

      bitAsLit :: SBV -> SBit SBV -> Maybe Bool
    bitAsLit SBV
    _ SBit SBV
    b = SVal -> Maybe Bool
    svAsBool SVal
    SBit SBV
    b
      wordAsLit :: SBV -> SWord SBV -> Maybe (Integer, Integer)
    wordAsLit SBV
    _ SWord SBV
    w =
        case SVal -> Maybe Integer
    svAsInteger SVal
    SWord SBV
    w of
          Just Integer
    x -> (Integer, Integer) -> Maybe (Integer, Integer)
    forall a. a -> Maybe a
    Just (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    w), Integer
    x)
          Maybe Integer
    Nothing -> Maybe (Integer, Integer)
    forall a. Maybe a
    Nothing
      integerAsLit :: SBV -> SInteger SBV -> Maybe Integer
    integerAsLit SBV
    _ SInteger SBV
    v = SVal -> Maybe Integer
    svAsInteger SVal
    SInteger SBV
    v

      bitLit :: SBV -> Bool -> SBit SBV
    bitLit SBV
    _ Bool
    b     = Bool -> SVal
    svBool Bool
    b
      wordLit :: SBV -> Integer -> Integer -> SEval SBV (SWord SBV)
    wordLit SBV
    _ Integer
    n Integer
    x  = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Int -> Integer -> SWord SBV
    literalSWord (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n) Integer
    x
      integerLit :: SBV -> Integer -> SEval SBV (SInteger SBV)
    integerLit SBV
    _ Integer
    x = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    x

      bitEq :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
    bitEq  SBV
    _ SBit SBV
    x SBit SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svEqual SVal
    SBit SBV
    x SVal
    SBit SBV
    y
      bitOr :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
    bitOr  SBV
    _ SBit SBV
    x SBit SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svOr SVal
    SBit SBV
    x SVal
    SBit SBV
    y
      bitAnd :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
    bitAnd SBV
    _ SBit SBV
    x SBit SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svAnd SVal
    SBit SBV
    x SVal
    SBit SBV
    y
      bitXor :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
    bitXor SBV
    _ SBit SBV
    x SBit SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svXOr SVal
    SBit SBV
    x SVal
    SBit SBV
    y
      bitComplement :: SBV -> SBit SBV -> SEval SBV (SBit SBV)
    bitComplement SBV
    _ SBit SBV
    x = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal
    svNot SVal
    SBit SBV
    x

      wordBit :: SBV -> SWord SBV -> Integer -> SEval SBV (SBit SBV)
    wordBit SBV
    _ SWord SBV
    x Integer
    idx = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> Int -> SVal
    svTestBit SVal
    SWord SBV
    x (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    idx)

      wordUpdate :: SBV -> SWord SBV -> Integer -> SBit SBV -> SEval SBV (SWord SBV)
    wordUpdate SBV
    _ SWord SBV
    x Integer
    idx SBit SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    SWord SBV
    x) Bool
    False SVal
    SBit SBV
    b SVal
    wtrue SVal
    wfalse
        where
         i' :: Int
    i' = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    idx
         wtrue :: SVal
    wtrue  = SVal
    SWord SBV
    x SVal -> SVal -> SVal
    `svOr`  Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    SWord SBV
    x) (Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    i' :: Integer)
         wfalse :: SVal
    wfalse = SVal
    SWord SBV
    x SVal -> SVal -> SVal
    `svAnd` Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    SWord SBV
    x) (Integer -> Integer
    forall a. Bits a => a -> a
    complement (Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    i' :: Integer))

      packWord :: SBV -> [SBit SBV] -> SEval SBV (SWord SBV)
    packWord SBV
    _ [SBit SBV]
    bs  = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! [SBit SBV] -> SWord SBV
    packSBV [SBit SBV]
    bs
      unpackWord :: SBV -> SWord SBV -> SEval SBV [SBit SBV]
    unpackWord SBV
    _ SWord SBV
    x = [SVal] -> SBVEval [SVal]
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([SVal] -> SBVEval [SVal]) -> [SVal] -> SBVEval [SVal]
    forall a b. (a -> b) -> a -> b
    $! SWord SBV -> [SBit SBV]
    unpackSBV SWord SBV
    x

      wordEq :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
    wordEq SBV
    _ SWord SBV
    x SWord SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svEqual SVal
    SWord SBV
    x SVal
    SWord SBV
    y
      wordLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
    wordLessThan SBV
    _ SWord SBV
    x SWord SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svLessThan SVal
    SWord SBV
    x SVal
    SWord SBV
    y
      wordGreaterThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
    wordGreaterThan SBV
    _ SWord SBV
    x SWord SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svGreaterThan SVal
    SWord SBV
    x SVal
    SWord SBV
    y

      wordSignedLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
    wordSignedLessThan SBV
    _ SWord SBV
    x SWord SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svLessThan SVal
    sx SVal
    sy
        where sx :: SVal
    sx = SVal -> SVal
    svSign SVal
    SWord SBV
    x
              sy :: SVal
    sy = SVal -> SVal
    svSign SVal
    SWord SBV
    y

      joinWord :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    joinWord SBV
    _ SWord SBV
    x SWord SBV
    y = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svJoin SVal
    SWord SBV
    x SVal
    SWord SBV
    y

      splitWord :: SBV
    -> Integer
    -> Integer
    -> SWord SBV
    -> SEval SBV (SWord SBV, SWord SBV)
    splitWord SBV
    _ Integer
    _leftW Integer
    rightW SWord SBV
    w = (SVal, SVal) -> SBVEval (SVal, SVal)
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
        ( Int -> Int -> SVal -> SVal
    svExtract (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    rightW) SVal
    SWord SBV
    w
        , Int -> Int -> SVal -> SVal
    svExtract (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    rightW Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Int
    0 SVal
    SWord SBV
    w
        )

      extractWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV)
    extractWord SBV
    _ Integer
    len Integer
    start SWord SBV
    w =
        SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Int -> Int -> SVal -> SVal
    svExtract (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    start Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    start) SVal
    SWord SBV
    w

      wordAnd :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordAnd SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svAnd SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordOr :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordOr  SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svOr SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordXor :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordXor SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svXOr SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordComplement :: SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordComplement SBV
    _ SWord SBV
    a = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal
    svNot SVal
    SWord SBV
    a

      wordPlus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordPlus  SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svPlus SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordMinus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordMinus SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svMinus SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordMult :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordMult  SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svTimes SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordNegate :: SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordNegate SBV
    _ SWord SBV
    a  = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal
    svUNeg SVal
    SWord SBV
    a

      wordShiftLeft :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordShiftLeft SBV
    _ SWord SBV
    a SWord SBV
    b   = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    shl SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordShiftRight :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordShiftRight SBV
    _ SWord SBV
    a SWord SBV
    b  = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    lshr SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordRotateLeft :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordRotateLeft SBV
    _ SWord SBV
    a SWord SBV
    b  = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    SBV.svRotateLeft SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordRotateRight :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordRotateRight SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    SBV.svRotateRight SVal
    SWord SBV
    a SVal
    SWord SBV
    b
      wordSignedShiftRight :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordSignedShiftRight SBV
    _ SWord SBV
    a SWord SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    ashr SVal
    SWord SBV
    a SVal
    SWord SBV
    b

      wordDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordDiv SBV
    sym SWord SBV
    a SWord SBV
    b =
        do let z :: SWord SBV
    z = Int -> Integer -> SWord SBV
    literalSWord (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    b) Integer
    0
           SBV -> SBit SBV -> EvalError -> SEval SBV ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition SBV
    sym (SVal -> SVal
    svNot (SVal -> SVal -> SVal
    svEqual SVal
    SWord SBV
    b SVal
    SWord SBV
    z)) EvalError
    DivideByZero
           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svQuot SVal
    SWord SBV
    a SVal
    SWord SBV
    b

      wordMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordMod SBV
    sym SWord SBV
    a SWord SBV
    b =
        do let z :: SWord SBV
    z = Int -> Integer -> SWord SBV
    literalSWord (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    b) Integer
    0
           SBV -> SBit SBV -> EvalError -> SEval SBV ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition SBV
    sym (SVal -> SVal
    svNot (SVal -> SVal -> SVal
    svEqual SVal
    SWord SBV
    b SVal
    SWord SBV
    z)) EvalError
    DivideByZero
           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svRem SVal
    SWord SBV
    a SVal
    SWord SBV
    b

      wordSignedDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordSignedDiv SBV
    sym SWord SBV
    a SWord SBV
    b =
        do let z :: SWord SBV
    z = Int -> Integer -> SWord SBV
    literalSWord (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    b) Integer
    0
           SBV -> SBit SBV -> EvalError -> SEval SBV ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition SBV
    sym (SVal -> SVal
    svNot (SVal -> SVal -> SVal
    svEqual SVal
    SWord SBV
    b SVal
    SWord SBV
    z)) EvalError
    DivideByZero
           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SWord SBV -> SWord SBV -> SWord SBV
    signedQuot SWord SBV
    a SWord SBV
    b

      wordSignedMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordSignedMod SBV
    sym SWord SBV
    a SWord SBV
    b =
        do let z :: SWord SBV
    z = Int -> Integer -> SWord SBV
    literalSWord (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    SWord SBV
    b) Integer
    0
           SBV -> SBit SBV -> EvalError -> SEval SBV ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition SBV
    sym (SVal -> SVal
    svNot (SVal -> SVal -> SVal
    svEqual SVal
    SWord SBV
    b SVal
    SWord SBV
    z)) EvalError
    DivideByZero
           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SWord SBV -> SWord SBV -> SWord SBV
    signedRem SWord SBV
    a SWord SBV
    b

      wordLg2 :: SBV -> SWord SBV -> SEval SBV (SWord SBV)
    wordLg2 SBV
    _ SWord SBV
    a = SWord SBV -> SEval SBV (SWord SBV)
    sLg2 SWord SBV
    a

      wordToInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV)
    wordToInt SBV
    _ SWord SBV
    x = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SWord SBV -> SInteger SBV
    svToInteger SWord SBV
    x
      wordToSignedInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV)
    wordToSignedInt SBV
    _ SWord SBV
    x = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SWord SBV -> SInteger SBV
    svToInteger (SVal -> SVal
    svSign SVal
    SWord SBV
    x)
      wordFromInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV)
    wordFromInt SBV
    _ Integer
    w SInteger SBV
    i = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Integer -> SInteger SBV -> SWord SBV
    svFromInteger Integer
    w SInteger SBV
    i

      intEq :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
    intEq SBV
    _ SInteger SBV
    a SInteger SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svEqual SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b
      intLessThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
    intLessThan SBV
    _ SInteger SBV
    a SInteger SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svLessThan SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b
      intGreaterThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
    intGreaterThan SBV
    _ SInteger SBV
    a SInteger SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svGreaterThan SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b

      intPlus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    intPlus  SBV
    _ SInteger SBV
    a SInteger SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svPlus SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b
      intMinus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    intMinus SBV
    _ SInteger SBV
    a SInteger SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svMinus SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b
      intMult :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    intMult  SBV
    _ SInteger SBV
    a SInteger SBV
    b = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svTimes SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b
      intNegate :: SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    intNegate SBV
    _ SInteger SBV
    a  = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal
    SBV.svUNeg SVal
    SInteger SBV
    a

      intDiv :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    intDiv SBV
    sym SInteger SBV
    a SInteger SBV
    b =
        do let z :: SVal
    z = Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    0
           SBV -> SBit SBV -> EvalError -> SEval SBV ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition SBV
    sym (SVal -> SVal
    svNot (SVal -> SVal -> SVal
    svEqual SVal
    SInteger SBV
    b SVal
    z)) EvalError
    DivideByZero
           let p :: SVal
    p = SVal -> SVal -> SVal
    svLessThan SVal
    z SVal
    SInteger SBV
    b
           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge Kind
    KUnbounded Bool
    True SVal
    p (SVal -> SVal -> SVal
    svQuot SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b) (SVal -> SVal -> SVal
    svQuot (SVal -> SVal
    svUNeg SVal
    SInteger SBV
    a) (SVal -> SVal
    svUNeg SVal
    SInteger SBV
    b))
      intMod :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    intMod SBV
    sym SInteger SBV
    a SInteger SBV
    b =
        do let z :: SVal
    z = Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    0
           SBV -> SBit SBV -> EvalError -> SEval SBV ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition SBV
    sym (SVal -> SVal
    svNot (SVal -> SVal -> SVal
    svEqual SVal
    SInteger SBV
    b SVal
    z)) EvalError
    DivideByZero
           let p :: SVal
    p = SVal -> SVal -> SVal
    svLessThan SVal
    z SVal
    SInteger SBV
    b
           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge Kind
    KUnbounded Bool
    True SVal
    p (SVal -> SVal -> SVal
    svRem SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b) (SVal -> SVal
    svUNeg (SVal -> SVal -> SVal
    svRem (SVal -> SVal
    svUNeg SVal
    SInteger SBV
    a) (SVal -> SVal
    svUNeg SVal
    SInteger SBV
    b)))

      -- NB, we don't do reduction here
      intToZn :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    intToZn SBV
    _ Integer
    _m SInteger SBV
    a = SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SVal
    SInteger SBV
    a

      znToInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    znToInt SBV
    _ Integer
    0 SInteger SBV
    _ = String -> [String] -> SBVEval SVal
    forall a. String -> [String] -> a
    evalPanic String
    "znToInt" [String
    "0 modulus not allowed"]
      znToInt SBV
    _ Integer
    m SInteger SBV
    a =
        do let m' :: SVal
    m' = Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    m
           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $! SVal -> SVal -> SVal
    svRem SVal
    SInteger SBV
    a SVal
    m'

      znEq :: SBV
    -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
    znEq SBV
    _ Integer
    0 SInteger SBV
    _ SInteger SBV
    _ = String -> [String] -> SBVEval SVal
    forall a. String -> [String] -> a
    evalPanic String
    "znEq" [String
    "0 modulus not allowed"]
      znEq SBV
    sym Integer
    m SInteger SBV
    a SInteger SBV
    b = SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
    svDivisible SBV
    sym Integer
    m (SVal -> SVal -> SVal
    SBV.svMinus SVal
    SInteger SBV
    a SVal
    SInteger SBV
    b)

      znPlus :: SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    znPlus  SBV
    sym Integer
    m SInteger SBV
    a SInteger SBV
    b = SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    sModAdd SBV
    sym Integer
    m SInteger SBV
    a SInteger SBV
    b
      znMinus :: SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    znMinus SBV
    sym Integer
    m SInteger SBV
    a SInteger SBV
    b = SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    sModSub SBV
    sym Integer
    m SInteger SBV
    a SInteger SBV
    b
      znMult :: SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    znMult  SBV
    sym Integer
    m SInteger SBV
    a SInteger SBV
    b = SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    sModMult SBV
    sym Integer
    m SInteger SBV
    a SInteger SBV
    b
      znNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    znNegate SBV
    sym Integer
    m SInteger SBV
    a  = SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModNegate SBV
    sym Integer
    m SInteger SBV
    a
      znRecip :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    znRecip = SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModRecip

      fpAsLit :: SBV -> SFloat SBV -> Maybe BF
    fpAsLit SBV
    _ SFloat SBV
    _               = Maybe BF
    forall a. Maybe a
    Nothing
      iteFloat :: SBV
    -> SBit SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
    iteFloat SBV
    _ SBit SBV
    _ SFloat SBV
    _ SFloat SBV
    _          = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "iteFloat"
      fpNaN :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV)
    fpNaN SBV
    _ Integer
    _ Integer
    _               = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpNaN"
      fpPosInf :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV)
    fpPosInf SBV
    _ Integer
    _ Integer
    _            = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpPosInf"
      fpExactLit :: SBV -> BF -> SEval SBV (SFloat SBV)
    fpExactLit SBV
    _ BF
    _            = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpExactLit"
      fpLit :: SBV -> Integer -> Integer -> Rational -> SEval SBV (SFloat SBV)
    fpLit SBV
    _ Integer
    _ Integer
    _ Rational
    _             = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpLit"
      fpLogicalEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpLogicalEq SBV
    _ SFloat SBV
    _ SFloat SBV
    _         = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpLogicalEq"
      fpEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpEq SBV
    _ SFloat SBV
    _ SFloat SBV
    _                = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpEq"
      fpLessThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpLessThan SBV
    _ SFloat SBV
    _ SFloat SBV
    _          = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpLessThan"
      fpGreaterThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpGreaterThan SBV
    _ SFloat SBV
    _ SFloat SBV
    _       = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpGreaterThan"
      fpPlus :: FPArith2 SBV
    fpPlus SBV
    _ SWord SBV
    _ SFloat SBV
    _ SFloat SBV
    _            = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpPlus"
      fpMinus :: FPArith2 SBV
    fpMinus SBV
    _ SWord SBV
    _ SFloat SBV
    _ SFloat SBV
    _           = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpMinus"
      fpMult :: FPArith2 SBV
    fpMult SBV
    _ SWord SBV
    _ SFloat SBV
    _ SFloat SBV
    _            = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpMult"
      fpDiv :: FPArith2 SBV
    fpDiv SBV
    _ SWord SBV
    _ SFloat SBV
    _ SFloat SBV
    _             = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpDiv"
      fpAbs :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
    fpAbs SBV
    _ SFloat SBV
    _                 = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpAbs"
      fpSqrt :: SBV -> SWord SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
    fpSqrt SBV
    _ SWord SBV
    _ SFloat SBV
    _              = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpSqrt"
      fpFMA :: SBV
    -> SWord SBV
    -> SFloat SBV
    -> SFloat SBV
    -> SFloat SBV
    -> SEval SBV (SFloat SBV)
    fpFMA SBV
    _ SWord SBV
    _ SFloat SBV
    _ SFloat SBV
    _ SFloat SBV
    _           = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpFMA"
      fpNeg :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
    fpNeg SBV
    _ SFloat SBV
    _                 = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpNeg"
      fpFromInteger :: SBV
    -> Integer
    -> Integer
    -> SWord SBV
    -> SInteger SBV
    -> SEval SBV (SFloat SBV)
    fpFromInteger SBV
    _ Integer
    _ Integer
    _ SWord SBV
    _ SInteger SBV
    _   = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpFromInteger"
      fpToInteger :: SBV
    -> String -> SWord SBV -> SFloat SBV -> SEval SBV (SInteger SBV)
    fpToInteger SBV
    _ String
    _ SWord SBV
    _ SFloat SBV
    _       = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpToInteger"
      fpIsZero :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpIsZero SBV
    _ SFloat SBV
    _              = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpIsZero"
      fpIsInf :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpIsInf SBV
    _ SFloat SBV
    _               = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpIsInf"
      fpIsNeg :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpIsNeg SBV
    _ SFloat SBV
    _               = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpIsNeg"
      fpIsNaN :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpIsNaN SBV
    _ SFloat SBV
    _               = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpIsNaN"
      fpIsNorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpIsNorm SBV
    _ SFloat SBV
    _              = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpIsNorm"
      fpIsSubnorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
    fpIsSubnorm SBV
    _ SFloat SBV
    _           = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpIsSubnorm"
      fpToBits :: SBV -> SFloat SBV -> SEval SBV (SWord SBV)
    fpToBits SBV
    _ SFloat SBV
    _              = String -> SEval SBV SVal
    forall a. String -> SEval SBV a
    unsupported String
    "fpToBits"
      fpFromBits :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SFloat SBV)
    fpFromBits SBV
    _ Integer
    _ Integer
    _ SWord SBV
    _        = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpFromBits"
      fpToRational :: SBV -> SFloat SBV -> SEval SBV (SRational SBV)
    fpToRational SBV
    _ SFloat SBV
    _          = String -> SEval SBV (SRational SBV)
    forall a. String -> SEval SBV a
    unsupported String
    "fpToRational"
      fpFromRational :: SBV
    -> Integer
    -> Integer
    -> SWord SBV
    -> SRational SBV
    -> SEval SBV (SFloat SBV)
    fpFromRational SBV
    _ Integer
    _ Integer
    _ SWord SBV
    _ SRational SBV
    _  = String -> SEval SBV ()
    forall a. String -> SEval SBV a
    unsupported String
    "fpFromRational"

    unsupported :: String -> SEval SBV a
    unsupported :: forall a. String -> SEval SBV a
    unsupported String
    x = IO a -> SBVEval a
    forall a. IO a -> SBVEval a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Unsupported -> IO a
    forall a e. Exception e => e -> a
    X.throw (String -> Unsupported
    UnsupportedSymbolicOp String
    x))

    svToInteger :: SWord SBV -> SInteger SBV
    svToInteger :: SWord SBV -> SInteger SBV
    svToInteger SWord SBV
    w =
      case SVal -> Maybe Integer
    svAsInteger SVal
    SWord SBV
    w of
        Maybe Integer
    Nothing -> Kind -> SVal -> SVal
    svFromIntegral Kind
    KUnbounded SVal
    SWord SBV
    w
        Just Integer
    x  -> Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    x

    svFromInteger :: Integer -> SInteger SBV -> SWord SBV
    svFromInteger :: Integer -> SInteger SBV -> SWord SBV
    svFromInteger Integer
    0 SInteger SBV
    _ = Int -> Integer -> SWord SBV
    literalSWord Int
    0 Integer
    0
    svFromInteger Integer
    n SInteger SBV
    i =
      case SVal -> Maybe Integer
    svAsInteger SVal
    SInteger SBV
    i of
        Maybe Integer
    Nothing -> Kind -> SVal -> SVal
    svFromIntegral (Bool -> Int -> Kind
    KBounded Bool
    False (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)) SVal
    SInteger SBV
    i
        Just Integer
    x  -> Int -> Integer -> SWord SBV
    literalSWord (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n) Integer
    x

    -- Errors ----------------------------------------------------------------------

    evalPanic :: String -> [String] -> a
    evalPanic :: forall a. String -> [String] -> a
    evalPanic String
    cxt = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic (String
    "[SBV] " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cxt)

    sModAdd :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModAdd :: SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    sModAdd SBV
    _ Integer
    0 SInteger SBV
    _ SInteger SBV
    _ = String -> [String] -> SBVEval SVal
    forall a. String -> [String] -> a
    evalPanic String
    "sModAdd" [String
    "0 modulus not allowed"]
    sModAdd SBV
    sym Integer
    modulus SInteger SBV
    x SInteger SBV
    y =
      case (SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    x, SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    y) of
        (Just Integer
    i, Just Integer
    j) -> SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym ((Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    j) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    modulus)
        (Maybe Integer, Maybe Integer)
    _                -> SVal -> SEval SBV SVal
    forall a. a -> SEval SBV a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SEval SBV SVal) -> SVal -> SEval SBV SVal
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    SBV.svPlus SVal
    SInteger SBV
    x SVal
    SInteger SBV
    y

    sModSub :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModSub :: SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    sModSub SBV
    _ Integer
    0 SInteger SBV
    _ SInteger SBV
    _ = String -> [String] -> SBVEval SVal
    forall a. String -> [String] -> a
    evalPanic String
    "sModSub" [String
    "0 modulus not allowed"]
    sModSub SBV
    sym Integer
    modulus SInteger SBV
    x SInteger SBV
    y =
      case (SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    x, SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    y) of
        (Just Integer
    i, Just Integer
    j) -> SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym ((Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    j) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    modulus)
        (Maybe Integer, Maybe Integer)
    _                -> SVal -> SEval SBV SVal
    forall a. a -> SEval SBV a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SEval SBV SVal) -> SVal -> SEval SBV SVal
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    SBV.svMinus SVal
    SInteger SBV
    x SVal
    SInteger SBV
    y

    sModNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModNegate SBV
    _ Integer
    0 SInteger SBV
    _ = String -> [String] -> SBVEval SVal
    forall a. String -> [String] -> a
    evalPanic String
    "sModNegate" [String
    "0 modulus not allowed"]
    sModNegate SBV
    sym Integer
    modulus SInteger SBV
    x =
      case SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    x of
        Just Integer
    i -> SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym ((Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    i) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    modulus)
        Maybe Integer
    _      -> SVal -> SEval SBV SVal
    forall a. a -> SEval SBV a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SEval SBV SVal) -> SVal -> SEval SBV SVal
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal
    SBV.svUNeg SVal
    SInteger SBV
    x

    sModMult :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModMult :: SBV
    -> Integer
    -> SInteger SBV
    -> SInteger SBV
    -> SEval SBV (SInteger SBV)
    sModMult SBV
    _ Integer
    0 SInteger SBV
    _ SInteger SBV
    _ = String -> [String] -> SBVEval SVal
    forall a. String -> [String] -> a
    evalPanic String
    "sModMult" [String
    "0 modulus not allowed"]
    sModMult SBV
    sym Integer
    modulus SInteger SBV
    x SInteger SBV
    y =
      case (SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    x, SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    y) of
        (Just Integer
    i, Just Integer
    j) -> SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym ((Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    j) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    modulus)
        (Maybe Integer, Maybe Integer)
    _                -> SVal -> SEval SBV SVal
    forall a. a -> SEval SBV a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SEval SBV SVal) -> SVal -> SEval SBV SVal
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    SBV.svTimes SVal
    SInteger SBV
    x SVal
    SInteger SBV
    y

    -- Create a fresh constant and assert that it is the
    -- multiplicitive inverse of x; return the constant.
    -- Such an inverse must exist under the precondition
    -- that the modulus is prime and the input is nonzero.
    sModRecip ::
      SBV ->
      Integer {- ^ modulus: must be prime -} ->
      SInteger SBV ->
      SEval SBV (SInteger SBV)
    sModRecip :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
    sModRecip SBV
    _sym Integer
    0 SInteger SBV
    _ = String -> [String] -> SBVEval SVal
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "sModRecip" [String
    "0 modulus not allowed"]
    sModRecip SBV
    sym Integer
    m SInteger SBV
    x
      -- If the input is concrete, evaluate the answer
      | Just Integer
    xi <- SVal -> Maybe Integer
    svAsInteger SVal
    SInteger SBV
    x
      = case Integer -> Integer -> Maybe Integer
    Integer.integerRecipMod Integer
    xi Integer
    m of
          Just Integer
    r  -> SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym Integer
    r
          Maybe Integer
    Nothing -> SBV -> EvalError -> SEval SBV SVal
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. SBV -> EvalError -> SEval SBV a
    raiseError SBV
    sym EvalError
    DivideByZero

      -- If the input is symbolic, create a new symbolic constant
      -- and assert that it is the desired multiplicitive inverse.
      -- Such an inverse will exist under the precondition that
      -- the modulus is prime, and as long as the input is nonzero.
      | Bool
    otherwise
      = do SVal
    divZero <- SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
    svDivisible SBV
    sym Integer
    m SInteger SBV
    x
           SBV -> SBit SBV -> EvalError -> SEval SBV ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition SBV
    sym (SVal -> SVal
    svNot SVal
    divZero) EvalError
    DivideByZero

           SVal
    z <- IO SVal -> SBVEval SVal
    forall a. IO a -> SBVEval a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (SBV -> IO (SInteger SBV)
    freshSInteger_ SBV
    sym)
           let xz :: SVal
    xz = SVal -> SVal -> SVal
    svTimes SVal
    SInteger SBV
    x SVal
    z
           SVal
    rel <- SBV
    -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
    forall sym.
    Backend sym =>
    sym
    -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    znEq SBV
    sym Integer
    m SVal
    SInteger SBV
    xz (Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    1)
           let range :: SVal
    range = SVal -> SVal -> SVal
    svAnd (SVal -> SVal -> SVal
    svLessThan (Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    0) SVal
    z)
                             (SVal -> SVal -> SVal
    svLessThan SVal
    z (Kind -> Integer -> SVal
    svInteger Kind
    KUnbounded Integer
    m))
           IO () -> SBVEval ()
    forall a. IO a -> SBVEval a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (SBV -> SVal -> IO ()
    addDefEqn SBV
    sym (SVal -> SVal -> SVal
    svAnd SVal
    range (SVal -> SVal -> SVal
    svOr SVal
    divZero SVal
    rel)))

           SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SVal
    z

    -- | Ceiling (log_2 x)
    sLg2 :: SWord SBV -> SEval SBV (SWord SBV)
    sLg2 :: SWord SBV -> SEval SBV (SWord SBV)
    sLg2 SWord SBV
    x = SWord SBV -> SEval SBV (SWord SBV)
    forall a. a -> SEval SBV a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SWord SBV -> SEval SBV (SWord SBV))
    -> SWord SBV -> SEval SBV (SWord SBV)
    forall a b. (a -> b) -> a -> b
    $ Int -> SVal
    go Int
    0
      where
        lit :: Integer -> SWord SBV
    lit Integer
    n = Int -> Integer -> SWord SBV
    literalSWord (SVal -> Int
    forall a. HasKind a => a -> Int
    SBV.intSizeOf SVal
    SWord SBV
    x) Integer
    n
        go :: Int -> SVal
    go Int
    i | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < SVal -> Int
    forall a. HasKind a => a -> Int
    SBV.intSizeOf SVal
    SWord SBV
    x = SVal -> SVal -> SVal -> SVal
    SBV.svIte (SVal -> SVal -> SVal
    SBV.svLessEq SVal
    SWord SBV
    x (Integer -> SWord SBV
    lit (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    i))) (Integer -> SWord SBV
    lit (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    i)) (Int -> SVal
    go (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1))
             | Bool
    otherwise           = Integer -> SWord SBV
    lit (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    i)

    svDivisible :: SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
    svDivisible :: SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
    svDivisible SBV
    sym Integer
    m SInteger SBV
    x =
      do SVal
    m' <- SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym Integer
    m
         SVal
    z  <- SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym Integer
    0
         SVal -> SBVEval SVal
    forall a. a -> SBVEval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    SBV.svEqual (SVal -> SVal -> SVal
    SBV.svRem SVal
    SInteger SBV
    x SVal
    m') SVal
    z

    signedQuot :: SWord SBV -> SWord SBV -> SWord SBV
    signedQuot :: SWord SBV -> SWord SBV -> SWord SBV
    signedQuot SWord SBV
    x SWord SBV
    y = SVal -> SVal
    SBV.svUnsign (SVal -> SVal -> SVal
    SBV.svQuot (SVal -> SVal
    SBV.svSign SVal
    SWord SBV
    x) (SVal -> SVal
    SBV.svSign SVal
    SWord SBV
    y))

    signedRem :: SWord SBV -> SWord SBV -> SWord SBV
    signedRem :: SWord SBV -> SWord SBV -> SWord SBV
    signedRem SWord SBV
    x SWord SBV
    y = SVal -> SVal
    SBV.svUnsign (SVal -> SVal -> SVal
    SBV.svRem (SVal -> SVal
    SBV.svSign SVal
    SWord SBV
    x) (SVal -> SVal
    SBV.svSign SVal
    SWord SBV
    y))

    ashr :: SVal -> SVal -> SVal
    ashr :: SVal -> SVal -> SVal
    ashr SVal
    x SVal
    idx =
      case SVal -> Maybe Integer
    SBV.svAsInteger SVal
    idx of
        Just Integer
    i  -> SVal -> SVal
    SBV.svUnsign (SVal -> Int -> SVal
    SBV.svShr (SVal -> SVal
    SBV.svSign SVal
    x) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i))
        Maybe Integer
    Nothing -> SVal -> SVal
    SBV.svUnsign (SVal -> SVal -> SVal
    SBV.svShiftRight (SVal -> SVal
    SBV.svSign SVal
    x) SVal
    idx)

    lshr :: SVal -> SVal -> SVal
    lshr :: SVal -> SVal -> SVal
    lshr SVal
    x SVal
    idx =
      case SVal -> Maybe Integer
    SBV.svAsInteger SVal
    idx of
        Just Integer
    i -> SVal -> Int -> SVal
    SBV.svShr SVal
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i)
        Maybe Integer
    Nothing -> SVal -> SVal -> SVal
    SBV.svShiftRight SVal
    x SVal
    idx

    shl :: SVal -> SVal -> SVal
    shl :: SVal -> SVal -> SVal
    shl SVal
    x SVal
    idx =
      case SVal -> Maybe Integer
    SBV.svAsInteger SVal
    idx of
        Just Integer
    i  -> SVal -> Int -> SVal
    SBV.svShl SVal
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i)
        Maybe Integer
    Nothing -> SVal -> SVal -> SVal
    SBV.svShiftLeft SVal
    x SVal
    idx