    ------------------------------------------------------------------------
    -- |
    -- Module      : What4.SWord
    -- Description : Dynamically-sized bitvector values
    -- Copyright   : Galois, Inc. 2018-2020
    -- License     : BSD3
    -- Maintainer  : rdockins@galois.com
    -- Stability   : experimental
    -- Portability : non-portable (language extensions)
    --
    -- A wrapper for What4 bitvectors so that the width is not tracked
    -- statically.
    ------------------------------------------------------------------------

    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DeriveTraversable #-}
    {-# LANGUAGE DeriveFoldable #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE DoAndIfThenElse #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE PartialTypeSignatures #-}

    module What4.SWord
      ( SWord(..)
      , bvAsSignedInteger
      , bvAsUnsignedInteger
      , integerToBV
      , bvToInteger
      , sbvToInteger
      , freshBV
      , bvWidth
      , bvLit
      , bvFill
      , bvAtBE
      , bvAtLE
      , bvSetBE
      , bvSetLE
      , bvSliceBE
      , bvSliceLE
      , bvJoin
      , bvIte
      , bvPackBE
      , bvPackLE
      , bvUnpackBE
      , bvUnpackLE
      , bvForall
      , unsignedBVBounds
      , signedBVBounds

        -- * Logic operations
      , bvNot
      , bvAnd
      , bvOr
      , bvXor

        -- * Arithmetic operations
      , bvNeg
      , bvAdd
      , bvSub
      , bvMul
      , bvUDiv
      , bvURem
      , bvSDiv
      , bvSRem

        -- * Comparison operations
      , bvEq
      , bvsle
      , bvslt
      , bvule
      , bvult
      , bvsge
      , bvsgt
      , bvuge
      , bvugt
      , bvIsNonzero

        -- * bit-counting operations
      , bvPopcount
      , bvCountLeadingZeros
      , bvCountTrailingZeros
      , bvLg2

        -- * Shift and rotates
      , bvShl
      , bvLshr
      , bvAshr
      , bvRol
      , bvRor

        -- * Zero- and sign-extend
      , bvZext
      , bvSext
      ) where

    import           Data.Vector (Vector)
    import qualified Data.Vector as V
    import           Numeric.Natural

    import           GHC.TypeNats

    import qualified Data.BitVector.Sized as BV
    import           Data.Parameterized.NatRepr
    import           Data.Parameterized.Some(Some(..))

    import           What4.Interface(SymBV,Pred,SymInteger,IsExpr,SymExpr,IsExprBuilder,IsSymExprBuilder)
    import qualified What4.Interface as W
    import           What4.Panic (panic)

    -------------------------------------------------------------
    --
    -- | A What4 symbolic bitvector where the size does not appear in the type
    data SWord sym where

      DBV :: (IsExpr (SymExpr sym), 1<=w) => SymBV sym w -> SWord sym
      -- a bit-vector with positive length

      ZBV :: SWord sym
      -- a zero-length bit vector. i.e. 0

    instance Show (SWord sym) where
      show :: SWord sym -> String
    show (DBV SymBV sym w
    bv) = Doc Any -> String
    forall a. Show a => a -> String
    show (Doc Any -> String) -> Doc Any -> String
    forall a b. (a -> b) -> a -> b
    $ SymBV sym w -> Doc Any
    forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
    forall (e :: BaseType -> Type) (tp :: BaseType) ann.
    IsExpr e =>
    e tp -> Doc ann
    W.printSymExpr SymBV sym w
    bv
      show SWord sym
    ZBV      = String
    "0:[0]"

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

    -- | Return the signed value if this is a constant bitvector
    bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
    bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
    bvAsSignedInteger SWord sym
    ZBV = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    0
    bvAsSignedInteger (DBV (SymBV sym w
    bv :: SymBV sym w)) =
      NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv) (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> SymBV sym w -> Maybe (BV w)
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> Maybe (BV w)
    W.asBV SymBV sym w
    bv

    -- | Return the unsigned value if this is a constant bitvector
    bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
    bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
    bvAsUnsignedInteger SWord sym
    ZBV = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    0
    bvAsUnsignedInteger (DBV (SymBV sym w
    bv :: SymBV sym w)) =
      BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> SymBV sym w -> Maybe (BV w)
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> Maybe (BV w)
    W.asBV SymBV sym w
    bv

    unsignedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
    unsignedBVBounds :: forall sym.
    IsExprBuilder sym =>
    SWord sym -> Maybe (Integer, Integer)
    unsignedBVBounds SWord sym
    ZBV = (Integer, Integer) -> Maybe (Integer, Integer)
    forall a. a -> Maybe a
    Just (Integer
    0, Integer
    0)
    unsignedBVBounds (DBV SymBV sym w
    bv) = SymBV sym w -> Maybe (Integer, Integer)
    forall (w :: Natural).
    (1 <= w) =>
    SymExpr sym (BaseBVType w) -> Maybe (Integer, Integer)
    forall (e :: BaseType -> Type) (w :: Natural).
    (IsExpr e, 1 <= w) =>
    e (BaseBVType w) -> Maybe (Integer, Integer)
    W.unsignedBVBounds SymBV sym w
    bv

    signedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
    signedBVBounds :: forall sym.
    IsExprBuilder sym =>
    SWord sym -> Maybe (Integer, Integer)
    signedBVBounds SWord sym
    ZBV = (Integer, Integer) -> Maybe (Integer, Integer)
    forall a. a -> Maybe a
    Just (Integer
    0, Integer
    0)
    signedBVBounds (DBV SymBV sym w
    bv) = SymBV sym w -> Maybe (Integer, Integer)
    forall (w :: Natural).
    (1 <= w) =>
    SymExpr sym (BaseBVType w) -> Maybe (Integer, Integer)
    forall (e :: BaseType -> Type) (w :: Natural).
    (IsExpr e, 1 <= w) =>
    e (BaseBVType w) -> Maybe (Integer, Integer)
    W.signedBVBounds SymBV sym w
    bv

    -- | Convert an integer to an unsigned bitvector.
    --   The input value is reduced modulo 2^w.
    integerToBV :: forall sym width. (Show width, Integral width, IsExprBuilder sym) =>
      sym ->  SymInteger sym -> width -> IO (SWord sym)
    integerToBV :: forall sym width.
    (Show width, Integral width, IsExprBuilder sym) =>
    sym -> SymInteger sym -> width -> IO (SWord sym)
    integerToBV sym
    sym SymInteger sym
    i width
    w
      | Just (Some NatRepr x
    wr) <- width -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat width
    w
      , Just LeqProof 1 x
    LeqProof  <- NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    wr
      = SymBV sym x -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym x -> SWord sym) -> IO (SymBV sym x) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymInteger sym -> NatRepr x -> IO (SymBV sym x)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
    W.integerToBV sym
    sym SymInteger sym
    i NatRepr x
    wr
      | Integer
    0 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == width -> Integer
    forall a. Integral a => a -> Integer
    toInteger width
    w
      = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
      | Bool
    otherwise
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "integerToBV" [String
    "invalid bit-width", width -> String
    forall a. Show a => a -> String
    show width
    w]

    -- | Interpret the bit-vector as an unsigned integer
    bvToInteger :: forall sym. (IsExprBuilder sym) =>
      sym -> SWord sym -> IO (SymInteger sym)
    bvToInteger :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> IO (SymInteger sym)
    bvToInteger sym
    sym SWord sym
    ZBV      = sym -> Integer -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W.intLit sym
    sym Integer
    0
    bvToInteger sym
    sym (DBV SymBV sym w
    bv) = sym -> SymBV sym w -> IO (SymExpr sym BaseIntegerType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseIntegerType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymInteger sym)
    W.bvToInteger sym
    sym SymBV sym w
    bv

    -- | Interpret the bit-vector as a signed integer
    sbvToInteger :: forall sym. (IsExprBuilder sym) =>
      sym -> SWord sym -> IO (SymInteger sym)
    sbvToInteger :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> IO (SymInteger sym)
    sbvToInteger sym
    sym SWord sym
    ZBV      = sym -> Integer -> IO (SymExpr sym BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    W.intLit sym
    sym Integer
    0
    sbvToInteger sym
    sym (DBV SymBV sym w
    bv) = sym -> SymBV sym w -> IO (SymExpr sym BaseIntegerType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseIntegerType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymInteger sym)
    W.sbvToInteger sym
    sym SymBV sym w
    bv

    -- | Get the width of a bitvector
    bvWidth :: forall sym. SWord sym -> Integer
    bvWidth :: forall sym. SWord sym -> Integer
    bvWidth (DBV SymBV sym w
    x) = Integer -> Integer
    forall a. Num a => Integer -> a
    fromInteger (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x))
    bvWidth SWord sym
    ZBV = Integer
    0

    -- | Create a bitvector with the given width and value
    bvLit :: forall sym. IsExprBuilder sym =>
      sym -> Integer -> Integer -> IO (SWord sym)
    bvLit :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    bvLit sym
    _ Integer
    w Integer
    _
      | Integer
    w Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0
      = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    bvLit sym
    sym Integer
    w Integer
    dat
      | Just (Some NatRepr x
    rw) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    w
      , Just LeqProof 1 x
    LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    rw
      = SymBV sym x -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym x -> SWord sym) -> IO (SymBV sym x) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> NatRepr x -> BV x -> IO (SymBV sym x)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    W.bvLit sym
    sym NatRepr x
    rw (NatRepr x -> Integer -> BV x
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr x
    rw Integer
    dat)
      | Bool
    otherwise
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvLit" [String
    "size of bitvector is < 0 or >= maxInt", Integer -> String
    forall a. Show a => a -> String
    show Integer
    w]

    freshBV :: forall sym. IsSymExprBuilder sym =>
      sym -> W.SolverSymbol -> Integer -> IO (SWord sym)
    freshBV :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> Integer -> IO (SWord sym)
    freshBV sym
    sym SolverSymbol
    nm Integer
    w
      | Integer
    w Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0
      = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV

      | Just (Some NatRepr x
    rw) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    w
      , Just LeqProof 1 x
    LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    rw
      = SymBV sym x -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym x -> SWord sym) -> IO (SymBV sym x) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SolverSymbol -> BaseTypeRepr ('BaseBVType x) -> IO (SymBV sym x)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    forall (tp :: BaseType).
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    W.freshConstant sym
    sym SolverSymbol
    nm (NatRepr x -> BaseTypeRepr ('BaseBVType x)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    W.BaseBVRepr NatRepr x
    rw)

      | Bool
    otherwise
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "freshBV" [String
    "size of bitvector is < 0 or >= maxInt", Integer -> String
    forall a. Show a => a -> String
    show Integer
    w]

    bvFill :: forall sym. IsExprBuilder sym =>
      sym -> Integer -> Pred sym -> IO (SWord sym)
    bvFill :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Pred sym -> IO (SWord sym)
    bvFill sym
    sym Integer
    w Pred sym
    p
      | Integer
    w Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0
      = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV

      | Just (Some NatRepr x
    rw) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    w
      , Just LeqProof 1 x
    LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    rw
      = SymBV sym x -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym x -> SWord sym) -> IO (SymBV sym x) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> NatRepr x -> Pred sym -> IO (SymBV sym x)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
    W.bvFill sym
    sym NatRepr x
    rw Pred sym
    p

      | Bool
    otherwise
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvFill" [String
    "size of bitvector is < 0 or >= maxInt", Integer -> String
    forall a. Show a => a -> String
    show Integer
    w]

    -- | Returns true if the corresponding bit in the bitvector is set.
    --   NOTE bits are numbered in big-endian ordering, meaning the
    --   most-significant bit is bit 0
    bvAtBE :: forall sym.
      IsExprBuilder sym =>
      sym ->
      SWord sym ->
      Integer {- ^ Index of bit (0 is the most significant bit) -} ->
      IO (Pred sym)
    bvAtBE :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> Integer -> IO (Pred sym)
    bvAtBE sym
    sym (DBV SymBV sym w
    bv) Integer
    i = do
      let w :: Natural
    w   = NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv)
      let idx :: Natural
    idx = Natural
    w Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    1 Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger Integer
    i
      sym -> Natural -> SymBV sym w -> IO (Pred sym)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (Pred sym)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (Pred sym)
    W.testBitBV sym
    sym Natural
    idx SymBV sym w
    bv
    bvAtBE sym
    _ SWord sym
    ZBV Integer
    _ = String -> [String] -> IO (Pred sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvAtBE" [String
    "cannot index into empty bitvector"]

    -- | Returns true if the corresponding bit in the bitvector is set.
    --   NOTE bits are numbered in little-endian ordering, meaning the
    --   least-significant bit is bit 0
    bvAtLE :: forall sym.
      IsExprBuilder sym =>
      sym ->
      SWord sym ->
      Integer {- ^ Index of bit (0 is the most significant bit) -} ->
      IO (Pred sym)
    bvAtLE :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> Integer -> IO (Pred sym)
    bvAtLE sym
    sym (DBV SymBV sym w
    bv) Integer
    i =
      sym -> Natural -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (Pred sym)
    W.testBitBV sym
    sym (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger Integer
    i) SymBV sym w
    bv
    bvAtLE sym
    _ SWord sym
    ZBV Integer
    _ = String -> [String] -> IO (SymExpr sym BaseBoolType)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvAtLE" [String
    "cannot index into empty bitvector"]

    -- | Set the numbered bit in the given bitvector to the given
    --   bit value.
    --   NOTE bits are numbered in big-endian ordering, meaning the
    --   most-significant bit is bit 0
    bvSetBE :: forall sym.
      IsExprBuilder sym =>
      sym ->
      SWord sym ->
      Integer {- ^ Index of bit (0 is the most significant bit) -} ->
      Pred sym ->
      IO (SWord sym)
    bvSetBE :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
    bvSetBE sym
    _ SWord sym
    ZBV Integer
    _ Pred sym
    _ = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    bvSetBE sym
    sym (DBV SymBV sym w
    bv) Integer
    i Pred sym
    b =
      do let w :: Natural
    w = NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv)
         let idx :: Natural
    idx = Natural
    w Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    1 Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger Integer
    i
         SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
    W.bvSet sym
    sym SymBV sym w
    bv Natural
    idx Pred sym
    b

    -- | Set the numbered bit in the given bitvector to the given
    --   bit value.
    --   NOTE bits are numbered in big-endian ordering, meaning the
    --   most-significant bit is bit 0
    bvSetLE :: forall sym.
      IsExprBuilder sym =>
      sym ->
      SWord sym ->
      Integer {- ^ Index of bit (0 is the most significant bit) -} ->
      Pred sym ->
      IO (SWord sym)
    bvSetLE :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
    bvSetLE sym
    _ SWord sym
    ZBV Integer
    _ Pred sym
    _ = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    bvSetLE sym
    sym (DBV SymBV sym w
    bv) Integer
    i Pred sym
    b =
      SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
    W.bvSet sym
    sym SymBV sym w
    bv (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger Integer
    i) Pred sym
    b

    -- | Concatenate two bitvectors.
    bvJoin  :: forall sym. IsExprBuilder sym => sym
      -> SWord sym
      -- ^ most significant bits
      -> SWord sym
      -- ^ least significant bits
      -> IO (SWord sym)
    bvJoin :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvJoin sym
    _ SWord sym
    x SWord sym
    ZBV = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    x
    bvJoin sym
    _ SWord sym
    ZBV SWord sym
    x = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    x
    bvJoin sym
    sym (DBV SymBV sym w
    bv1) (DBV SymBV sym w
    bv2)
      | LeqProof 1 (w + w)
    LeqProof <- NatRepr w -> NatRepr w -> LeqProof 1 (w + w)
    forall (m :: Natural) (n :: Natural) (p :: Natural -> Type)
           (q :: Natural -> Type).
    (1 <= m, 1 <= n) =>
    p m -> q n -> LeqProof 1 (m + n)
    leqAddPos (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv1) (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv2)
      = SymBV sym (w + w) -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym (w + w) -> SWord sym)
    -> IO (SymBV sym (w + w)) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
    forall (u :: Natural) (v :: Natural).
    (1 <= u, 1 <= v) =>
    sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
    forall sym (u :: Natural) (v :: Natural).
    (IsExprBuilder sym, 1 <= u, 1 <= v) =>
    sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
    W.bvConcat sym
    sym SymBV sym w
    bv1 SymBV sym w
    bv2

    -- | Select a subsequence from a bitvector, with bits
    --   numbered in Big Endian order (most significant bit is 0).
    --   This fails if idx + n is >= w
    bvSliceBE :: forall sym. IsExprBuilder sym => sym
      -> Integer
      -- ^ Starting index, from 0 as most significant bit
      -> Integer
      -- ^ Number of bits to take
      -> SWord sym
      -> IO (SWord sym)
    bvSliceBE :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    bvSliceBE sym
    _ Integer
    _m Integer
    0 SWord sym
    _  = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure SWord sym
    forall sym. SWord sym
    ZBV
    bvSliceBE sym
    sym Integer
    m Integer
    n (DBV SymBV sym w
    bv)
      | Just (Some NatRepr x
    nr) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    n,
        Just LeqProof 1 x
    LeqProof  <- NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    nr,
        Just (Some NatRepr x
    mr) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    m,
        let wr :: NatRepr w
    wr = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv,
        Just LeqProof (x + x) w
    LeqProof <- NatRepr (x + x) -> NatRepr w -> Maybe (LeqProof (x + x) w)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (NatRepr x -> NatRepr x -> NatRepr (x + x)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr x
    mr NatRepr x
    nr)  NatRepr w
    wr,
        let idx :: NatRepr (w - (x + x))
    idx = NatRepr w -> NatRepr (x + x) -> NatRepr (w - (x + x))
    forall (n :: Natural) (m :: Natural).
    (n <= m) =>
    NatRepr m -> NatRepr n -> NatRepr (m - n)
    subNat NatRepr w
    wr (NatRepr x -> NatRepr x -> NatRepr (x + x)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr x
    mr NatRepr x
    nr),
        Just LeqProof ((w - (x + x)) + x) w
    LeqProof <- NatRepr ((w - (x + x)) + x)
    -> NatRepr w -> Maybe (LeqProof ((w - (x + x)) + x) w)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (NatRepr (w - (x + x)) -> NatRepr x -> NatRepr ((w - (x + x)) + x)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr (w - (x + x))
    idx NatRepr x
    nr) NatRepr w
    wr
      = SymBV sym x -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym x -> SWord sym) -> IO (SymBV sym x) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> NatRepr (w - (x + x))
    -> NatRepr x
    -> SymBV sym w
    -> IO (SymBV sym x)
    forall (idx :: Natural) (n :: Natural) (w :: Natural).
    (1 <= n, (idx + n) <= w) =>
    sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
    forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
    (IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
    sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
    W.bvSelect sym
    sym NatRepr (w - (x + x))
    idx NatRepr x
    nr SymBV sym w
    bv
      | Bool
    otherwise
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvSliceBE"
          [String
    "invalid arguments to slice: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    m String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    n
            String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " from vector of length " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> String
    forall a. Show a => a -> String
    show (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv)]
    bvSliceBE sym
    _ Integer
    m Integer
    n SWord sym
    ZBV
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvSliceBE"
          [String
    "invalid arguments to slice: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    m String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    n
            String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " from vector of length 0"]

    -- | Select a subsequence from a bitvector, with bits
    --   numbered in Little Endian order (least significant bit is 0).
    --   This fails if idx + n is >= w
    bvSliceLE :: forall sym. IsExprBuilder sym => sym
      -> Integer
      -- ^ Starting index, from 0 as most significant bit
      -> Integer
      -- ^ Number of bits to take
      -> SWord sym
      -> IO (SWord sym)
    bvSliceLE :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
    bvSliceLE sym
    _ Integer
    _m Integer
    0 SWord sym
    _  = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    bvSliceLE sym
    sym Integer
    m Integer
    n (DBV SymBV sym w
    bv)
      | Just (Some NatRepr x
    nr) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    n,
        Just LeqProof 1 x
    LeqProof  <- NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    nr,
        Just (Some NatRepr x
    mr) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    m,
        let wr :: NatRepr w
    wr = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv,
        Just LeqProof (x + x) w
    LeqProof <- NatRepr (x + x) -> NatRepr w -> Maybe (LeqProof (x + x) w)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (NatRepr x -> NatRepr x -> NatRepr (x + x)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr x
    mr NatRepr x
    nr) NatRepr w
    wr
      = SymBV sym x -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym x -> SWord sym) -> IO (SymBV sym x) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> NatRepr x -> NatRepr x -> SymBV sym w -> IO (SymBV sym x)
    forall (idx :: Natural) (n :: Natural) (w :: Natural).
    (1 <= n, (idx + n) <= w) =>
    sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
    forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
    (IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
    sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
    W.bvSelect sym
    sym NatRepr x
    mr NatRepr x
    nr SymBV sym w
    bv

      | Bool
    otherwise
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvSliceLE"
          [String
    "invalid arguments to slice: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    m String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    n
            String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " from vector of length " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> String
    forall a. Show a => a -> String
    show (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv)]
    bvSliceLE sym
    _ Integer
    m Integer
    n SWord sym
    ZBV
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvSliceLE"
          [String
    "invalid arguments to slice: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    m String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    n
            String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " from vector of length 0"]

    -- | Ceiling (log_2 x)
    -- adapted from saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
    w_bvLg2 :: forall sym w. (IsExprBuilder sym, 1 <= w) =>
       sym -> SymBV sym w -> IO (SymBV sym w)
    w_bvLg2 :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    w_bvLg2 sym
    sym SymBV sym w
    x = Integer -> IO (SymBV sym w)
    go Integer
    0
      where
        w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x
        size :: Integer
        size :: Integer
    size = NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr w
    w
        lit :: Integer -> IO (SymBV sym w)
        -- BGS: This change could lead to some inefficency
        lit :: Integer -> IO (SymBV sym w)
    lit Integer
    n = sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    W.bvLit sym
    sym NatRepr w
    w (NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w Integer
    n)
        go :: Integer -> IO (SymBV sym w)
        go :: Integer -> IO (SymBV sym w)
    go Integer
    i | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    size = do
               SymBV sym w
    x' <- Integer -> IO (SymBV sym w)
    lit (Integer
    2 Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    i)
               SymExpr sym BaseBoolType
    b' <- sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvUle sym
    sym SymBV sym w
    x SymBV sym w
    x'
               SymBV sym w
    th <- Integer -> IO (SymBV sym w)
    lit Integer
    i
               SymBV sym w
    el <- Integer -> IO (SymBV sym w)
    go (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1)
               sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvIte sym
    sym SymExpr sym BaseBoolType
    b' SymBV sym w
    th SymBV sym w
    el
             | Bool
    otherwise    = Integer -> IO (SymBV sym w)
    lit Integer
    i

    -- | If-then-else applied to bitvectors.
    bvIte :: forall sym. IsExprBuilder sym =>
      sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvIte :: forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvIte sym
    _ Pred sym
    _ SWord sym
    ZBV SWord sym
    ZBV
      = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    bvIte sym
    sym Pred sym
    p (DBV SymBV sym w
    bv1) (DBV SymBV sym w
    bv2)
      | Just BaseBVType w :~: BaseBVType w
    Refl <- BaseTypeRepr (BaseBVType w)
    -> BaseTypeRepr (BaseBVType w)
    -> Maybe (BaseBVType w :~: BaseBVType w)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality (SymBV sym w -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W.exprType SymBV sym w
    bv1) (SymBV sym w -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W.exprType SymBV sym w
    bv2)
      = SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvIte sym
    sym Pred sym
    p SymBV sym w
    bv1 SymBV sym w
    SymBV sym w
    bv2
    bvIte sym
    _ Pred sym
    _ SWord sym
    x SWord sym
    y
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvIte" [String
    "bit-vectors don't have same length", Integer -> String
    forall a. Show a => a -> String
    show (SWord sym -> Integer
    forall sym. SWord sym -> Integer
    bvWidth SWord sym
    x), Integer -> String
    forall a. Show a => a -> String
    show (SWord sym -> Integer
    forall sym. SWord sym -> Integer
    bvWidth SWord sym
    y)]

    ----------------------------------------------------------------------
    -- Convert to/from Vectors
    ----------------------------------------------------------------------

    -- | Explode a bitvector into a vector of booleans in Big Endian
    --   order (most significant bit first)
    bvUnpackBE :: forall sym. IsExprBuilder sym =>
      sym -> SWord sym -> IO (Vector (Pred sym))
    bvUnpackBE :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> IO (Vector (Pred sym))
    bvUnpackBE sym
    _   SWord sym
    ZBV = Vector (SymExpr sym BaseBoolType)
    -> IO (Vector (SymExpr sym BaseBoolType))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Vector (SymExpr sym BaseBoolType)
    forall a. Vector a
    V.empty
    bvUnpackBE sym
    sym (DBV SymBV sym w
    bv) = do
      let w :: Natural
          w :: Natural
    w = NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv)
      Int
    -> (Int -> IO (SymExpr sym BaseBoolType))
    -> IO (Vector (SymExpr sym BaseBoolType))
    forall (m :: Type -> Type) a.
    Monad m =>
    Int -> (Int -> m a) -> m (Vector a)
    V.generateM (Natural -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    w)
                  (\Int
    i -> sym -> Natural -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (Pred sym)
    W.testBitBV sym
    sym (Natural
    w Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    1 Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i) SymBV sym w
    bv)

    -- | Explode a bitvector into a vector of booleans in Little Endian
    --   order (least significant bit first)
    bvUnpackLE :: forall sym. IsExprBuilder sym =>
      sym -> SWord sym -> IO (Vector (Pred sym))
    bvUnpackLE :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> IO (Vector (Pred sym))
    bvUnpackLE sym
    _   SWord sym
    ZBV = Vector (SymExpr sym BaseBoolType)
    -> IO (Vector (SymExpr sym BaseBoolType))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Vector (SymExpr sym BaseBoolType)
    forall a. Vector a
    V.empty
    bvUnpackLE sym
    sym (DBV SymBV sym w
    bv) = do
      let w :: Natural
          w :: Natural
    w = NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    bv)
      Int
    -> (Int -> IO (SymExpr sym BaseBoolType))
    -> IO (Vector (SymExpr sym BaseBoolType))
    forall (m :: Type -> Type) a.
    Monad m =>
    Int -> (Int -> m a) -> m (Vector a)
    V.generateM (Natural -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    w)
                  (\Int
    i -> sym -> Natural -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Natural -> SymBV sym w -> IO (Pred sym)
    W.testBitBV sym
    sym (Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i) SymBV sym w
    bv)

    -- | convert a vector of booleans to a bitvector.  The input
    --   are used in Big Endian order (most significant bit first)
    bvPackBE :: forall sym. (W.IsExpr (W.SymExpr sym), IsExprBuilder sym) =>
      sym -> Vector (Pred sym) -> IO (SWord sym)
    bvPackBE :: forall sym.
    (IsExpr (SymExpr sym), IsExprBuilder sym) =>
    sym -> Vector (Pred sym) -> IO (SWord sym)
    bvPackBE sym
    sym Vector (Pred sym)
    vec = do
      Vector (SWord sym)
    vec' <- (Pred sym -> IO (SWord sym))
    -> Vector (Pred sym) -> IO (Vector (SWord sym))
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Vector a -> m (Vector b)
    V.mapM (\Pred sym
    p -> do
                         SWord sym
    v1 <- sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    bvLit sym
    sym Integer
    1 Integer
    1
                         SWord sym
    v2 <- sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    bvLit sym
    sym Integer
    1 Integer
    0
                         sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvIte sym
    sym Pred sym
    p SWord sym
    v1 SWord sym
    v2) Vector (Pred sym)
    vec
      (SWord sym -> SWord sym -> IO (SWord sym))
    -> SWord sym -> Vector (SWord sym) -> IO (SWord sym)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> b -> m a) -> a -> Vector b -> m a
    V.foldM (\SWord sym
    x SWord sym
    y -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvJoin sym
    sym SWord sym
    x SWord sym
    y) SWord sym
    forall sym. SWord sym
    ZBV Vector (SWord sym)
    vec'

    -- | convert a vector of booleans to a bitvector.  The inputs
    --   are used in Little Endian order (least significant bit first)
    bvPackLE :: forall sym. (W.IsExpr (W.SymExpr sym), IsExprBuilder sym) =>
      sym -> Vector (Pred sym) -> IO (SWord sym)
    bvPackLE :: forall sym.
    (IsExpr (SymExpr sym), IsExprBuilder sym) =>
    sym -> Vector (Pred sym) -> IO (SWord sym)
    bvPackLE sym
    sym Vector (Pred sym)
    vec = do
      Vector (SWord sym)
    vec' <- (Pred sym -> IO (SWord sym))
    -> Vector (Pred sym) -> IO (Vector (SWord sym))
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Vector a -> m (Vector b)
    V.mapM (\Pred sym
    p -> do
                         SWord sym
    v1 <- sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    bvLit sym
    sym Integer
    1 Integer
    1
                         SWord sym
    v2 <- sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    bvLit sym
    sym Integer
    1 Integer
    0
                         sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvIte sym
    sym Pred sym
    p SWord sym
    v1 SWord sym
    v2) Vector (Pred sym)
    vec
      (SWord sym -> SWord sym -> IO (SWord sym))
    -> SWord sym -> Vector (SWord sym) -> IO (SWord sym)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> b -> m a) -> a -> Vector b -> m a
    V.foldM (\SWord sym
    x SWord sym
    y -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvJoin sym
    sym SWord sym
    y SWord sym
    x) SWord sym
    forall sym. SWord sym
    ZBV Vector (SWord sym)
    vec'

    ----------------------------------------------------------------------
    -- Generic wrapper for unary operators
    ----------------------------------------------------------------------

    -- | Type of unary operation on bitvectors
    type SWordUn =
      forall sym. IsExprBuilder sym =>
      sym -> SWord sym -> IO (SWord sym)

    -- | Convert a unary operation on length indexed bvs to a unary operation
    -- on `SWord`
    bvUn ::  forall sym. IsExprBuilder sym =>
       (forall w. 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)) ->
       sym -> SWord sym -> IO (SWord sym)
    bvUn :: forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    bvUn forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    f sym
    sym (DBV SymBV sym w
    bv) = SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    f sym
    sym SymBV sym w
    bv
    bvUn forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    _ sym
    _  SWord sym
    ZBV = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV

    ----------------------------------------------------------------------
    -- Generic wrapper for binary operators that take two words
    -- of the same length
    ----------------------------------------------------------------------

    -- | type of binary operation that returns a bitvector
    type SWordBin =
      forall sym. IsExprBuilder sym =>
      sym -> SWord sym -> SWord sym -> IO (SWord sym)
    -- | type of binary operation that returns a boolean
    type PredBin =
      forall sym. IsExprBuilder sym =>
      sym -> SWord sym -> SWord sym -> IO (Pred sym)

    -- | convert binary operations that return bitvectors
    bvBin  :: forall sym. IsExprBuilder sym =>
      (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)) ->
      sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin :: forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    f sym
    sym (DBV SymBV sym w
    bv1) (DBV SymBV sym w
    bv2)
      | Just BaseBVType w :~: BaseBVType w
    Refl <- BaseTypeRepr (BaseBVType w)
    -> BaseTypeRepr (BaseBVType w)
    -> Maybe (BaseBVType w :~: BaseBVType w)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality (SymBV sym w -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W.exprType SymBV sym w
    bv1) (SymBV sym w -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W.exprType SymBV sym w
    bv2)
      = SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    f sym
    sym SymBV sym w
    bv1 SymBV sym w
    SymBV sym w
    bv2
    bvBin forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    _ sym
    _ SWord sym
    ZBV SWord sym
    ZBV
      = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    bvBin forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    _ sym
    _ SWord sym
    x SWord sym
    y
      = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvBin" [String
    "bit-vectors don't have same length", Integer -> String
    forall a. Show a => a -> String
    show (SWord sym -> Integer
    forall sym. SWord sym -> Integer
    bvWidth SWord sym
    x), Integer -> String
    forall a. Show a => a -> String
    show (SWord sym -> Integer
    forall sym. SWord sym -> Integer
    bvWidth SWord sym
    y)]

    -- | convert binary operations that return booleans (Pred)
    bvBinPred  :: forall sym. IsExprBuilder sym =>
      Bool {- ^ answer to give on 0-width bitvectors -} ->
      (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)) ->
      sym -> SWord sym -> SWord sym -> IO (Pred sym)
    bvBinPred :: forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    _ forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    f sym
    sym (DBV SymBV sym w
    bv1) (DBV SymBV sym w
    bv2)
      | Just BaseBVType w :~: BaseBVType w
    Refl <- BaseTypeRepr (BaseBVType w)
    -> BaseTypeRepr (BaseBVType w)
    -> Maybe (BaseBVType w :~: BaseBVType w)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality (SymBV sym w -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W.exprType SymBV sym w
    bv1) (SymBV sym w -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W.exprType SymBV sym w
    bv2)
      = sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    f sym
    sym SymBV sym w
    bv1 SymBV sym w
    SymBV sym w
    bv2
    bvBinPred Bool
    b forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    _ sym
    sym SWord sym
    ZBV SWord sym
    ZBV
      = Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (sym -> Bool -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
    W.backendPred sym
    sym Bool
    b)
    bvBinPred Bool
    _ forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    _ sym
    _ SWord sym
    x SWord sym
    y
      = String -> [String] -> IO (Pred sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvBinPred" [String
    "bit-vectors don't have same length", Integer -> String
    forall a. Show a => a -> String
    show (SWord sym -> Integer
    forall sym. SWord sym -> Integer
    bvWidth SWord sym
    x), Integer -> String
    forall a. Show a => a -> String
    show (SWord sym -> Integer
    forall sym. SWord sym -> Integer
    bvWidth SWord sym
    y)]

     -- Bitvector logical

    -- | Bitwise complement
    bvNot :: SWordUn
    bvNot :: SWordUn
    bvNot = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    bvUn sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W.bvNotBits

    -- | Bitwise logical and.
    bvAnd :: SWordBin
    bvAnd :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvAnd = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvAndBits

    -- | Bitwise logical or.
    bvOr :: SWordBin
    bvOr :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvOr = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvOrBits

    -- | Bitwise logical exclusive or.
    bvXor :: SWordBin
    bvXor :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvXor = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvXorBits

     -- Bitvector arithmetic

    -- | 2's complement negation.
    bvNeg :: SWordUn
    bvNeg :: SWordUn
    bvNeg = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    bvUn sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W.bvNeg

    -- | Add two bitvectors.
    bvAdd :: SWordBin
    bvAdd :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvAdd = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvAdd

    -- | Subtract one bitvector from another.
    bvSub :: SWordBin
    bvSub :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvSub = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvSub

    -- | Multiply one bitvector by another.
    bvMul :: SWordBin
    bvMul :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvMul = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvMul

    bvPopcount :: SWordUn
    bvPopcount :: SWordUn
    bvPopcount = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    bvUn sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W.bvPopcount

    bvCountLeadingZeros :: SWordUn
    bvCountLeadingZeros :: SWordUn
    bvCountLeadingZeros = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    bvUn sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W.bvCountLeadingZeros

    bvCountTrailingZeros :: SWordUn
    bvCountTrailingZeros :: SWordUn
    bvCountTrailingZeros = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    bvUn sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W.bvCountTrailingZeros

    bvForall :: W.IsSymExprBuilder sym =>
      sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
    bvForall :: forall sym.
    IsSymExprBuilder sym =>
    sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
    bvForall sym
    sym Natural
    n SWord sym -> IO (Pred sym)
    f =
      case String -> Either SolverSymbolError SolverSymbol
    W.userSymbol String
    "i" of
        Left SolverSymbolError
    err -> String -> [String] -> IO (Pred sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "bvForall" [SolverSymbolError -> String
    forall a. Show a => a -> String
    show SolverSymbolError
    err]
        Right SolverSymbol
    indexSymbol ->
          case Natural -> Some NatRepr
    mkNatRepr Natural
    n of
            Some NatRepr x
    w
              | Just LeqProof 1 x
    LeqProof <- NatRepr 1 -> NatRepr x -> Maybe (LeqProof 1 x)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1) NatRepr x
    w ->
                  do BoundVar sym ('BaseBVType x)
    i <- sym
    -> SolverSymbol
    -> BaseTypeRepr ('BaseBVType x)
    -> IO (BoundVar sym ('BaseBVType x))
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
    forall (tp :: BaseType).
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
    W.freshBoundVar sym
    sym SolverSymbol
    indexSymbol (BaseTypeRepr ('BaseBVType x) -> IO (BoundVar sym ('BaseBVType x)))
    -> BaseTypeRepr ('BaseBVType x)
    -> IO (BoundVar sym ('BaseBVType x))
    forall a b. (a -> b) -> a -> b
    $ NatRepr x -> BaseTypeRepr ('BaseBVType x)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    W.BaseBVRepr NatRepr x
    w
                     Pred sym
    body <- SWord sym -> IO (Pred sym)
    f (SWord sym -> IO (Pred sym))
    -> (SymExpr sym ('BaseBVType x) -> SWord sym)
    -> SymExpr sym ('BaseBVType x)
    -> IO (Pred sym)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SymExpr sym ('BaseBVType x) -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymExpr sym ('BaseBVType x) -> IO (Pred sym))
    -> SymExpr sym ('BaseBVType x) -> IO (Pred sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> BoundVar sym ('BaseBVType x) -> SymExpr sym ('BaseBVType x)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> BoundVar sym tp -> SymExpr sym tp
    forall (tp :: BaseType). sym -> BoundVar sym tp -> SymExpr sym tp
    W.varExpr sym
    sym BoundVar sym ('BaseBVType x)
    i
                     sym -> BoundVar sym ('BaseBVType x) -> Pred sym -> IO (Pred sym)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
    forall (tp :: BaseType).
    sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
    W.forallPred sym
    sym BoundVar sym ('BaseBVType x)
    i Pred sym
    body
              | Bool
    otherwise -> SWord sym -> IO (Pred sym)
    f SWord sym
    forall sym. SWord sym
    ZBV

    -- | Unsigned bitvector division.
    --
    --   The result is undefined when @y@ is zero,
    --   but is otherwise equal to @floor( x / y )@.
    bvUDiv :: SWordBin
    bvUDiv :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvUDiv = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvUdiv

    -- | Unsigned bitvector remainder.
    --
    --   The result is undefined when @y@ is zero,
    --   but is otherwise equal to @x - (bvUdiv x y) * y@.
    bvURem :: SWordBin
    bvURem :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvURem = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvUrem

    -- | Signed bitvector division.  The result is truncated to zero.
    --
    --   The result of @bvSdiv x y@ is undefined when @y@ is zero,
    --   but is equal to @floor(x/y)@ when @x@ and @y@ have the same sign,
    --   and equal to @ceiling(x/y)@ when @x@ and @y@ have opposite signs.
    --
    --   NOTE! However, that there is a corner case when dividing @MIN_INT@ by
    --   @-1@, in which case an overflow condition occurs, and the result is instead
    --   @MIN_INT@.
    bvSDiv :: SWordBin
    bvSDiv :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvSDiv = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvSdiv

    -- | Signed bitvector remainder.
    --
    --   The result of @bvSrem x y@ is undefined when @y@ is zero, but is
    --   otherwise equal to @x - (bvSdiv x y) * y@.
    bvSRem :: SWordBin
    bvSRem :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvSRem = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvBin sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvSrem

    bvLg2 :: SWordUn
    bvLg2 :: SWordUn
    bvLg2 = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> IO (SWord sym)
    bvUn sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    w_bvLg2

     -- Bitvector comparisons

    -- | Return true if bitvectors are equal.
    bvEq   :: PredBin
    bvEq :: PredBin
    bvEq = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    True sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvEq

    -- | Signed less-than-or-equal.
    bvsle  :: PredBin
    bvsle :: PredBin
    bvsle = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    True sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvSle

    -- | Signed less-than.
    bvslt  :: PredBin
    bvslt :: PredBin
    bvslt = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    False sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvSlt

    -- | Unsigned less-than-or-equal.
    bvule  :: PredBin
    bvule :: PredBin
    bvule = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    True sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvUle

    -- | Unsigned less-than.
    bvult  :: PredBin
    bvult :: PredBin
    bvult = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    False sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvUlt

    -- | Signed greater-than-or-equal.
    bvsge  :: PredBin
    bvsge :: PredBin
    bvsge = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    True sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvSge

    -- | Signed greater-than.
    bvsgt  :: PredBin
    bvsgt :: PredBin
    bvsgt = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    False sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvSgt

    -- | Unsigned greater-than-or-equal.
    bvuge  :: PredBin
    bvuge :: PredBin
    bvuge = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    True sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvUge

    -- | Unsigned greater-than.
    bvugt  :: PredBin
    bvugt :: PredBin
    bvugt = Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    Bool
    -> (forall (w :: Natural).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> sym
    -> SWord sym
    -> SWord sym
    -> IO (Pred sym)
    bvBinPred Bool
    False sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvUgt

    bvIsNonzero :: IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
    bvIsNonzero :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
    bvIsNonzero sym
    sym SWord sym
    ZBV = SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (sym -> SymExpr sym BaseBoolType
    forall sym. IsExprBuilder sym => sym -> Pred sym
    W.falsePred sym
    sym)
    bvIsNonzero sym
    sym (DBV SymBV sym w
    x) = sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    W.bvIsNonzero sym
    sym SymBV sym w
    x

    ----------------------------------------
    -- Bitvector shifts and rotates
    ----------------------------------------

    bvMin ::
      (IsExprBuilder sym, 1 <= w) =>
      sym ->
      W.SymBV sym w ->
      W.SymBV sym w ->
      IO (W.SymBV sym w)
    bvMin :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvMin sym
    sym SymBV sym w
    x SymBV sym w
    y =
      do SymExpr sym BaseBoolType
    p <- sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W.bvUle sym
    sym SymBV sym w
    x SymBV sym w
    y
         sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvIte sym
    sym SymExpr sym BaseBoolType
    p SymBV sym w
    x SymBV sym w
    y

    reduceShift ::
      IsExprBuilder sym =>
      (forall w. (1 <= w) => sym -> W.SymBV sym w -> W.SymBV sym w -> IO (W.SymBV sym w)) ->
      sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceShift :: forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceShift forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    _wop sym
    _sym SWord sym
    ZBV SWord sym
    _ = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    reduceShift forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    _wop sym
    _sym SWord sym
    x SWord sym
    ZBV = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    x
    reduceShift forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym (DBV SymBV sym w
    x) (DBV SymBV sym w
    y) =
      case NatRepr w -> NatRepr w -> NatComparison w w
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatComparison m n
    compareNat (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    y) of

        -- already the same size, apply the operation
        NatComparison w w
    NatEQ -> SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym SymBV sym w
    x SymBV sym w
    SymBV sym w
    y

        -- y is shorter, zero extend
        NatGT NatRepr y
    _diff ->
          do SymBV sym w
    y' <- sym -> NatRepr w -> SymBV sym w -> IO (SymBV sym w)
    forall (u :: Natural) (r :: Natural).
    (1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    forall sym (u :: Natural) (r :: Natural).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    W.bvZext sym
    sym (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) SymBV sym w
    y
             SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym SymBV sym w
    x SymBV sym w
    y'

        -- y is longer, clamp to the width of x then truncate.
        -- Truncation is OK because the value will always fit after
        -- clamping.
        NatLT NatRepr y
    _diff ->
          do SymBV sym w
    wx <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    W.bvLit sym
    sym (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    y) (NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    y) (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x)))
             SymBV sym w
    y' <- sym -> NatRepr w -> SymBV sym w -> IO (SymBV sym w)
    forall (r :: Natural) (w :: Natural).
    (1 <= r, (r + 1) <= w) =>
    sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
    forall sym (r :: Natural) (w :: Natural).
    (IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
    sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
    W.bvTrunc sym
    sym (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) (SymBV sym w -> IO (SymBV sym w))
    -> IO (SymBV sym w) -> IO (SymBV sym w)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvMin sym
    sym SymBV sym w
    y SymBV sym w
    wx
             SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym SymBV sym w
    x SymBV sym w
    y'

    reduceRotate ::
      IsExprBuilder sym =>
      (forall w. (1 <= w) => sym -> W.SymBV sym w -> W.SymBV sym w -> IO (W.SymBV sym w)) ->
      sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceRotate :: forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceRotate forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    _wop sym
    _sym SWord sym
    ZBV SWord sym
    _ = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    forall sym. SWord sym
    ZBV
    reduceRotate forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    _wop sym
    _sym SWord sym
    x SWord sym
    ZBV = SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SWord sym
    x
    reduceRotate forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym (DBV SymBV sym w
    x) (DBV SymBV sym w
    y) =
      case NatRepr w -> NatRepr w -> NatComparison w w
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatComparison m n
    compareNat (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    y) of

        -- already the same size, apply the operation
        NatComparison w w
    NatEQ -> SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym SymBV sym w
    x SymBV sym w
    SymBV sym w
    y

        -- y is shorter, zero extend
        NatGT NatRepr y
    _diff ->
          do SymBV sym w
    y' <- sym -> NatRepr w -> SymBV sym w -> IO (SymBV sym w)
    forall (u :: Natural) (r :: Natural).
    (1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    forall sym (u :: Natural) (r :: Natural).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    W.bvZext sym
    sym (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) SymBV sym w
    y
             SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym SymBV sym w
    x SymBV sym w
    y'

        -- y is longer, reduce modulo the width of x, then truncate
        -- Truncation is OK because the value will always
        -- fit after modulo reduction
        NatLT NatRepr y
    _diff ->
          do SymBV sym w
    wx <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    W.bvLit sym
    sym (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    y) (NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    y) (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x)))
             SymBV sym w
    y' <- sym -> NatRepr w -> SymBV sym w -> IO (SymBV sym w)
    forall (r :: Natural) (w :: Natural).
    (1 <= r, (r + 1) <= w) =>
    sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
    forall sym (r :: Natural) (w :: Natural).
    (IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
    sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
    W.bvTrunc sym
    sym (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) (SymBV sym w -> IO (SymBV sym w))
    -> IO (SymBV sym w) -> IO (SymBV sym w)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvUrem sym
    sym SymBV sym w
    y SymBV sym w
    wx
             SymBV sym w -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    wop sym
    sym SymBV sym w
    x SymBV sym w
    y'

    bvShl  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvShl :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvShl = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceShift sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvShl

    bvLshr  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvLshr :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvLshr = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceShift sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvLshr

    bvAshr :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvAshr :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvAshr = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceShift sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvAshr

    bvRol  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvRol :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvRol = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceRotate sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvRol

    bvRor  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvRor :: forall sym.
    IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
    bvRor = (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (w :: Natural).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
    reduceRotate sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W.bvRor

    -- | Zero-extend a value, adding the specified number of bits.
    bvZext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
    bvZext :: forall sym.
    IsExprBuilder sym =>
    sym -> Natural -> SWord sym -> IO (SWord sym)
    bvZext sym
    sym Natural
    n SWord sym
    sw =
      case Natural -> Some NatRepr
    mkNatRepr Natural
    n of
        Some (NatRepr x
    nr :: NatRepr n) ->
          case NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    nr of
            Maybe (LeqProof 1 x)
    Nothing -> SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure SWord sym
    sw
            Just lp :: LeqProof 1 x
    lp@LeqProof 1 x
    LeqProof ->
              case SWord sym
    sw of
                SWord sym
    ZBV -> sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    bvLit sym
    sym (Natural -> Integer
    forall a. Integral a => a -> Integer
    toInteger Natural
    n) Integer
    0
                DBV (SymBV sym w
    x :: W.SymBV sym w) ->
                  LeqProof (w + 1) (w + x)
    -> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (LeqProof w w -> LeqProof 1 x -> LeqProof (w + 1) (w + x)
    forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
    leqAdd2 (NatRepr w -> LeqProof w w
    forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
    leqRefl (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x)) LeqProof 1 x
    lp :: LeqProof (w+1) (w+n)) ((((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
    -> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall a b. (a -> b) -> a -> b
    $
                  LeqProof 1 (w + x)
    -> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (LeqProof 1 w -> NatRepr x -> LeqProof 1 (w + x)
    forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd LeqProof 1 w
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof NatRepr x
    nr :: LeqProof 1 (w+n)) (((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
    -> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall a b. (a -> b) -> a -> b
    $
                  SymBV sym (w + x) -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym (w + x) -> SWord sym)
    -> IO (SymBV sym (w + x)) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> NatRepr (w + x) -> SymBV sym w -> IO (SymBV sym (w + x))
    forall (u :: Natural) (r :: Natural).
    (1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    forall sym (u :: Natural) (r :: Natural).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    W.bvZext sym
    sym (NatRepr w -> NatRepr x -> NatRepr (w + x)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) NatRepr x
    nr) SymBV sym w
    x

    -- | Sign-extend a value, adding the specified number of bits.
    bvSext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
    bvSext :: forall sym.
    IsExprBuilder sym =>
    sym -> Natural -> SWord sym -> IO (SWord sym)
    bvSext sym
    sym Natural
    n SWord sym
    sw =
      case Natural -> Some NatRepr
    mkNatRepr Natural
    n of
        Some (NatRepr x
    nr :: NatRepr n) ->
          case NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    nr of
            Maybe (LeqProof 1 x)
    Nothing -> SWord sym -> IO (SWord sym)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure SWord sym
    sw
            Just lp :: LeqProof 1 x
    lp@LeqProof 1 x
    LeqProof ->
              case SWord sym
    sw of
                SWord sym
    ZBV -> sym -> Integer -> Integer -> IO (SWord sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
    bvLit sym
    sym (Natural -> Integer
    forall a. Integral a => a -> Integer
    toInteger Natural
    n) Integer
    0
                DBV (SymBV sym w
    x :: W.SymBV sym w) ->
                  LeqProof (w + 1) (w + x)
    -> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (LeqProof w w -> LeqProof 1 x -> LeqProof (w + 1) (w + x)
    forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
    leqAdd2 (NatRepr w -> LeqProof w w
    forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
    leqRefl (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x)) LeqProof 1 x
    lp :: LeqProof (w+1) (w+n)) ((((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
    -> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall a b. (a -> b) -> a -> b
    $
                  LeqProof 1 (w + x)
    -> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (LeqProof 1 w -> NatRepr x -> LeqProof 1 (w + x)
    forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd LeqProof 1 w
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof NatRepr x
    nr :: LeqProof 1 (w+n)) (((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
    -> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
    forall a b. (a -> b) -> a -> b
    $
                  SymBV sym (w + x) -> SWord sym
    forall sym (w :: Natural).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym (w + x) -> SWord sym)
    -> IO (SymBV sym (w + x)) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> NatRepr (w + x) -> SymBV sym w -> IO (SymBV sym (w + x))
    forall (u :: Natural) (r :: Natural).
    (1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    forall sym (u :: Natural) (r :: Natural).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    W.bvSext sym
    sym (NatRepr w -> NatRepr x -> NatRepr (w + x)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat (SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    W.bvWidth SymBV sym w
    x) NatRepr x
    nr) SymBV sym w
    x