    -- |
    -- Module      :  Cryptol.Backend.What4
    -- Copyright   :  (c) 2020 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com

    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE ViewPatterns #-}
    module Cryptol.Backend.What4 where

    import qualified Control.Exception as X
    import           Control.Concurrent.MVar
    import           Control.Monad (foldM,ap,liftM)
    import           Control.Monad.IO.Class
    import           Data.Bits (bit)
    import qualified Data.BitVector.Sized as BV
    import           Data.List
    import           Data.Map (Map)
    import           Data.Set (Set)
    import           Data.Text (Text)
    import           Data.Parameterized.NatRepr
    import           Data.Parameterized.Some

    import qualified GHC.Num.Compat as Integer

    import qualified What4.Interface as W4
    import qualified What4.SWord as SW
    import qualified What4.SFloat as FP

    import Cryptol.Backend
    import Cryptol.Backend.FloatHelpers
    import Cryptol.Backend.Monad
       ( Eval(..), EvalError(..), EvalErrorEx(..)
       , Unsupported(..), delayFill, blackhole, evalSpark
       , modifyCallStack, getCallStack, maybeReady
       )
    import Cryptol.Utils.Panic

    data What4 sym =
      What4
      { forall sym. What4 sym -> sym
    w4  :: sym
      , forall sym. What4 sym -> MVar (Pred sym)
    w4defs :: MVar (W4.Pred sym)
      , forall sym. What4 sym -> MVar (What4FunCache sym)
    w4funs :: MVar (What4FunCache sym)
      , forall sym. What4 sym -> MVar (Set Text)
    w4uninterpWarns :: MVar (Set Text)
      }

    type What4FunCache sym = Map Text (SomeSymFn sym)

    data SomeSymFn sym =
      forall args ret. SomeSymFn (W4.SymFn sym args ret)

    {- | This is the monad used for symbolic evaluation. It adds to
    aspects to 'Eval'---'WConn' keeps track of the backend and collects
    definitional predicates, and 'W4Eval` adds support for partially
    defined values -}
    newtype W4Eval sym a = W4Eval { forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
    evalPartial :: W4Conn sym (W4Result sym a) }

    {- | This layer has the symbolic back-end, and can keep track of definitional
    predicates used when working with uninterpreted constants defined
    via a property. -}
    newtype W4Conn sym a = W4Conn { forall sym a. W4Conn sym a -> sym -> Eval a
    evalConn :: sym -> Eval a }

    -- | The symbolic value we computed.
    data W4Result sym a
      = W4Error !EvalErrorEx
        -- ^ A malformed value

      | W4Result !(W4.Pred sym) !a
        -- ^ safety predicate and result: the result only makes sense when
        -- the predicate holds.
     deriving (forall a b. (a -> b) -> W4Result sym a -> W4Result sym b)
    -> (forall a b. a -> W4Result sym b -> W4Result sym a)
    -> Functor (W4Result sym)
    forall a b. a -> W4Result sym b -> W4Result sym a
    forall a b. (a -> b) -> W4Result sym a -> W4Result sym b
    forall sym a b. a -> W4Result sym b -> W4Result sym a
    forall sym a b. (a -> b) -> W4Result sym a -> W4Result sym b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall sym a b. (a -> b) -> W4Result sym a -> W4Result sym b
    fmap :: forall a b. (a -> b) -> W4Result sym a -> W4Result sym b
    $c<$ :: forall sym a b. a -> W4Result sym b -> W4Result sym a
    <$ :: forall a b. a -> W4Result sym b -> W4Result sym a
    Functor

    --------------------------------------------------------------------------------
    -- Moving between the layers

    w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval :: forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval (W4Eval (W4Conn sym -> Eval (W4Result sym a)
    m)) = sym -> Eval (W4Result sym a)
    m

    w4Thunk :: Eval (W4Result sym a) -> W4Eval sym a
    w4Thunk :: forall sym a. Eval (W4Result sym a) -> W4Eval sym a
    w4Thunk Eval (W4Result sym a)
    m = W4Conn sym (W4Result sym a) -> W4Eval sym a
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval ((sym -> Eval (W4Result sym a)) -> W4Conn sym (W4Result sym a)
    forall sym a. (sym -> Eval a) -> W4Conn sym a
    W4Conn \sym
    _ -> Eval (W4Result sym a)
    m)

    -- | A value with no context.
    doEval :: W4.IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval :: forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval Eval a
    m = (sym -> Eval a) -> W4Conn sym a
    forall sym a. (sym -> Eval a) -> W4Conn sym a
    W4Conn \sym
    _sym -> Eval a
    m

    -- | A total value.
    total :: W4.IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total :: forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total W4Conn sym a
    m = W4Conn sym (W4Result sym a) -> W4Eval sym a
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval
      do sym
    sym <- W4Conn sym sym
    forall sym. W4Conn sym sym
    getSym
         Pred sym -> a -> W4Result sym a
    forall sym a. Pred sym -> a -> W4Result sym a
    W4Result (sym -> Bool -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
    W4.backendPred sym
    sym Bool
    True) (a -> W4Result sym a)
    -> W4Conn sym a -> W4Conn sym (W4Result sym a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> W4Conn sym a
    m

    --------------------------------------------------------------------------------
    -- Operations in WConn

    instance W4.IsSymExprBuilder sym => Functor (W4Conn sym) where
      fmap :: forall a b. (a -> b) -> W4Conn sym a -> W4Conn sym b
    fmap = (a -> b) -> W4Conn sym a -> W4Conn sym b
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM

    instance W4.IsSymExprBuilder sym => Applicative (W4Conn sym) where
      pure :: forall a. a -> W4Conn sym a
    pure   = Eval a -> W4Conn sym a
    forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval (Eval a -> W4Conn sym a) -> (a -> Eval a) -> a -> W4Conn sym a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Eval a
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      <*> :: forall a b. W4Conn sym (a -> b) -> W4Conn sym a -> W4Conn sym b
    (<*>)  = W4Conn sym (a -> b) -> W4Conn sym a -> W4Conn sym b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance W4.IsSymExprBuilder sym => Monad (W4Conn sym) where
      W4Conn sym a
    m1 >>= :: forall a b. W4Conn sym a -> (a -> W4Conn sym b) -> W4Conn sym b
    >>= a -> W4Conn sym b
    f = (sym -> Eval b) -> W4Conn sym b
    forall sym a. (sym -> Eval a) -> W4Conn sym a
    W4Conn \sym
    sym ->
        do a
    res1 <- W4Conn sym a -> sym -> Eval a
    forall sym a. W4Conn sym a -> sym -> Eval a
    evalConn W4Conn sym a
    m1 sym
    sym
           W4Conn sym b -> sym -> Eval b
    forall sym a. W4Conn sym a -> sym -> Eval a
    evalConn (a -> W4Conn sym b
    f a
    res1) sym
    sym

    instance W4.IsSymExprBuilder sym => MonadIO (W4Conn sym) where
      liftIO :: forall a. IO a -> W4Conn sym a
    liftIO = Eval a -> W4Conn sym a
    forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval (Eval a -> W4Conn sym a)
    -> (IO a -> Eval a) -> IO a -> W4Conn sym a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IO a -> Eval a
    forall a. IO a -> Eval a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO

    -- | Access the symbolic back-end
    getSym :: W4Conn sym sym
    getSym :: forall sym. W4Conn sym sym
    getSym = (sym -> Eval sym) -> W4Conn sym sym
    forall sym a. (sym -> Eval a) -> W4Conn sym a
    W4Conn \sym
    sym -> sym -> Eval sym
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure sym
    sym

    -- | Record a definition.
    --addDef :: W4.Pred sym -> W4Conn sym ()
    --addDef p = W4Conn \_ -> pure W4Defs { w4Defs = p, w4Result = () }

    -- | Compute conjunction.
    w4And :: W4.IsSymExprBuilder sym =>
             W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)
    w4And :: forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    w4And Pred sym
    p Pred sym
    q =
      do sym
    sym <- W4Conn sym sym
    forall sym. W4Conn sym sym
    getSym
         IO (Pred sym) -> W4Conn sym (Pred sym)
    forall a. IO a -> W4Conn sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred sym
    sym Pred sym
    p Pred sym
    q)

    -- | Compute negation.
    w4Not :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Conn sym (W4.Pred sym)
    w4Not :: forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> W4Conn sym (Pred sym)
    w4Not Pred sym
    p =
      do sym
    sym <- W4Conn sym sym
    forall sym. W4Conn sym sym
    getSym
         IO (Pred sym) -> W4Conn sym (Pred sym)
    forall a. IO a -> W4Conn sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred sym
    sym Pred sym
    p)

    -- | Compute if-then-else.
    w4ITE :: W4.IsSymExprBuilder sym =>
             W4.Pred sym -> W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)
    w4ITE :: forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    w4ITE Pred sym
    ifP Pred sym
    ifThen Pred sym
    ifElse =
      do sym
    sym <- W4Conn sym sym
    forall sym. W4Conn sym sym
    getSym
         IO (Pred sym) -> W4Conn sym (Pred sym)
    forall a. IO a -> W4Conn sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.itePred sym
    sym Pred sym
    ifP Pred sym
    ifThen Pred sym
    ifElse)

    --------------------------------------------------------------------------------
    -- Operations in W4Eval

    instance W4.IsSymExprBuilder sym => Functor (W4Eval sym) where
      fmap :: forall a b. (a -> b) -> W4Eval sym a -> W4Eval sym b
    fmap = (a -> b) -> W4Eval sym a -> W4Eval sym b
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM

    instance W4.IsSymExprBuilder sym => Applicative (W4Eval sym) where
      pure :: forall a. a -> W4Eval sym a
    pure  = W4Conn sym a -> W4Eval sym a
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total (W4Conn sym a -> W4Eval sym a)
    -> (a -> W4Conn sym a) -> a -> W4Eval sym a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> W4Conn sym a
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      <*> :: forall a b. W4Eval sym (a -> b) -> W4Eval sym a -> W4Eval sym b
    (<*>) = W4Eval sym (a -> b) -> W4Eval sym a -> W4Eval sym b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance W4.IsSymExprBuilder sym => Monad (W4Eval sym) where
      W4Eval sym a
    m1 >>= :: forall a b. W4Eval sym a -> (a -> W4Eval sym b) -> W4Eval sym b
    >>= a -> W4Eval sym b
    f = W4Conn sym (W4Result sym b) -> W4Eval sym b
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval
        do W4Result sym a
    res1 <- W4Eval sym a -> W4Conn sym (W4Result sym a)
    forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
    evalPartial W4Eval sym a
    m1
           case W4Result sym a
    res1 of
             W4Error EvalErrorEx
    err -> W4Result sym b -> W4Conn sym (W4Result sym b)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (EvalErrorEx -> W4Result sym b
    forall sym a. EvalErrorEx -> W4Result sym a
    W4Error EvalErrorEx
    err)
             W4Result Pred sym
    px a
    x' ->
               do W4Result sym b
    res2 <- W4Eval sym b -> W4Conn sym (W4Result sym b)
    forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
    evalPartial (a -> W4Eval sym b
    f a
    x')
                  case W4Result sym b
    res2 of
                    W4Result Pred sym
    py b
    y ->
                      do Pred sym
    pz <- Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    w4And Pred sym
    px Pred sym
    py
                         W4Result sym b -> W4Conn sym (W4Result sym b)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pred sym -> b -> W4Result sym b
    forall sym a. Pred sym -> a -> W4Result sym a
    W4Result Pred sym
    pz b
    y)
                    W4Error EvalErrorEx
    _ -> W4Result sym b -> W4Conn sym (W4Result sym b)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure W4Result sym b
    res2

    instance W4.IsSymExprBuilder sym => MonadIO (W4Eval sym) where
      liftIO :: forall a. IO a -> W4Eval sym a
    liftIO = W4Conn sym a -> W4Eval sym a
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total (W4Conn sym a -> W4Eval sym a)
    -> (IO a -> W4Conn sym a) -> IO a -> W4Eval sym a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IO a -> W4Conn sym a
    forall a. IO a -> W4Conn sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO

    -- | Add a definitional equation.
    -- This will always be asserted when we make queries to the solver.
    addDefEqn :: W4.IsSymExprBuilder sym => What4 sym -> W4.Pred sym -> W4Eval sym ()
    addDefEqn :: forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> Pred sym -> W4Eval sym ()
    addDefEqn What4 sym
    sym Pred sym
    p =
      IO () -> W4Eval sym ()
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (MVar (Pred sym) -> (Pred sym -> IO (Pred sym)) -> IO ()
    forall a. MVar a -> (a -> IO a) -> IO ()
    modifyMVar_ (What4 sym -> MVar (Pred sym)
    forall sym. What4 sym -> MVar (Pred sym)
    w4defs What4 sym
    sym) (sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Pred sym
    p))

    -- | Add s safety condition.
    addSafety :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Eval sym ()
    addSafety :: forall sym. IsSymExprBuilder sym => Pred sym -> W4Eval sym ()
    addSafety Pred sym
    p = W4Conn sym (W4Result sym ()) -> W4Eval sym ()
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval (W4Result sym () -> W4Conn sym (W4Result sym ())
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pred sym -> () -> W4Result sym ()
    forall sym a. Pred sym -> a -> W4Result sym a
    W4Result Pred sym
    p ()))

    -- | A fully undefined symbolic value
    evalError :: W4.IsSymExprBuilder sym => EvalError -> W4Eval sym a
    evalError :: forall sym a. IsSymExprBuilder sym => EvalError -> W4Eval sym a
    evalError EvalError
    err = W4Conn sym (W4Result sym a) -> W4Eval sym a
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval (W4Conn sym (W4Result sym a) -> W4Eval sym a)
    -> W4Conn sym (W4Result sym a) -> W4Eval sym a
    forall a b. (a -> b) -> a -> b
    $ (sym -> Eval (W4Result sym a)) -> W4Conn sym (W4Result sym a)
    forall sym a. (sym -> Eval a) -> W4Conn sym a
    W4Conn ((sym -> Eval (W4Result sym a)) -> W4Conn sym (W4Result sym a))
    -> (sym -> Eval (W4Result sym a)) -> W4Conn sym (W4Result sym a)
    forall a b. (a -> b) -> a -> b
    $ \sym
    _sym ->
      do CallStack
    stk <- Eval CallStack
    getCallStack
         W4Result sym a -> Eval (W4Result sym a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (EvalErrorEx -> W4Result sym a
    forall sym a. EvalErrorEx -> W4Result sym a
    W4Error (CallStack -> EvalError -> EvalErrorEx
    EvalErrorEx CallStack
    stk EvalError
    err))

    --------------------------------------------------------------------------------

    assertBVDivisor :: W4.IsSymExprBuilder sym => What4 sym -> SW.SWord sym -> W4Eval sym ()
    assertBVDivisor :: forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord sym -> W4Eval sym ()
    assertBVDivisor What4 sym
    sym SWord sym
    x =
      do SymExpr sym BaseBoolType
    p <- IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
    SW.bvIsNonzero (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    x)
         What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition What4 sym
    sym SymExpr sym BaseBoolType
    SBit (What4 sym)
    p EvalError
    DivideByZero

    assertIntDivisor ::
      W4.IsSymExprBuilder sym => What4 sym -> W4.SymInteger sym -> W4Eval sym ()
    assertIntDivisor :: forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SymInteger sym -> W4Eval sym ()
    assertIntDivisor What4 sym
    sym SymInteger sym
    x =
      do SymExpr sym BaseBoolType
    p <- IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    W4.intEq (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymInteger sym
    x (SymInteger sym -> IO (SymExpr sym BaseBoolType))
    -> IO (SymInteger sym) -> IO (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    0)
         What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition What4 sym
    sym SymExpr sym BaseBoolType
    SBit (What4 sym)
    p EvalError
    DivideByZero

    instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
      type SBit (What4 sym)     = W4.Pred sym
      type SWord (What4 sym)    = SW.SWord sym
      type SInteger (What4 sym) = W4.SymInteger sym
      type SFloat (What4 sym)   = FP.SFloat sym
      type SEval (What4 sym)    = W4Eval sym

      raiseError :: forall a. What4 sym -> EvalError -> SEval (What4 sym) a
    raiseError What4 sym
    _ = EvalError -> SEval (What4 sym) a
    EvalError -> W4Eval sym a
    forall sym a. IsSymExprBuilder sym => EvalError -> W4Eval sym a
    evalError

      assertSideCondition :: What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()
    assertSideCondition What4 sym
    _ SBit (What4 sym)
    cond EvalError
    err
        | Just Bool
    False <- SymExpr sym BaseBoolType -> Maybe Bool
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseBoolType -> Maybe Bool
    W4.asConstantPred SymExpr sym BaseBoolType
    SBit (What4 sym)
    cond = EvalError -> W4Eval sym ()
    forall sym a. IsSymExprBuilder sym => EvalError -> W4Eval sym a
    evalError EvalError
    err
        | Bool
    otherwise = SymExpr sym BaseBoolType -> W4Eval sym ()
    forall sym. IsSymExprBuilder sym => Pred sym -> W4Eval sym ()
    addSafety SymExpr sym BaseBoolType
    SBit (What4 sym)
    cond

      isReady :: forall a.
    What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (Maybe a)
    isReady What4 sym
    sym SEval (What4 sym) a
    m = W4Conn sym (W4Result sym (Maybe a)) -> W4Eval sym (Maybe a)
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval (W4Conn sym (W4Result sym (Maybe a)) -> W4Eval sym (Maybe a))
    -> W4Conn sym (W4Result sym (Maybe a)) -> W4Eval sym (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ (sym -> Eval (W4Result sym (Maybe a)))
    -> W4Conn sym (W4Result sym (Maybe a))
    forall sym a. (sym -> Eval a) -> W4Conn sym a
    W4Conn ((sym -> Eval (W4Result sym (Maybe a)))
     -> W4Conn sym (W4Result sym (Maybe a)))
    -> (sym -> Eval (W4Result sym (Maybe a)))
    -> W4Conn sym (W4Result sym (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ \sym
    _ ->
        Eval (W4Result sym a) -> Eval (Maybe (W4Result sym a))
    forall a. Eval a -> Eval (Maybe a)
    maybeReady (W4Eval sym a -> sym -> Eval (W4Result sym a)
    forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval SEval (What4 sym) a
    W4Eval sym a
    m (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym)) Eval (Maybe (W4Result sym a))
    -> (Maybe (W4Result sym a) -> Eval (W4Result sym (Maybe a)))
    -> Eval (W4Result sym (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 W4Result sym a
    x  -> W4Result sym (Maybe a) -> Eval (W4Result sym (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) -> W4Result sym a -> W4Result sym (Maybe a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> W4Result sym a
    x)
          Maybe (W4Result sym a)
    Nothing -> W4Result sym (Maybe a) -> Eval (W4Result sym (Maybe a))
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SymExpr sym BaseBoolType -> Maybe a -> W4Result sym (Maybe a)
    forall sym a. Pred sym -> a -> W4Result sym a
    W4Result (sym -> Bool -> SymExpr sym BaseBoolType
    forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
    W4.backendPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Bool
    True) Maybe a
    forall a. Maybe a
    Nothing)

      sDelayFill :: forall a.
    What4 sym
    -> SEval (What4 sym) a
    -> Maybe (SEval (What4 sym) a)
    -> String
    -> SEval (What4 sym) (SEval (What4 sym) a)
    sDelayFill What4 sym
    _ SEval (What4 sym) a
    m Maybe (SEval (What4 sym) a)
    retry String
    msg =
        W4Conn sym (W4Eval sym a) -> W4Eval sym (W4Eval sym a)
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total
        do sym
    sym <- W4Conn sym sym
    forall sym. W4Conn sym sym
    getSym
           Eval (W4Eval sym a) -> W4Conn sym (W4Eval sym a)
    forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval (Eval (W4Result sym a) -> W4Eval sym a
    forall sym a. Eval (W4Result sym a) -> W4Eval sym a
    w4Thunk (Eval (W4Result sym a) -> W4Eval sym a)
    -> Eval (Eval (W4Result sym a)) -> Eval (W4Eval sym a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval (W4Result sym a)
    -> Maybe (Eval (W4Result sym a))
    -> String
    -> Eval (Eval (W4Result sym a))
    forall a. Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
    delayFill (W4Eval sym a -> sym -> Eval (W4Result sym a)
    forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval SEval (What4 sym) a
    W4Eval sym a
    m sym
    sym) (W4Eval sym a -> sym -> Eval (W4Result sym a)
    forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval (W4Eval sym a -> sym -> Eval (W4Result sym a))
    -> Maybe (W4Eval sym a) -> Maybe (sym -> Eval (W4Result sym a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (SEval (What4 sym) a)
    Maybe (W4Eval sym a)
    retry Maybe (sym -> Eval (W4Result sym a))
    -> Maybe sym -> Maybe (Eval (W4Result sym a))
    forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> sym -> Maybe sym
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure sym
    sym) String
    msg)

      sSpark :: forall a.
    What4 sym
    -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a)
    sSpark What4 sym
    _ SEval (What4 sym) a
    m =
        W4Conn sym (W4Eval sym a) -> W4Eval sym (W4Eval sym a)
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total
        do sym
    sym   <- W4Conn sym sym
    forall sym. W4Conn sym sym
    getSym
           Eval (W4Eval sym a) -> W4Conn sym (W4Eval sym a)
    forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval (Eval (W4Result sym a) -> W4Eval sym a
    forall sym a. Eval (W4Result sym a) -> W4Eval sym a
    w4Thunk (Eval (W4Result sym a) -> W4Eval sym a)
    -> Eval (Eval (W4Result sym a)) -> Eval (W4Eval sym a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval (W4Result sym a) -> Eval (Eval (W4Result sym a))
    forall a. Eval a -> Eval (Eval a)
    evalSpark (W4Eval sym a -> sym -> Eval (W4Result sym a)
    forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval SEval (What4 sym) a
    W4Eval sym a
    m sym
    sym))

      sModifyCallStack :: forall a.
    What4 sym
    -> (CallStack -> CallStack)
    -> SEval (What4 sym) a
    -> SEval (What4 sym) a
    sModifyCallStack What4 sym
    _ CallStack -> CallStack
    f (W4Eval (W4Conn sym -> Eval (W4Result sym a)
    m)) =
        W4Conn sym (W4Result sym a) -> W4Eval sym a
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval ((sym -> Eval (W4Result sym a)) -> W4Conn sym (W4Result sym a)
    forall sym a. (sym -> Eval a) -> W4Conn sym a
    W4Conn \sym
    sym -> (CallStack -> CallStack)
    -> Eval (W4Result sym a) -> Eval (W4Result sym a)
    forall a. (CallStack -> CallStack) -> Eval a -> Eval a
    modifyCallStack CallStack -> CallStack
    f (sym -> Eval (W4Result sym a)
    m sym
    sym))

      sGetCallStack :: What4 sym -> SEval (What4 sym) CallStack
    sGetCallStack What4 sym
    _ = W4Conn sym CallStack -> W4Eval sym CallStack
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total (Eval CallStack -> W4Conn sym CallStack
    forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval Eval CallStack
    getCallStack)

      sDeclareHole :: forall a.
    What4 sym
    -> String
    -> SEval
         (What4 sym)
         (SEval (What4 sym) a, SEval (What4 sym) a -> SEval (What4 sym) ())
    sDeclareHole What4 sym
    _ String
    msg =
        W4Conn sym (W4Eval sym a, W4Eval sym a -> W4Eval sym ())
    -> W4Eval sym (W4Eval sym a, W4Eval sym a -> W4Eval sym ())
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total
        do (Eval (W4Result sym a)
    hole, Eval (W4Result sym a) -> Eval ()
    fill) <- Eval (Eval (W4Result sym a), Eval (W4Result sym a) -> Eval ())
    -> W4Conn
         sym (Eval (W4Result sym a), Eval (W4Result sym a) -> Eval ())
    forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval (String
    -> Eval (Eval (W4Result sym a), Eval (W4Result sym a) -> Eval ())
    forall a. String -> Eval (Eval a, Eval a -> Eval ())
    blackhole String
    msg)
           (W4Eval sym a, W4Eval sym a -> W4Eval sym ())
    -> W4Conn sym (W4Eval sym a, W4Eval sym a -> W4Eval sym ())
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ( Eval (W4Result sym a) -> W4Eval sym a
    forall sym a. Eval (W4Result sym a) -> W4Eval sym a
    w4Thunk Eval (W4Result sym a)
    hole
                , \W4Eval sym a
    m -> W4Conn sym () -> W4Eval sym ()
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
    total
                        do sym
    sym <- W4Conn sym sym
    forall sym. W4Conn sym sym
    getSym
                           Eval () -> W4Conn sym ()
    forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
    doEval (Eval (W4Result sym a) -> Eval ()
    fill (W4Eval sym a -> sym -> Eval (W4Result sym a)
    forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
    w4Eval W4Eval sym a
    m sym
    sym))
                )

      mergeEval :: forall a.
    What4 sym
    -> (SBit (What4 sym) -> a -> a -> SEval (What4 sym) a)
    -> SBit (What4 sym)
    -> SEval (What4 sym) a
    -> SEval (What4 sym) a
    -> SEval (What4 sym) a
    mergeEval What4 sym
    _sym SBit (What4 sym) -> a -> a -> SEval (What4 sym) a
    f SBit (What4 sym)
    c SEval (What4 sym) a
    mx SEval (What4 sym) a
    my = W4Conn sym (W4Result sym a) -> W4Eval sym a
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
    W4Eval
        do W4Result sym a
    rx <- W4Eval sym a -> W4Conn sym (W4Result sym a)
    forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
    evalPartial SEval (What4 sym) a
    W4Eval sym a
    mx
           W4Result sym a
    ry <- W4Eval sym a -> W4Conn sym (W4Result sym a)
    forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
    evalPartial SEval (What4 sym) a
    W4Eval sym a
    my
           case (W4Result sym a
    rx, W4Result sym a
    ry) of

             (W4Error EvalErrorEx
    err, W4Error EvalErrorEx
    _) ->
               W4Result sym a -> W4Conn sym (W4Result sym a)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (EvalErrorEx -> W4Result sym a
    forall sym a. EvalErrorEx -> W4Result sym a
    W4Error EvalErrorEx
    err) -- arbitrarily choose left error to report

             (W4Error EvalErrorEx
    _, W4Result SymExpr sym BaseBoolType
    p a
    y) ->
               do SymExpr sym BaseBoolType
    p' <- SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> W4Conn sym (SymExpr sym BaseBoolType)
    forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    w4And SymExpr sym BaseBoolType
    p (SymExpr sym BaseBoolType -> W4Conn sym (SymExpr sym BaseBoolType))
    -> W4Conn sym (SymExpr sym BaseBoolType)
    -> W4Conn sym (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SymExpr sym BaseBoolType -> W4Conn sym (SymExpr sym BaseBoolType)
    forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> W4Conn sym (Pred sym)
    w4Not SymExpr sym BaseBoolType
    SBit (What4 sym)
    c
                  W4Result sym a -> W4Conn sym (W4Result sym a)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SymExpr sym BaseBoolType -> a -> W4Result sym a
    forall sym a. Pred sym -> a -> W4Result sym a
    W4Result SymExpr sym BaseBoolType
    p' a
    y)

             (W4Result SymExpr sym BaseBoolType
    p a
    x, W4Error EvalErrorEx
    _) ->
               do SymExpr sym BaseBoolType
    p' <- SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> W4Conn sym (SymExpr sym BaseBoolType)
    forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    w4And SymExpr sym BaseBoolType
    p SymExpr sym BaseBoolType
    SBit (What4 sym)
    c
                  W4Result sym a -> W4Conn sym (W4Result sym a)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SymExpr sym BaseBoolType -> a -> W4Result sym a
    forall sym a. Pred sym -> a -> W4Result sym a
    W4Result SymExpr sym BaseBoolType
    p' a
    x)

             (W4Result SymExpr sym BaseBoolType
    px a
    x, W4Result SymExpr sym BaseBoolType
    py a
    y) ->
               do W4Result sym a
    zr <- W4Eval sym a -> W4Conn sym (W4Result sym a)
    forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
    evalPartial (SBit (What4 sym) -> a -> a -> SEval (What4 sym) a
    f SBit (What4 sym)
    c a
    x a
    y)
                  case W4Result sym a
    zr of
                    W4Error EvalErrorEx
    err -> W4Result sym a -> W4Conn sym (W4Result sym a)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (W4Result sym a -> W4Conn sym (W4Result sym a))
    -> W4Result sym a -> W4Conn sym (W4Result sym a)
    forall a b. (a -> b) -> a -> b
    $ EvalErrorEx -> W4Result sym a
    forall sym a. EvalErrorEx -> W4Result sym a
    W4Error EvalErrorEx
    err
                    W4Result SymExpr sym BaseBoolType
    pz a
    z ->
                      do SymExpr sym BaseBoolType
    p' <- SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> W4Conn sym (SymExpr sym BaseBoolType)
    forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    w4And SymExpr sym BaseBoolType
    pz (SymExpr sym BaseBoolType -> W4Conn sym (SymExpr sym BaseBoolType))
    -> W4Conn sym (SymExpr sym BaseBoolType)
    -> W4Conn sym (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> W4Conn sym (SymExpr sym BaseBoolType)
    forall sym.
    IsSymExprBuilder sym =>
    Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
    w4ITE SymExpr sym BaseBoolType
    SBit (What4 sym)
    c SymExpr sym BaseBoolType
    px SymExpr sym BaseBoolType
    py
                         W4Result sym a -> W4Conn sym (W4Result sym a)
    forall a. a -> W4Conn sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SymExpr sym BaseBoolType -> a -> W4Result sym a
    forall sym a. Pred sym -> a -> W4Result sym a
    W4Result SymExpr sym BaseBoolType
    p' a
    z)

      wordAsChar :: What4 sym -> SWord (What4 sym) -> Maybe Char
    wordAsChar What4 sym
    _ SWord (What4 sym)
    bv
        | SWord sym -> Integer
    forall sym. SWord sym -> Integer
    SW.bvWidth SWord sym
    SWord (What4 sym)
    bv Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    8 = Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Int -> Char) -> (Integer -> Int) -> Integer -> Char
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Char) -> Maybe Integer -> Maybe Char
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SWord sym -> Maybe Integer
    forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
    SW.bvAsUnsignedInteger SWord sym
    SWord (What4 sym)
    bv
        | Bool
    otherwise = Maybe Char
    forall a. Maybe a
    Nothing

      wordLen :: What4 sym -> SWord (What4 sym) -> Integer
    wordLen What4 sym
    _ SWord (What4 sym)
    bv = SWord sym -> Integer
    forall sym. SWord sym -> Integer
    SW.bvWidth SWord sym
    SWord (What4 sym)
    bv

      bitLit :: What4 sym -> Bool -> SBit (What4 sym)
    bitLit What4 sym
    sym Bool
    b = sym -> Bool -> SymExpr sym BaseBoolType
    forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
    W4.backendPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Bool
    b
      bitAsLit :: What4 sym -> SBit (What4 sym) -> Maybe Bool
    bitAsLit What4 sym
    _ SBit (What4 sym)
    v = SymExpr sym BaseBoolType -> Maybe Bool
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseBoolType -> Maybe Bool
    W4.asConstantPred SymExpr sym BaseBoolType
    SBit (What4 sym)
    v

      wordLit :: What4 sym
    -> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym))
    wordLit What4 sym
    sym Integer
    intw Integer
    i
        | Just (Some NatRepr x
    w) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    intw
        = case NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    w of
            Maybe (LeqProof 1 x)
    Nothing -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
    forall a. a -> SEval (What4 sym) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)))
    -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ SWord sym
    SWord (What4 sym)
    forall sym. SWord sym
    SW.ZBV
            Just LeqProof 1 x
    LeqProof -> SymBV sym x -> SWord sym
    forall sym (w :: Nat).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    SW.DBV (SymBV sym x -> SWord sym)
    -> W4Eval sym (SymBV sym x) -> W4Eval sym (SWord sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO (SymBV sym x) -> W4Eval sym (SymBV sym x)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> NatRepr x -> BV x -> IO (SymBV sym x)
    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)
    W4.bvLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) NatRepr x
    w (NatRepr x -> Integer -> BV x
    forall (w :: Nat). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr x
    w Integer
    i))
        | Bool
    otherwise = String -> [String] -> W4Eval sym (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "what4: wordLit" [String
    "invalid bit width:", Integer -> String
    forall a. Show a => a -> String
    show Integer
    intw ]

      wordAsLit :: What4 sym -> SWord (What4 sym) -> Maybe (Integer, Integer)
    wordAsLit What4 sym
    _ SWord (What4 sym)
    v
        | Just Integer
    x <- SWord sym -> Maybe Integer
    forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
    SW.bvAsUnsignedInteger SWord sym
    SWord (What4 sym)
    v = (Integer, Integer) -> Maybe (Integer, Integer)
    forall a. a -> Maybe a
    Just (SWord sym -> Integer
    forall sym. SWord sym -> Integer
    SW.bvWidth SWord sym
    SWord (What4 sym)
    v, Integer
    x)
        | Bool
    otherwise = Maybe (Integer, Integer)
    forall a. Maybe a
    Nothing

      integerLit :: What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym))
    integerLit What4 sym
    sym Integer
    i = IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Integer -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    i)

      integerAsLit :: What4 sym -> SInteger (What4 sym) -> Maybe Integer
    integerAsLit What4 sym
    _ SInteger (What4 sym)
    v = SymExpr sym BaseIntegerType -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    v

      iteBit :: What4 sym
    -> SBit (What4 sym)
    -> SBit (What4 sym)
    -> SBit (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    iteBit What4 sym
    sym SBit (What4 sym)
    c SBit (What4 sym)
    x SBit (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.itePred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    c SymExpr sym BaseBoolType
    SBit (What4 sym)
    x SymExpr sym BaseBoolType
    SBit (What4 sym)
    y)
      iteWord :: What4 sym
    -> SBit (What4 sym)
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    iteWord What4 sym
    sym SBit (What4 sym)
    c SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SWord sym
    -> SWord sym
    -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvIte (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    c SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      iteInteger :: What4 sym
    -> SBit (What4 sym)
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    iteInteger What4 sym
    sym SBit (What4 sym)
    c SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    W4.intIte (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    c SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y)
      iteFloat :: What4 sym
    -> SBit (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    iteFloat What4 sym
    sym SBit (What4 sym)
    p SFloat (What4 sym)
    x SFloat (What4 sym)
    y = IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    FP.fpIte (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    p SFloat sym
    SFloat (What4 sym)
    x SFloat sym
    SFloat (What4 sym)
    y)

      bitEq :: What4 sym
    -> SBit (What4 sym)
    -> SBit (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    bitEq  What4 sym
    sym SBit (What4 sym)
    x SBit (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.eqPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    x SymExpr sym BaseBoolType
    SBit (What4 sym)
    y)
      bitAnd :: What4 sym
    -> SBit (What4 sym)
    -> SBit (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    bitAnd What4 sym
    sym SBit (What4 sym)
    x SBit (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    x SymExpr sym BaseBoolType
    SBit (What4 sym)
    y)
      bitOr :: What4 sym
    -> SBit (What4 sym)
    -> SBit (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    bitOr  What4 sym
    sym SBit (What4 sym)
    x SBit (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.orPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    x SymExpr sym BaseBoolType
    SBit (What4 sym)
    y)
      bitXor :: What4 sym
    -> SBit (What4 sym)
    -> SBit (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    bitXor What4 sym
    sym SBit (What4 sym)
    x SBit (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.xorPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    x SymExpr sym BaseBoolType
    SBit (What4 sym)
    y)
      bitComplement :: What4 sym
    -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
    bitComplement What4 sym
    sym SBit (What4 sym)
    x = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    SBit (What4 sym)
    x)

      wordBit :: What4 sym
    -> SWord (What4 sym)
    -> Integer
    -> SEval (What4 sym) (SBit (What4 sym))
    wordBit What4 sym
    sym SWord (What4 sym)
    bv Integer
    idx = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> Integer -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> Integer -> IO (Pred sym)
    SW.bvAtBE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    bv Integer
    idx)
      wordUpdate :: What4 sym
    -> SWord (What4 sym)
    -> Integer
    -> SBit (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordUpdate What4 sym
    sym SWord (What4 sym)
    bv Integer
    idx SBit (What4 sym)
    b = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SWord sym
    -> Integer
    -> SymExpr sym BaseBoolType
    -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
    SW.bvSetBE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    bv Integer
    idx SymExpr sym BaseBoolType
    SBit (What4 sym)
    b)

      packWord :: What4 sym
    -> [SBit (What4 sym)] -> SEval (What4 sym) (SWord (What4 sym))
    packWord What4 sym
    sym [SBit (What4 sym)]
    bs =
        do SWord sym
    z <- What4 sym
    -> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym))
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SWord sym)
    wordLit What4 sym
    sym ([SymExpr sym BaseBoolType] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [SymExpr sym BaseBoolType]
    [SBit (What4 sym)]
    bs) Integer
    0
           let f :: SWord sym
    -> (Integer, SymExpr sym BaseBoolType)
    -> SEval (What4 sym) (SWord (What4 sym))
    f SWord sym
    w (Integer
    idx,SymExpr sym BaseBoolType
    b) = What4 sym
    -> SWord (What4 sym)
    -> Integer
    -> SBit (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    forall sym.
    Backend sym =>
    sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
    wordUpdate What4 sym
    sym SWord sym
    SWord (What4 sym)
    w Integer
    idx SymExpr sym BaseBoolType
    SBit (What4 sym)
    b
           (SWord sym
     -> (Integer, SymExpr sym BaseBoolType) -> W4Eval sym (SWord sym))
    -> SWord sym
    -> [(Integer, SymExpr sym BaseBoolType)]
    -> W4Eval sym (SWord sym)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM SWord sym
    -> (Integer, SymExpr sym BaseBoolType)
    -> SEval (What4 sym) (SWord (What4 sym))
    SWord sym
    -> (Integer, SymExpr sym BaseBoolType) -> W4Eval sym (SWord sym)
    f SWord sym
    z ([Integer]
    -> [SymExpr sym BaseBoolType]
    -> [(Integer, SymExpr sym BaseBoolType)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Integer
    0..] [SymExpr sym BaseBoolType]
    [SBit (What4 sym)]
    bs)

      unpackWord :: What4 sym
    -> SWord (What4 sym) -> SEval (What4 sym) [SBit (What4 sym)]
    unpackWord What4 sym
    sym SWord (What4 sym)
    bv = IO [SBit (What4 sym)] -> SEval (What4 sym) [SBit (What4 sym)]
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [SBit (What4 sym)] -> SEval (What4 sym) [SBit (What4 sym)])
    -> IO [SBit (What4 sym)] -> SEval (What4 sym) [SBit (What4 sym)]
    forall a b. (a -> b) -> a -> b
    $
        (Integer -> IO (SymExpr sym BaseBoolType))
    -> [Integer] -> IO [SymExpr sym BaseBoolType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym -> SWord sym -> Integer -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> Integer -> IO (Pred sym)
    SW.bvAtBE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    bv) [Integer
    0 .. SWord sym -> Integer
    forall sym. SWord sym -> Integer
    SW.bvWidth SWord sym
    SWord (What4 sym)
    bvInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1]

      joinWord :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    joinWord What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord (What4 sym)) -> SEval (What4 sym) (SWord (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord (What4 sym)) -> SEval (What4 sym) (SWord (What4 sym)))
    -> IO (SWord (What4 sym)) -> SEval (What4 sym) (SWord (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvJoin (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y

      splitWord :: What4 sym
    -> Integer
    -> Integer
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym))
    splitWord What4 sym
    _sym Integer
    0 Integer
    _ SWord (What4 sym)
    bv = (SWord sym, SWord sym) -> W4Eval sym (SWord sym, SWord sym)
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SWord sym
    forall sym. SWord sym
    SW.ZBV, SWord sym
    SWord (What4 sym)
    bv)
      splitWord What4 sym
    _sym Integer
    _ Integer
    0 SWord (What4 sym)
    bv = (SWord sym, SWord sym) -> W4Eval sym (SWord sym, SWord sym)
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SWord sym
    SWord (What4 sym)
    bv, SWord sym
    forall sym. SWord sym
    SW.ZBV)
      splitWord What4 sym
    sym Integer
    lw Integer
    rw SWord (What4 sym)
    bv = IO (SWord (What4 sym), SWord (What4 sym))
    -> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord (What4 sym), SWord (What4 sym))
     -> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym)))
    -> IO (SWord (What4 sym), SWord (What4 sym))
    -> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym))
    forall a b. (a -> b) -> a -> b
    $
        do SWord sym
    l <- sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    SW.bvSliceBE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    0 Integer
    lw SWord sym
    SWord (What4 sym)
    bv
           SWord sym
    r <- sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    SW.bvSliceBE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    lw Integer
    rw SWord sym
    SWord (What4 sym)
    bv
           (SWord sym, SWord sym) -> IO (SWord sym, SWord sym)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SWord sym
    l, SWord sym
    r)

      extractWord :: What4 sym
    -> Integer
    -> Integer
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    extractWord What4 sym
    sym Integer
    bits Integer
    idx SWord (What4 sym)
    bv =
        IO (SWord (What4 sym)) -> SEval (What4 sym) (SWord (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord (What4 sym)) -> SEval (What4 sym) (SWord (What4 sym)))
    -> IO (SWord (What4 sym)) -> SEval (What4 sym) (SWord (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    SW.bvSliceLE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    idx Integer
    bits SWord sym
    SWord (What4 sym)
    bv

      wordEq :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    wordEq                What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
    PredBin
    SW.bvEq  (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordLessThan :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    wordLessThan          What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
    PredBin
    SW.bvult (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordGreaterThan :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    wordGreaterThan       What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
    PredBin
    SW.bvugt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordSignedLessThan :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    wordSignedLessThan    What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
    PredBin
    SW.bvslt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)

      wordOr :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordOr  What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvOr  (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordAnd :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordAnd What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvAnd (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordXor :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordXor What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvXor (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordComplement :: What4 sym
    -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
    wordComplement What4 sym
    sym SWord (What4 sym)
    x = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> IO (SWord sym)
    SWordUn
    SW.bvNot (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x)

      wordPlus :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordPlus   What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvAdd (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordMinus :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordMinus  What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvSub (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordMult :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordMult   What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvMul (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordNegate :: What4 sym
    -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
    wordNegate What4 sym
    sym SWord (What4 sym)
    x   = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> IO (SWord sym)
    SWordUn
    SW.bvNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x)
      wordLg2 :: What4 sym
    -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
    wordLg2    What4 sym
    sym SWord (What4 sym)
    x   = sym -> SWord sym -> SEval (What4 sym) (SWord sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SEval (What4 sym) (SWord sym)
    sLg2 (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x

      wordShiftLeft :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordShiftLeft   What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvShl (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y
      wordShiftRight :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordShiftRight  What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvLshr (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y
      wordRotateLeft :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordRotateLeft  What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvRol (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y
      wordRotateRight :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordRotateRight What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvRor (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y
      wordSignedShiftRight :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordSignedShiftRight What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y = sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvAshr (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y

      wordDiv :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordDiv What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y =
         do What4 sym -> SWord sym -> W4Eval sym ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord sym -> W4Eval sym ()
    assertBVDivisor What4 sym
    sym SWord sym
    SWord (What4 sym)
    y
            IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvUDiv (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordMod :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordMod What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y =
         do What4 sym -> SWord sym -> W4Eval sym ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord sym -> W4Eval sym ()
    assertBVDivisor What4 sym
    sym SWord sym
    SWord (What4 sym)
    y
            IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvURem (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordSignedDiv :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordSignedDiv What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y =
         do What4 sym -> SWord sym -> W4Eval sym ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord sym -> W4Eval sym ()
    assertBVDivisor What4 sym
    sym SWord sym
    SWord (What4 sym)
    y
            IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvSDiv (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)
      wordSignedMod :: What4 sym
    -> SWord (What4 sym)
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordSignedMod What4 sym
    sym SWord (What4 sym)
    x SWord (What4 sym)
    y =
         do What4 sym -> SWord sym -> W4Eval sym ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord sym -> W4Eval sym ()
    assertBVDivisor What4 sym
    sym SWord sym
    SWord (What4 sym)
    y
            IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvSRem (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x SWord sym
    SWord (What4 sym)
    y)

      wordToInt :: What4 sym
    -> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
    wordToInt What4 sym
    sym SWord (What4 sym)
    x = IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> IO (SymInteger sym)
    SW.bvToInteger (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x)
      wordToSignedInt :: What4 sym
    -> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
    wordToSignedInt What4 sym
    sym SWord (What4 sym)
    x = IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SWord sym -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> IO (SymInteger sym)
    SW.sbvToInteger (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SWord sym
    SWord (What4 sym)
    x)
      wordFromInt :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SWord (What4 sym))
    wordFromInt What4 sym
    sym Integer
    width SInteger (What4 sym)
    i = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SymExpr sym BaseIntegerType -> Integer -> IO (SWord sym)
    forall sym width.
    (Show width, Integral width, IsExprBuilder sym) =>
    sym -> SymInteger sym -> width -> IO (SWord sym)
    SW.integerToBV (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    i Integer
    width)

      intPlus :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    intPlus   What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y  = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intAdd (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      intMinus :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    intMinus  What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y  = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intSub (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      intMult :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    intMult   What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y  = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMul (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      intNegate :: What4 sym
    -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
    intNegate What4 sym
    sym SInteger (What4 sym)
    x    = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x

      -- NB: What4's division operation provides SMTLib's euclidean division,
      -- which doesn't match the round-to-neg-infinity semantics of Cryptol,
      -- so we have to do some work to get the desired semantics.
      intDiv :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    intDiv What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y =
        do What4 sym -> SymExpr sym BaseIntegerType -> W4Eval sym ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SymInteger sym -> W4Eval sym ()
    assertIntDivisor What4 sym
    sym SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
           IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SymExpr sym BaseIntegerType)
     -> W4Eval sym (SymExpr sym BaseIntegerType))
    -> IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a b. (a -> b) -> a -> b
    $ do
             SymExpr sym BaseBoolType
    neg <- IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
    forall a. IO a -> IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    W4.intLt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseIntegerType)
    -> IO (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    0)
             case SymExpr sym BaseBoolType -> Maybe Bool
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseBoolType -> Maybe Bool
    W4.asConstantPred SymExpr sym BaseBoolType
    neg of
               Just Bool
    False -> sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intDiv (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
               Just Bool
    True  ->
                  do SymExpr sym BaseIntegerType
    xneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x
                     SymExpr sym BaseIntegerType
    yneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
                     sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intDiv (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    xneg SymExpr sym BaseIntegerType
    yneg
               Maybe Bool
    Nothing ->
                  do SymExpr sym BaseIntegerType
    xneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x
                     SymExpr sym BaseIntegerType
    yneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
                     SymExpr sym BaseIntegerType
    zneg <- sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intDiv (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    xneg SymExpr sym BaseIntegerType
    yneg
                     SymExpr sym BaseIntegerType
    z    <- sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intDiv (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
                     sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    W4.intIte (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    neg SymExpr sym BaseIntegerType
    zneg SymExpr sym BaseIntegerType
    z

      -- NB: What4's division operation provides SMTLib's euclidean division,
      -- which doesn't match the round-to-neg-infinity semantics of Cryptol,
      -- so we have to do some work to get the desired semantics.
      intMod :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    intMod What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y =
        do What4 sym -> SymExpr sym BaseIntegerType -> W4Eval sym ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SymInteger sym -> W4Eval sym ()
    assertIntDivisor What4 sym
    sym SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
           IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SymExpr sym BaseIntegerType)
     -> W4Eval sym (SymExpr sym BaseIntegerType))
    -> IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a b. (a -> b) -> a -> b
    $ do
             SymExpr sym BaseBoolType
    neg <- IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
    forall a. IO a -> IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    W4.intLt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseIntegerType)
    -> IO (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    0)
             case SymExpr sym BaseBoolType -> Maybe Bool
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseBoolType -> Maybe Bool
    W4.asConstantPred SymExpr sym BaseBoolType
    neg of
               Just Bool
    False -> sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMod (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
               Just Bool
    True  ->
                  do SymExpr sym BaseIntegerType
    xneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x
                     SymExpr sym BaseIntegerType
    yneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
                     sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType))
    -> IO (SymExpr sym BaseIntegerType)
    -> IO (SymExpr sym BaseIntegerType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMod (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    xneg SymExpr sym BaseIntegerType
    yneg
               Maybe Bool
    Nothing ->
                  do SymExpr sym BaseIntegerType
    xneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x
                     SymExpr sym BaseIntegerType
    yneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
                     SymExpr sym BaseIntegerType
    z    <- sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMod (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
                     SymExpr sym BaseIntegerType
    zneg <- sym
    -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType))
    -> IO (SymExpr sym BaseIntegerType)
    -> IO (SymExpr sym BaseIntegerType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMod (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    xneg SymExpr sym BaseIntegerType
    yneg
                     sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    W4.intIte (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    neg SymExpr sym BaseIntegerType
    zneg SymExpr sym BaseIntegerType
    z

      intEq :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    intEq What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    W4.intEq (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      intLessThan :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    intLessThan What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    W4.intLt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      intGreaterThan :: What4 sym
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    intGreaterThan What4 sym
    sym SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    W4.intLt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x

      -- NB, we don't do reduction here on symbolic values
      intToZn :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    intToZn What4 sym
    sym Integer
    m SInteger (What4 sym)
    x
        | Just Integer
    xi <- SymExpr sym BaseIntegerType -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x
        = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> Integer -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (Integer
    xi Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m)

        | Bool
    otherwise
        = SymExpr sym BaseIntegerType
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x

      znToInt :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    znToInt What4 sym
    _ Integer
    0 SInteger (What4 sym)
    _ = String -> [String] -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. String -> [String] -> a
    evalPanic String
    "znToInt" [String
    "0 modulus not allowed"]
      znToInt What4 sym
    sym Integer
    m SInteger (What4 sym)
    x = IO (SymExpr sym BaseIntegerType)
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMod (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType))
    -> IO (SymExpr sym BaseIntegerType)
    -> IO (SymExpr sym BaseIntegerType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    m)

      znEq :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    znEq What4 sym
    _ Integer
    0 SInteger (What4 sym)
    _ SInteger (What4 sym)
    _ = String -> [String] -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. String -> [String] -> a
    evalPanic String
    "znEq" [String
    "0 modulus not allowed"]
      znEq What4 sym
    sym Integer
    m SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $
         do SymExpr sym BaseIntegerType
    diff <- sym
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intSub (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
            sym
    -> SymExpr sym BaseIntegerType
    -> Nat
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> Nat -> IO (Pred sym)
    W4.intDivisible (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseIntegerType
    diff (Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger Integer
    m)

      znPlus :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    znPlus   What4 sym
    sym Integer
    m SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> Integer
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsSymExprBuilder sym =>
    sym
    -> Integer
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    sModAdd (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    m SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      znMinus :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    znMinus  What4 sym
    sym Integer
    m SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> Integer
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsSymExprBuilder sym =>
    sym
    -> Integer
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    sModSub (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    m SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      znMult :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    znMult   What4 sym
    sym Integer
    m SInteger (What4 sym)
    x SInteger (What4 sym)
    y = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> Integer
    -> SymExpr sym BaseIntegerType
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsSymExprBuilder sym =>
    sym
    -> Integer
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    sModMult (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    m SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    y
      znNegate :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    znNegate What4 sym
    sym Integer
    m SInteger (What4 sym)
    x   = IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SInteger (What4 sym))
     -> SEval (What4 sym) (SInteger (What4 sym)))
    -> IO (SInteger (What4 sym))
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> Integer
    -> SymExpr sym BaseIntegerType
    -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
    sModNegate (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    m SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x
      znRecip :: What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    znRecip = What4 sym
    -> Integer
    -> SymExpr sym BaseIntegerType
    -> W4Eval sym (SymExpr sym BaseIntegerType)
    What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym
    -> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym)
    sModRecip

      --------------------------------------------------------------

      fpLit :: What4 sym
    -> Integer
    -> Integer
    -> Rational
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpLit What4 sym
    sym Integer
    e Integer
    p Rational
    r = IO (SFloat (What4 sym)) -> SEval (What4 sym) (SFloat (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SFloat (What4 sym)) -> SEval (What4 sym) (SFloat (What4 sym)))
    -> IO (SFloat (What4 sym))
    -> SEval (What4 sym) (SFloat (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
    FP.fpFromRationalLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    e Integer
    p Rational
    r
      fpAsLit :: What4 sym -> SFloat (What4 sym) -> Maybe BF
    fpAsLit What4 sym
    _ SFloat (What4 sym)
    f = Integer -> Integer -> BigFloat -> BF
    BF Integer
    e Integer
    p (BigFloat -> BF) -> Maybe BigFloat -> Maybe BF
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SFloat sym -> Maybe BigFloat
    forall sym. SFloat sym -> Maybe BigFloat
    FP.fpAsLit SFloat sym
    SFloat (What4 sym)
    f
        where (Integer
    e,Integer
    p) = SFloat sym -> (Integer, Integer)
    forall sym. SFloat sym -> (Integer, Integer)
    FP.fpSize SFloat sym
    SFloat (What4 sym)
    f

      fpExactLit :: What4 sym -> BF -> SEval (What4 sym) (SFloat (What4 sym))
    fpExactLit What4 sym
    sym BF{ bfExpWidth :: BF -> Integer
    bfExpWidth = Integer
    e, bfPrecWidth :: BF -> Integer
    bfPrecWidth = Integer
    p, bfValue :: BF -> BigFloat
    bfValue = BigFloat
    bf } =
        IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
    FP.fpFromBinary (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    e Integer
    p (SWord sym -> IO (SFloat sym)) -> IO (SWord sym) -> IO (SFloat sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    SW.bvLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) (Integer
    eInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    p) (Integer -> Integer -> BigFloat -> Integer
    floatToBits Integer
    e Integer
    p BigFloat
    bf))

      fpNaN :: What4 sym
    -> Integer -> Integer -> SEval (What4 sym) (SFloat (What4 sym))
    fpNaN What4 sym
    sym Integer
    e Integer
    p = IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Integer -> Integer -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SFloat sym)
    FP.fpNaN (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    e Integer
    p)
      fpPosInf :: What4 sym
    -> Integer -> Integer -> SEval (What4 sym) (SFloat (What4 sym))
    fpPosInf What4 sym
    sym Integer
    e Integer
    p = IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Integer -> Integer -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SFloat sym)
    FP.fpPosInf (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    e Integer
    p)

      fpToBits :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
    fpToBits What4 sym
    sym SFloat (What4 sym)
    f = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SFloat sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SWord sym)
    FP.fpToBinary (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    f)
      fpFromBits :: What4 sym
    -> Integer
    -> Integer
    -> SWord (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpFromBits What4 sym
    sym Integer
    e Integer
    p SWord (What4 sym)
    w = IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
    FP.fpFromBinary (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    e Integer
    p SWord sym
    SWord (What4 sym)
    w)

      fpEq :: What4 sym
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    fpEq          What4 sym
    sym SFloat (What4 sym)
    x SFloat (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ SFloatRel sym
    forall sym. IsExprBuilder sym => SFloatRel sym
    FP.fpEqIEEE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x SFloat sym
    SFloat (What4 sym)
    y
      fpLessThan :: What4 sym
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    fpLessThan    What4 sym
    sym SFloat (What4 sym)
    x SFloat (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ SFloatRel sym
    forall sym. IsExprBuilder sym => SFloatRel sym
    FP.fpLtIEEE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x SFloat sym
    SFloat (What4 sym)
    y
      fpGreaterThan :: What4 sym
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    fpGreaterThan What4 sym
    sym SFloat (What4 sym)
    x SFloat (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ SFloatRel sym
    forall sym. IsExprBuilder sym => SFloatRel sym
    FP.fpGtIEEE (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x SFloat sym
    SFloat (What4 sym)
    y
      fpLogicalEq :: What4 sym
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    fpLogicalEq   What4 sym
    sym SFloat (What4 sym)
    x SFloat (What4 sym)
    y = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ SFloatRel sym
    forall sym. IsExprBuilder sym => SFloatRel sym
    FP.fpEq (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x SFloat sym
    SFloat (What4 sym)
    y

      fpPlus :: FPArith2 (What4 sym)
    fpPlus  = SFloatBinArith sym -> FPArith2 (What4 sym)
    forall sym.
    IsSymExprBuilder sym =>
    SFloatBinArith sym
    -> What4 sym
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpBinArith SFloatBinArith sym
    forall sym. IsExprBuilder sym => SFloatBinArith sym
    FP.fpAdd
      fpMinus :: FPArith2 (What4 sym)
    fpMinus = SFloatBinArith sym -> FPArith2 (What4 sym)
    forall sym.
    IsSymExprBuilder sym =>
    SFloatBinArith sym
    -> What4 sym
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpBinArith SFloatBinArith sym
    forall sym. IsExprBuilder sym => SFloatBinArith sym
    FP.fpSub
      fpMult :: FPArith2 (What4 sym)
    fpMult  = SFloatBinArith sym -> FPArith2 (What4 sym)
    forall sym.
    IsSymExprBuilder sym =>
    SFloatBinArith sym
    -> What4 sym
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpBinArith SFloatBinArith sym
    forall sym. IsExprBuilder sym => SFloatBinArith sym
    FP.fpMul
      fpDiv :: FPArith2 (What4 sym)
    fpDiv   = SFloatBinArith sym -> FPArith2 (What4 sym)
    forall sym.
    IsSymExprBuilder sym =>
    SFloatBinArith sym
    -> What4 sym
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpBinArith SFloatBinArith sym
    forall sym. IsExprBuilder sym => SFloatBinArith sym
    FP.fpDiv

      fpNeg :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))
    fpNeg What4 sym
    sym SFloat (What4 sym)
    x = IO (SFloat (What4 sym)) -> SEval (What4 sym) (SFloat (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SFloat (What4 sym)) -> SEval (What4 sym) (SFloat (What4 sym)))
    -> IO (SFloat (What4 sym))
    -> SEval (What4 sym) (SFloat (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SFloat sym)
    FP.fpNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x
      fpAbs :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))
    fpAbs What4 sym
    sym SFloat (What4 sym)
    x = IO (SFloat (What4 sym)) -> SEval (What4 sym) (SFloat (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SFloat (What4 sym)) -> SEval (What4 sym) (SFloat (What4 sym)))
    -> IO (SFloat (What4 sym))
    -> SEval (What4 sym) (SFloat (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SFloat sym)
    FP.fpAbs (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x
      fpSqrt :: What4 sym
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpSqrt What4 sym
    sym SWord (What4 sym)
    r SFloat (What4 sym)
    x =
        do RoundingMode
    rm <- What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    fpRoundingMode What4 sym
    sym SWord (What4 sym)
    r
           IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SFloat sym) -> W4Eval sym (SFloat sym))
    -> IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
    FP.fpSqrt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) RoundingMode
    rm SFloat sym
    SFloat (What4 sym)
    x

      fpFMA :: What4 sym
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpFMA What4 sym
    sym SWord (What4 sym)
    r SFloat (What4 sym)
    x SFloat (What4 sym)
    y SFloat (What4 sym)
    z =
        do RoundingMode
    rm <- What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    fpRoundingMode What4 sym
    sym SWord (What4 sym)
    r
           IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SFloat sym) -> W4Eval sym (SFloat sym))
    -> IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    FP.fpFMA (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) RoundingMode
    rm SFloat sym
    SFloat (What4 sym)
    x SFloat sym
    SFloat (What4 sym)
    y SFloat sym
    SFloat (What4 sym)
    z

      fpIsZero :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
    fpIsZero What4 sym
    sym SFloat (What4 sym)
    x = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsZero (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x
      fpIsNeg :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
    fpIsNeg What4 sym
    sym SFloat (What4 sym)
    x = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsNeg (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x
      fpIsNaN :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
    fpIsNaN What4 sym
    sym SFloat (What4 sym)
    x = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsNaN (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x
      fpIsInf :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
    fpIsInf What4 sym
    sym SFloat (What4 sym)
    x = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsInf (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x
      fpIsNorm :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
    fpIsNorm What4 sym
    sym SFloat (What4 sym)
    x = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsNorm (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x
      fpIsSubnorm :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
    fpIsSubnorm What4 sym
    sym SFloat (What4 sym)
    x = IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym)))
    -> IO (SBit (What4 sym)) -> SEval (What4 sym) (SBit (What4 sym))
    forall a b. (a -> b) -> a -> b
    $ sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsSubnorm (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SFloat sym
    SFloat (What4 sym)
    x

      fpFromInteger :: What4 sym
    -> Integer
    -> Integer
    -> SWord (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpFromInteger What4 sym
    sym Integer
    e Integer
    p SWord (What4 sym)
    r SInteger (What4 sym)
    x =
        do RoundingMode
    rm <- What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    fpRoundingMode What4 sym
    sym SWord (What4 sym)
    r
           IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SFloat sym) -> W4Eval sym (SFloat sym))
    -> IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymExpr sym BaseIntegerType
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymInteger sym
    -> IO (SFloat sym)
    FP.fpFromInteger (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    e Integer
    p RoundingMode
    rm SymExpr sym BaseIntegerType
    SInteger (What4 sym)
    x

      fpToInteger :: What4 sym
    -> String
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    fpToInteger = What4 sym
    -> String
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SInteger (What4 sym))
    forall sy sym.
    (IsSymExprBuilder sy, sym ~ What4 sy) =>
    sym
    -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
    fpCvtToInteger

      fpFromRational :: What4 sym
    -> Integer
    -> Integer
    -> SWord (What4 sym)
    -> SRational (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpFromRational = What4 sym
    -> Integer
    -> Integer
    -> SWord (What4 sym)
    -> SRational (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    forall sy sym.
    (IsSymExprBuilder sy, sym ~ What4 sy) =>
    sym
    -> Integer
    -> Integer
    -> SWord sym
    -> SRational sym
    -> SEval sym (SFloat sym)
    fpCvtFromRational
      fpToRational :: What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SRational (What4 sym))
    fpToRational = What4 sym
    -> SFloat (What4 sym) -> SEval (What4 sym) (SRational (What4 sym))
    forall sy sym.
    (IsSymExprBuilder sy, sym ~ What4 sy) =>
    sym -> SFloat sym -> SEval sym (SRational sym)
    fpCvtToRational

    sModAdd :: W4.IsSymExprBuilder sym =>
      sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
    sModAdd :: forall sym.
    IsSymExprBuilder sym =>
    sym
    -> Integer
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    sModAdd sym
    _sym Integer
    0 SymInteger sym
    _ SymInteger sym
    _ = String -> [String] -> IO (SymInteger sym)
    forall a. String -> [String] -> a
    evalPanic String
    "sModAdd" [String
    "0 modulus not allowed"]
    sModAdd sym
    sym Integer
    m SymInteger sym
    x SymInteger sym
    y
      | Just Integer
    xi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    x
      , Just Integer
    yi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    y
      = sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit sym
    sym ((Integer
    xiInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    yi) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m)

      | Bool
    otherwise
      = sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intAdd sym
    sym SymInteger sym
    x SymInteger sym
    y

    sModSub :: W4.IsSymExprBuilder sym =>
      sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
    sModSub :: forall sym.
    IsSymExprBuilder sym =>
    sym
    -> Integer
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    sModSub sym
    _sym Integer
    0 SymInteger sym
    _ SymInteger sym
    _ = String -> [String] -> IO (SymInteger sym)
    forall a. String -> [String] -> a
    evalPanic String
    "sModSub" [String
    "0 modulus not allowed"]
    sModSub sym
    sym Integer
    m SymInteger sym
    x SymInteger sym
    y
      | Just Integer
    xi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    x
      , Just Integer
    yi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    y
      = sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit sym
    sym ((Integer
    xiInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    yi) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m)

      | Bool
    otherwise
      = sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intSub sym
    sym SymInteger sym
    x SymInteger sym
    y

    sModMult :: W4.IsSymExprBuilder sym =>
      sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
    sModMult :: forall sym.
    IsSymExprBuilder sym =>
    sym
    -> Integer
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    sModMult sym
    _sym Integer
    0 SymInteger sym
    _ SymInteger sym
    _ = String -> [String] -> IO (SymInteger sym)
    forall a. String -> [String] -> a
    evalPanic String
    "sModMult" [String
    "0 modulus not allowed"]
    sModMult sym
    sym Integer
    m SymInteger sym
    x SymInteger sym
    y
      | Just Integer
    xi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    x
      , Just Integer
    yi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    y
      = sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit sym
    sym ((Integer
    xiInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    yi) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m)

      | Bool
    otherwise
      = sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMul sym
    sym SymInteger sym
    x SymInteger sym
    y

    sModNegate :: W4.IsSymExprBuilder sym =>
      sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym)
    sModNegate :: forall sym.
    IsSymExprBuilder sym =>
    sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
    sModNegate sym
    _sym Integer
    0 SymInteger sym
    _ = String -> [String] -> IO (SymInteger sym)
    forall a. String -> [String] -> a
    evalPanic String
    "sModMult" [String
    "0 modulus not allowed"]
    sModNegate sym
    sym Integer
    m SymInteger sym
    x
      | Just Integer
    xi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    x
      = sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit sym
    sym ((Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    xi) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m)

      | Bool
    otherwise
      = sym -> SymInteger sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intNeg sym
    sym SymInteger sym
    x

    -- | Try successive powers of 2 to find the first that dominates the input.
    --   We could perhaps reduce to using CLZ instead...
    sLg2 :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SEval (What4 sym) (SW.SWord sym)
    sLg2 :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SEval (What4 sym) (SWord sym)
    sLg2 sym
    sym SWord sym
    x = IO (SWord sym) -> SEval (What4 sym) (SWord sym)
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord sym) -> SEval (What4 sym) (SWord sym))
    -> IO (SWord sym) -> SEval (What4 sym) (SWord sym)
    forall a b. (a -> b) -> a -> b
    $ Int -> IO (SWord sym)
    go Int
    0
      where
      w :: Integer
    w = SWord sym -> Integer
    forall sym. SWord sym -> Integer
    SW.bvWidth SWord sym
    x
      lit :: Int -> IO (SWord sym)
    lit Int
    n = sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    SW.bvLit sym
    sym Integer
    w (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n)

      go :: Int -> IO (SWord sym)
    go Int
    i | Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    w =
           do SymExpr sym BaseBoolType
    p <- sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
    PredBin
    SW.bvule sym
    sym SWord sym
    x (SWord sym -> IO (SymExpr sym BaseBoolType))
    -> IO (SWord sym) -> IO (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Int -> IO (SWord sym)
    lit (Int -> Int
    forall a. Bits a => Int -> a
    bit Int
    i)
              (SymExpr sym BaseBoolType
     -> SWord sym -> SWord sym -> IO (SWord sym))
    -> SymExpr sym BaseBoolType
    -> IO (SWord sym)
    -> IO (SWord sym)
    -> IO (SWord sym)
    forall (p :: BaseType -> *) (m :: * -> *) a.
    (IsExpr p, Monad m) =>
    (p BaseBoolType -> a -> a -> m a)
    -> p BaseBoolType -> m a -> m a -> m a
    lazyIte (sym
    -> SymExpr sym BaseBoolType
    -> SWord sym
    -> SWord sym
    -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvIte sym
    sym) SymExpr sym BaseBoolType
    p (Int -> IO (SWord sym)
    lit Int
    i) (Int -> IO (SWord sym)
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1))

      -- base case, should only happen when i = w
      go Int
    i = Int -> IO (SWord sym)
    lit Int
    i

    -- 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
    "[What4] " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cxt)

    lazyIte ::
      (W4.IsExpr p, Monad m) =>
      (p W4.BaseBoolType -> a -> a -> m a) ->
      p W4.BaseBoolType ->
      m a ->
      m a ->
      m a
    lazyIte :: forall (p :: BaseType -> *) (m :: * -> *) a.
    (IsExpr p, Monad m) =>
    (p BaseBoolType -> a -> a -> m a)
    -> p BaseBoolType -> m a -> m a -> m a
    lazyIte p BaseBoolType -> a -> a -> m a
    f p BaseBoolType
    c m a
    mx m a
    my
      | Just Bool
    b <- p BaseBoolType -> Maybe Bool
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseBoolType -> Maybe Bool
    W4.asConstantPred p BaseBoolType
    c = if Bool
    b then m a
    mx else m a
    my
      | Bool
    otherwise =
          do a
    x <- m a
    mx
             a
    y <- m a
    my
             p BaseBoolType -> a -> a -> m a
    f p BaseBoolType
    c a
    x a
    y

    w4bvShl  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
    w4bvShl :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvShl sym
    sym SWord sym
    x SWord sym
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
    -> IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvShl sym
    sym SWord sym
    x SWord sym
    y

    w4bvLshr  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
    w4bvLshr :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvLshr sym
    sym SWord sym
    x SWord sym
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
    -> IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvLshr sym
    sym SWord sym
    x SWord sym
    y

    w4bvAshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
    w4bvAshr :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvAshr sym
    sym SWord sym
    x SWord sym
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
    -> IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvAshr sym
    sym SWord sym
    x SWord sym
    y

    w4bvRol  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
    w4bvRol :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvRol sym
    sym SWord sym
    x SWord sym
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
    -> IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvRol sym
    sym SWord sym
    x SWord sym
    y

    w4bvRor  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
    w4bvRor :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
    w4bvRor sym
    sym SWord sym
    x SWord sym
    y = IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
    -> IO (SWord sym) -> W4Eval sym (SWord sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    SW.bvRor sym
    sym SWord sym
    x SWord sym
    y

    fpRoundingMode ::
      W4.IsSymExprBuilder sym =>
      What4 sym -> SWord (What4 sym) -> SEval (What4 sym) W4.RoundingMode
    fpRoundingMode :: forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    fpRoundingMode What4 sym
    sym SWord (What4 sym)
    v =
      case What4 sym -> SWord (What4 sym) -> Maybe (Integer, Integer)
    forall sym.
    Backend sym =>
    sym -> SWord sym -> Maybe (Integer, Integer)
    wordAsLit What4 sym
    sym SWord (What4 sym)
    v of
        Just (Integer
    _w,Integer
    i) ->
          case Integer
    i of
            Integer
    0 -> RoundingMode -> W4Eval sym RoundingMode
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RoundingMode
    W4.RNE
            Integer
    1 -> RoundingMode -> W4Eval sym RoundingMode
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RoundingMode
    W4.RNA
            Integer
    2 -> RoundingMode -> W4Eval sym RoundingMode
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RoundingMode
    W4.RTP
            Integer
    3 -> RoundingMode -> W4Eval sym RoundingMode
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RoundingMode
    W4.RTN
            Integer
    4 -> RoundingMode -> W4Eval sym RoundingMode
    forall a. a -> W4Eval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RoundingMode
    W4.RTZ
            Integer
    x -> What4 sym -> EvalError -> SEval (What4 sym) RoundingMode
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. What4 sym -> EvalError -> SEval (What4 sym) a
    raiseError What4 sym
    sym (Integer -> EvalError
    BadRoundingMode Integer
    x)
        Maybe (Integer, Integer)
    _ -> IO RoundingMode -> SEval (What4 sym) RoundingMode
    forall a. IO a -> SEval (What4 sym) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO RoundingMode -> SEval (What4 sym) RoundingMode)
    -> IO RoundingMode -> SEval (What4 sym) RoundingMode
    forall a b. (a -> b) -> a -> b
    $ Unsupported -> IO RoundingMode
    forall e a. Exception e => e -> IO a
    X.throwIO (Unsupported -> IO RoundingMode) -> Unsupported -> IO RoundingMode
    forall a b. (a -> b) -> a -> b
    $ String -> Unsupported
    UnsupportedSymbolicOp String
    "rounding mode"

    fpBinArith ::
      W4.IsSymExprBuilder sym =>
      FP.SFloatBinArith sym ->
      What4 sym ->
      SWord (What4 sym) ->
      SFloat (What4 sym) ->
      SFloat (What4 sym) ->
      SEval (What4 sym) (SFloat (What4 sym))
    fpBinArith :: forall sym.
    IsSymExprBuilder sym =>
    SFloatBinArith sym
    -> What4 sym
    -> SWord (What4 sym)
    -> SFloat (What4 sym)
    -> SFloat (What4 sym)
    -> SEval (What4 sym) (SFloat (What4 sym))
    fpBinArith SFloatBinArith sym
    fun = \What4 sym
    sym SWord (What4 sym)
    r SFloat (What4 sym)
    x SFloat (What4 sym)
    y ->
      do RoundingMode
    m <- What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    fpRoundingMode What4 sym
    sym SWord (What4 sym)
    r
         IO (SFloat sym) -> W4Eval sym (SFloat sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (SFloatBinArith sym
    fun (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) RoundingMode
    m SFloat sym
    SFloat (What4 sym)
    x SFloat sym
    SFloat (What4 sym)
    y)

    fpCvtToInteger ::
      (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
      sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
    fpCvtToInteger :: forall sy sym.
    (IsSymExprBuilder sy, sym ~ What4 sy) =>
    sym
    -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
    fpCvtToInteger sym
    sym String
    fun SWord sym
    r SFloat sym
    x =
      do SymExpr sy BaseBoolType
    grd <- IO (SymExpr sy BaseBoolType) -> W4Eval sy (SymExpr sy BaseBoolType)
    forall a. IO a -> W4Eval sy a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO
                  do SymExpr sy BaseBoolType
    bad1 <- sy -> SFloat sy -> IO (SymExpr sy BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsInf (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SFloat sy
    SFloat sym
    x
                     SymExpr sy BaseBoolType
    bad2 <- sy -> SFloat sy -> IO (SymExpr sy BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsNaN (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SFloat sy
    SFloat sym
    x
                     sy -> SymExpr sy BaseBoolType -> IO (SymExpr sy BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) (SymExpr sy BaseBoolType -> IO (SymExpr sy BaseBoolType))
    -> IO (SymExpr sy BaseBoolType) -> IO (SymExpr sy BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sy
    -> SymExpr sy BaseBoolType
    -> SymExpr sy BaseBoolType
    -> IO (SymExpr sy BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.orPred (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseBoolType
    bad1 SymExpr sy BaseBoolType
    bad2
         sym -> SBit sym -> EvalError -> SEval sym ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition sym
    sym SymExpr sy BaseBoolType
    SBit sym
    grd (String -> EvalError
    BadValue String
    fun)
         RoundingMode
    rnd  <- What4 sy -> SWord (What4 sy) -> SEval (What4 sy) RoundingMode
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    fpRoundingMode sym
    What4 sy
    sym SWord sym
    SWord (What4 sy)
    r
         IO (SymExpr sy BaseIntegerType)
    -> W4Eval sy (SymExpr sy BaseIntegerType)
    forall a. IO a -> W4Eval sy a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO
           do SymExpr sy BaseRealType
    y <- sy -> SFloat sy -> IO (SymExpr sy BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SymReal sym)
    FP.fpToReal (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SFloat sy
    SFloat sym
    x
              case RoundingMode
    rnd of
                RoundingMode
    W4.RNE -> sy -> SymExpr sy BaseRealType -> IO (SymExpr sy BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymInteger sym)
    W4.realRoundEven (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseRealType
    y
                RoundingMode
    W4.RNA -> sy -> SymExpr sy BaseRealType -> IO (SymExpr sy BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymInteger sym)
    W4.realRound (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseRealType
    y
                RoundingMode
    W4.RTP -> sy -> SymExpr sy BaseRealType -> IO (SymExpr sy BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymInteger sym)
    W4.realCeil (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseRealType
    y
                RoundingMode
    W4.RTN -> sy -> SymExpr sy BaseRealType -> IO (SymExpr sy BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymInteger sym)
    W4.realFloor (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseRealType
    y
                RoundingMode
    W4.RTZ -> sy -> SymExpr sy BaseRealType -> IO (SymExpr sy BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymInteger sym)
    W4.realTrunc (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseRealType
    y

    fpCvtToRational ::
      (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
      sym -> SFloat sym -> SEval sym (SRational sym)
    fpCvtToRational :: forall sy sym.
    (IsSymExprBuilder sy, sym ~ What4 sy) =>
    sym -> SFloat sym -> SEval sym (SRational sym)
    fpCvtToRational sym
    sym SFloat sym
    fp =
      do SymExpr sy BaseBoolType
    grd <- IO (SymExpr sy BaseBoolType) -> W4Eval sy (SymExpr sy BaseBoolType)
    forall a. IO a -> W4Eval sy a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO
                do SymExpr sy BaseBoolType
    bad1 <- sy -> SFloat sy -> IO (SymExpr sy BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsInf (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SFloat sy
    SFloat sym
    fp
                   SymExpr sy BaseBoolType
    bad2 <- sy -> SFloat sy -> IO (SymExpr sy BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    FP.fpIsNaN (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SFloat sy
    SFloat sym
    fp
                   sy -> SymExpr sy BaseBoolType -> IO (SymExpr sy BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) (SymExpr sy BaseBoolType -> IO (SymExpr sy BaseBoolType))
    -> IO (SymExpr sy BaseBoolType) -> IO (SymExpr sy BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sy
    -> SymExpr sy BaseBoolType
    -> SymExpr sy BaseBoolType
    -> IO (SymExpr sy BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.orPred (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseBoolType
    bad1 SymExpr sy BaseBoolType
    bad2
         sym -> SBit sym -> EvalError -> SEval sym ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition sym
    sym SymExpr sy BaseBoolType
    SBit sym
    grd (String -> EvalError
    BadValue String
    "fpToRational")
         (SymExpr sy BaseBoolType
    rel,SymExpr sy BaseIntegerType
    x,SymExpr sy BaseIntegerType
    y) <- IO
      (SymExpr sy BaseBoolType, SymExpr sy BaseIntegerType,
       SymExpr sy BaseIntegerType)
    -> W4Eval
         sy
         (SymExpr sy BaseBoolType, SymExpr sy BaseIntegerType,
          SymExpr sy BaseIntegerType)
    forall a. IO a -> W4Eval sy a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sy
    -> SFloat sy
    -> IO
         (SymExpr sy BaseBoolType, SymExpr sy BaseIntegerType,
          SymExpr sy BaseIntegerType)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym)
    FP.fpToRational (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SFloat sy
    SFloat sym
    fp)
         What4 sy -> SymExpr sy BaseBoolType -> W4Eval sy ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> Pred sym -> W4Eval sym ()
    addDefEqn sym
    What4 sy
    sym (SymExpr sy BaseBoolType -> W4Eval sy ())
    -> W4Eval sy (SymExpr sy BaseBoolType) -> W4Eval sy ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO (SymExpr sy BaseBoolType) -> W4Eval sy (SymExpr sy BaseBoolType)
    forall a. IO a -> W4Eval sy a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sy
    -> SymExpr sy BaseBoolType
    -> SymExpr sy BaseBoolType
    -> IO (SymExpr sy BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.impliesPred (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) SymExpr sy BaseBoolType
    grd SymExpr sy BaseBoolType
    rel)
         sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
    ratio sym
    sym SymExpr sy BaseIntegerType
    SInteger sym
    x SymExpr sy BaseIntegerType
    SInteger sym
    y

    fpCvtFromRational ::
      (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
      sym -> Integer -> Integer -> SWord sym ->
      SRational sym -> SEval sym (SFloat sym)
    fpCvtFromRational :: forall sy sym.
    (IsSymExprBuilder sy, sym ~ What4 sy) =>
    sym
    -> Integer
    -> Integer
    -> SWord sym
    -> SRational sym
    -> SEval sym (SFloat sym)
    fpCvtFromRational sym
    sym Integer
    e Integer
    p SWord sym
    r SRational sym
    rat =
      do RoundingMode
    rnd <- What4 sy -> SWord (What4 sy) -> SEval (What4 sy) RoundingMode
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
    fpRoundingMode sym
    What4 sy
    sym SWord sym
    SWord (What4 sy)
    r
         IO (SFloat sy) -> W4Eval sy (SFloat sy)
    forall a. IO a -> W4Eval sy a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sy
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymInteger sy
    -> SymInteger sy
    -> IO (SFloat sy)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SFloat sym)
    FP.fpFromRational (What4 sy -> sy
    forall sym. What4 sym -> sym
    w4 sym
    What4 sy
    sym) Integer
    e Integer
    p RoundingMode
    rnd (SRational sym -> SInteger sym
    forall sym. SRational sym -> SInteger sym
    sNum SRational sym
    rat) (SRational sym -> SInteger sym
    forall sym. SRational sym -> SInteger sym
    sDenom SRational sym
    rat))

    -- 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 ::
      W4.IsSymExprBuilder sym =>
      What4 sym ->
      Integer ->
      W4.SymInteger sym ->
      W4Eval sym (W4.SymInteger sym)
    sModRecip :: forall sym.
    IsSymExprBuilder sym =>
    What4 sym
    -> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym)
    sModRecip What4 sym
    _sym Integer
    0 SymInteger sym
    _ = String -> [String] -> W4Eval sym (SymInteger sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "sModRecip" [String
    "0 modulus not allowed"]
    sModRecip What4 sym
    sym Integer
    m SymInteger sym
    x
      -- If the input is concrete, evaluate the answer
      | Just Integer
    xi <- SymInteger sym -> Maybe Integer
    forall (e :: BaseType -> *).
    IsExpr e =>
    e BaseIntegerType -> Maybe Integer
    W4.asInteger SymInteger sym
    x
      = case Integer -> Integer -> Maybe Integer
    Integer.integerRecipMod Integer
    xi Integer
    m of
          Just Integer
    r  -> What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym))
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit What4 sym
    sym Integer
    r
          Maybe Integer
    Nothing -> What4 sym -> EvalError -> SEval (What4 sym) (SymInteger sym)
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. What4 sym -> EvalError -> SEval (What4 sym) a
    raiseError What4 sym
    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 SymExpr sym BaseBoolType
    divZero <- IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SymInteger sym -> Nat -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> Nat -> IO (Pred sym)
    W4.intDivisible (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymInteger sym
    x (Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger Integer
    m))
           SymExpr sym BaseBoolType
    ok <- IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    divZero)
           What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition What4 sym
    sym SymExpr sym BaseBoolType
    SBit (What4 sym)
    ok EvalError
    DivideByZero

           SymInteger sym
    z <- IO (SymInteger sym) -> W4Eval sym (SymInteger sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SolverSymbol
    -> Maybe Integer
    -> Maybe Integer
    -> IO (SymInteger sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym
    -> SolverSymbol
    -> Maybe Integer
    -> Maybe Integer
    -> IO (SymInteger sym)
    W4.freshBoundedInt (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SolverSymbol
    W4.emptySymbol (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    1) (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer
    mInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)))
           SymInteger sym
    xz <- IO (SymInteger sym) -> W4Eval sym (SymInteger sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMul (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymInteger sym
    x SymInteger sym
    z)
           SymExpr sym BaseBoolType
    rel <- What4 sym
    -> Integer
    -> SInteger (What4 sym)
    -> SInteger (What4 sym)
    -> SEval (What4 sym) (SBit (What4 sym))
    forall sym.
    Backend sym =>
    sym
    -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    znEq What4 sym
    sym Integer
    m SymInteger sym
    SInteger (What4 sym)
    xz (SymInteger sym -> W4Eval sym (SymExpr sym BaseBoolType))
    -> W4Eval sym (SymInteger sym)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO (SymInteger sym) -> W4Eval sym (SymInteger sym)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W4.intLit (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) Integer
    1)
           What4 sym -> SymExpr sym BaseBoolType -> W4Eval sym ()
    forall sym.
    IsSymExprBuilder sym =>
    What4 sym -> Pred sym -> W4Eval sym ()
    addDefEqn What4 sym
    sym (SymExpr sym BaseBoolType -> W4Eval sym ())
    -> W4Eval sym (SymExpr sym BaseBoolType) -> W4Eval sym ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO (SymExpr sym BaseBoolType)
    -> W4Eval sym (SymExpr sym BaseBoolType)
    forall a. IO a -> W4Eval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.orPred (What4 sym -> sym
    forall sym. What4 sym -> sym
    w4 What4 sym
    sym) SymExpr sym BaseBoolType
    divZero SymExpr sym BaseBoolType
    rel)

           SymInteger sym -> W4Eval sym (SymInteger sym)
    forall a. a -> W4Eval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SymInteger sym
    z