    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Operations
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Constructors and basic operations on symbolic values
    -----------------------------------------------------------------------------

    {-# LANGUAGE BangPatterns #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Core.Operations
      (
      -- ** Basic constructors
        svTrue, svFalse, svBool
      , svInteger, svFloat, svDouble, svReal, svEnumFromThenTo, svString, svChar
      -- ** Basic destructors
      , svAsBool, svAsInteger, svNumerator, svDenominator
      -- ** Basic operations
      , svPlus, svTimes, svMinus, svUNeg, svAbs
      , svDivide, svQuot, svRem, svQuotRem
      , svEqual, svNotEqual, svStrongEqual, svSetEqual
      , svLessThan, svGreaterThan, svLessEq, svGreaterEq, svStructuralLessThan
      , svAnd, svOr, svXOr, svNot
      , svShl, svShr, svRol, svRor
      , svExtract, svJoin
      , svIte, svLazyIte, svSymbolicMerge
      , svSelect
      , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE
      , svExp, svFromIntegral
      -- ** Overflows
      , svMkOverflow
      -- ** Derived operations
      , svToWord1, svFromWord1, svTestBit
      , svShiftLeft, svShiftRight
      , svRotateLeft, svRotateRight
      , svBarrelRotateLeft, svBarrelRotateRight
      , svBlastLE, svBlastBE
      , svAddConstant, svIncrement, svDecrement
      -- ** Basic array operations
      , SArr,         readSArr,     writeSArr,     mergeSArr,     newSArr,     eqSArr
      , SFunArr(..),  readSFunArr,  writeSFunArr,  mergeSFunArr,  newSFunArr
      -- Utils
      , mkSymOp
      )
      where

    import Data.Bits (Bits(..))
    import Data.List (genericIndex, genericLength, genericTake)

    import qualified Data.IORef         as R    (modifyIORef', newIORef, readIORef)
    import qualified Data.Map.Strict    as Map  (toList, fromList, lookup)
    import qualified Data.IntMap.Strict as IMap (IntMap, empty, toAscList, fromAscList, lookup, size, insert)

    import Data.SBV.Core.AlgReals
    import Data.SBV.Core.Kind
    import Data.SBV.Core.Concrete
    import Data.SBV.Core.Symbolic

    import Data.Ratio

    import Data.SBV.Utils.Numeric (fpIsEqualObjectH)

    --------------------------------------------------------------------------------
    -- Basic constructors

    -- | Boolean True.
    svTrue :: SVal
    svTrue :: SVal
    svTrue = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left CV
    trueCV)

    -- | Boolean False.
    svFalse :: SVal
    svFalse :: SVal
    svFalse = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left CV
    falseCV)

    -- | Convert from a Boolean.
    svBool :: Bool -> SVal
    svBool :: Bool -> SVal
    svBool b :: Bool
    b = if Bool
    b then SVal
    svTrue else SVal
    svFalse

    -- | Convert from an Integer.
    svInteger :: Kind -> Integer -> SVal
    svInteger :: Kind -> Integer -> SVal
    svInteger k :: Kind
    k n :: Integer
    n = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    n)

    -- | Convert from a Float
    svFloat :: Float -> SVal
    svFloat :: Float -> SVal
    svFloat f :: Float
    f = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KFloat (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> CVal -> CV
    CV Kind
    KFloat (Float -> CVal
    CFloat Float
    f))

    -- | Convert from a Float
    svDouble :: Double -> SVal
    svDouble :: Double -> SVal
    svDouble d :: Double
    d = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KDouble (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> CVal -> CV
    CV Kind
    KDouble (Double -> CVal
    CDouble Double
    d))

    -- | Convert from a String
    svString :: String -> SVal
    svString :: String -> SVal
    svString s :: String
    s = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KString (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> CVal -> CV
    CV Kind
    KString (String -> CVal
    CString String
    s))

    -- | Convert from a Char
    svChar :: Char -> SVal
    svChar :: Char -> SVal
    svChar c :: Char
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KChar (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> CVal -> CV
    CV Kind
    KChar (Char -> CVal
    CChar Char
    c))

    -- | Convert from a Rational
    svReal :: Rational -> SVal
    svReal :: Rational -> SVal
    svReal d :: Rational
    d = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KReal (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> CVal -> CV
    CV Kind
    KReal (AlgReal -> CVal
    CAlgReal (Rational -> AlgReal
    forall a. Fractional a => Rational -> a
    fromRational Rational
    d)))

    --------------------------------------------------------------------------------
    -- Basic destructors

    -- | Extract a bool, by properly interpreting the integer stored.
    svAsBool :: SVal -> Maybe Bool
    svAsBool :: SVal -> Maybe Bool
    svAsBool (SVal _ (Left cv :: CV
    cv)) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (CV -> Bool
    cvToBool CV
    cv)
    svAsBool _                  = Maybe Bool
    forall a. Maybe a
    Nothing

    -- | Extract an integer from a concrete value.
    svAsInteger :: SVal -> Maybe Integer
    svAsInteger :: SVal -> Maybe Integer
    svAsInteger (SVal _ (Left (CV _ (CInteger n :: Integer
    n)))) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    n
    svAsInteger _                                   = Maybe Integer
    forall a. Maybe a
    Nothing

    -- | Grab the numerator of an SReal, if available
    svNumerator :: SVal -> Maybe Integer
    svNumerator :: SVal -> Maybe Integer
    svNumerator (SVal KReal (Left (CV KReal (CAlgReal (AlgRational True r :: Rational
    r))))) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
    forall a b. (a -> b) -> a -> b
    $ Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    r
    svNumerator _                                                              = Maybe Integer
    forall a. Maybe a
    Nothing

    -- | Grab the denominator of an SReal, if available
    svDenominator :: SVal -> Maybe Integer
    svDenominator :: SVal -> Maybe Integer
    svDenominator (SVal KReal (Left (CV KReal (CAlgReal (AlgRational True r :: Rational
    r))))) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
    forall a b. (a -> b) -> a -> b
    $ Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    r
    svDenominator _                                                              = Maybe Integer
    forall a. Maybe a
    Nothing

    -------------------------------------------------------------------------------------
    -- | Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite
    -- Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping
    -- it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus
    -- the lifting to Integers preserves the bounds; and then going back is just fine. So, things like @[1, 5 .. 200] :: [SInt8]@ work just
    -- fine (end evaluate to empty list), since we see @[1, 5 .. -56]@ in the @Integer@ domain. Also note the explicit check for @s /= f@
    -- below to make sure we don't stutter and produce an infinite list.
    svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]
    svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]
    svEnumFromThenTo bf :: SVal
    bf mbs :: Maybe SVal
    mbs bt :: SVal
    bt
      | Just bs :: SVal
    bs <- Maybe SVal
    mbs, Just f :: Integer
    f <- SVal -> Maybe Integer
    svAsInteger SVal
    bf, Just s :: Integer
    s <- SVal -> Maybe Integer
    svAsInteger SVal
    bs, Just t :: Integer
    t <- SVal -> Maybe Integer
    svAsInteger SVal
    bt, Integer
    s Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    f = [SVal] -> Maybe [SVal]
    forall a. a -> Maybe a
    Just ([SVal] -> Maybe [SVal]) -> [SVal] -> Maybe [SVal]
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SVal) -> [Integer] -> [SVal]
    forall a b. (a -> b) -> [a] -> [b]
    map (Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    bf)) [Integer
    f, Integer
    s .. Integer
    t]
      | Maybe SVal
    Nothing <- Maybe SVal
    mbs, Just f :: Integer
    f <- SVal -> Maybe Integer
    svAsInteger SVal
    bf,                           Just t :: Integer
    t <- SVal -> Maybe Integer
    svAsInteger SVal
    bt         = [SVal] -> Maybe [SVal]
    forall a. a -> Maybe a
    Just ([SVal] -> Maybe [SVal]) -> [SVal] -> Maybe [SVal]
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SVal) -> [Integer] -> [SVal]
    forall a b. (a -> b) -> [a] -> [b]
    map (Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    bf)) [Integer
    f    .. Integer
    t]
      | Bool
    True                                                                                                 = Maybe [SVal]
    forall a. Maybe a
    Nothing

    -------------------------------------------------------------------------------------
    -- Basic operations

    -- | Addition.
    svPlus :: SVal -> SVal -> SVal
    svPlus :: SVal -> SVal -> SVal
    svPlus x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    x = SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    y = SVal
    x
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 (Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp Op
    Plus) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> AlgReal
    forall a. Num a => a -> a -> a
    (+) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+) Float -> Float -> Float
    forall a. Num a => a -> a -> a
    (+) Double -> Double -> Double
    forall a. Num a => a -> a -> a
    (+) SVal
    x SVal
    y

    -- | Multiplication.
    svTimes :: SVal -> SVal -> SVal
    svTimes :: SVal -> SVal -> SVal
    svTimes x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    x = SVal
    x
      | SVal -> Bool
    isConcreteZero SVal
    y = SVal
    y
      | SVal -> Bool
    isConcreteOne SVal
    x  = SVal
    y
      | SVal -> Bool
    isConcreteOne SVal
    y  = SVal
    x
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 (Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp Op
    Times) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> AlgReal
    forall a. Num a => a -> a -> a
    (*) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (*) Float -> Float -> Float
    forall a. Num a => a -> a -> a
    (*) Double -> Double -> Double
    forall a. Num a => a -> a -> a
    (*) SVal
    x SVal
    y

    -- | Subtraction.
    svMinus :: SVal -> SVal -> SVal
    svMinus :: SVal -> SVal -> SVal
    svMinus x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    y = SVal
    x
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 (Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp Op
    Minus) CV -> CV -> Bool
    rationalCheck (-) (-) (-) (-) SVal
    x SVal
    y

    -- | Unary minus.
    svUNeg :: SVal -> SVal
    svUNeg :: SVal -> SVal
    svUNeg = (State -> Kind -> SV -> IO SV)
    -> (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> SVal
    -> SVal
    liftSym1 (Op -> State -> Kind -> SV -> IO SV
    mkSymOp1 Op
    UNeg) AlgReal -> AlgReal
    forall a. Num a => a -> a
    negate Integer -> Integer
    forall a. Num a => a -> a
    negate Float -> Float
    forall a. Num a => a -> a
    negate Double -> Double
    forall a. Num a => a -> a
    negate

    -- | Absolute value.
    svAbs :: SVal -> SVal
    svAbs :: SVal -> SVal
    svAbs = (State -> Kind -> SV -> IO SV)
    -> (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> SVal
    -> SVal
    liftSym1 (Op -> State -> Kind -> SV -> IO SV
    mkSymOp1 Op
    Abs) AlgReal -> AlgReal
    forall a. Num a => a -> a
    abs Integer -> Integer
    forall a. Num a => a -> a
    abs Float -> Float
    forall a. Num a => a -> a
    abs Double -> Double
    forall a. Num a => a -> a
    abs

    -- | Division.
    svDivide :: SVal -> SVal -> SVal
    svDivide :: SVal -> SVal -> SVal
    svDivide = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 (Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp Op
    Quot) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> AlgReal
    forall a. Fractional a => a -> a -> a
    (/) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    idiv Float -> Float -> Float
    forall a. Fractional a => a -> a -> a
    (/) Double -> Double -> Double
    forall a. Fractional a => a -> a -> a
    (/)
       where idiv :: a -> a -> a
    idiv x :: a
    x 0 = a
    x
             idiv x :: a
    x y :: a
    y = a
    x a -> a -> a
    forall a. Integral a => a -> a -> a
    `div` a
    y

    -- | Exponentiation.
    svExp :: SVal -> SVal -> SVal
    svExp :: SVal -> SVal -> SVal
    svExp b :: SVal
    b e :: SVal
    e
      | Just x :: Integer
    x <- SVal -> Maybe Integer
    svAsInteger SVal
    e
      = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0 then let go :: a -> SVal -> SVal
    go n :: a
    n v :: SVal
    v
                            | a
    n a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 = SVal
    one
                            | a -> Bool
    forall a. Integral a => a -> Bool
    even a
    n =             a -> SVal -> SVal
    go (a
    n a -> a -> a
    forall a. Integral a => a -> a -> a
    `div` 2) (SVal -> SVal -> SVal
    svTimes SVal
    v SVal
    v)
                            | Bool
    True   = SVal -> SVal -> SVal
    svTimes SVal
    v (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ a -> SVal -> SVal
    go (a
    n a -> a -> a
    forall a. Integral a => a -> a -> a
    `div` 2) (SVal -> SVal -> SVal
    svTimes SVal
    v SVal
    v)
                       in  Integer -> SVal -> SVal
    forall a. Integral a => a -> SVal -> SVal
    go Integer
    x SVal
    b
                  else String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "svExp: exponentiation: negative exponent: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    x
      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    e) Bool -> Bool -> Bool
    || SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    e
      = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "svExp: exponentiation only works with unsigned bounded symbolic exponents, kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    e)
      | Bool
    True
      = [SVal] -> SVal
    prod ([SVal] -> SVal) -> [SVal] -> SVal
    forall a b. (a -> b) -> a -> b
    $ (SVal -> SVal -> SVal) -> [SVal] -> [SVal] -> [SVal]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\use :: SVal
    use n :: SVal
    n -> SVal -> SVal -> SVal -> SVal
    svIte SVal
    use SVal
    n SVal
    one)
                       (SVal -> [SVal]
    svBlastLE SVal
    e)
                       ((SVal -> SVal) -> SVal -> [SVal]
    forall a. (a -> a) -> a -> [a]
    iterate (\x :: SVal
    x -> SVal -> SVal -> SVal
    svTimes SVal
    x SVal
    x) SVal
    b)
      where prod :: [SVal] -> SVal
    prod = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SVal -> SVal -> SVal
    svTimes SVal
    one
            one :: SVal
    one  = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    b) 1

    -- | Bit-blast: Little-endian. Assumes the input is a bit-vector.
    svBlastLE :: SVal -> [SVal]
    svBlastLE :: SVal -> [SVal]
    svBlastLE x :: SVal
    x = (Int -> SVal) -> [Int] -> [SVal]
    forall a b. (a -> b) -> [a] -> [b]
    map (SVal -> Int -> SVal
    svTestBit SVal
    x) [0 .. SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]

    -- | Set a given bit at index
    svSetBit :: SVal -> Int -> SVal
    svSetBit :: SVal -> Int -> SVal
    svSetBit x :: SVal
    x i :: Int
    i = SVal
    x SVal -> SVal -> SVal
    `svOr` Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x) (Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    i :: Integer)

    -- | Bit-blast: Big-endian. Assumes the input is a bit-vector.
    svBlastBE :: SVal -> [SVal]
    svBlastBE :: SVal -> [SVal]
    svBlastBE = [SVal] -> [SVal]
    forall a. [a] -> [a]
    reverse ([SVal] -> [SVal]) -> (SVal -> [SVal]) -> SVal -> [SVal]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> [SVal]
    svBlastLE

    -- | Un-bit-blast from big-endian representation to a word of the right size.
    -- The input is assumed to be unsigned.
    svWordFromLE :: [SVal] -> SVal
    svWordFromLE :: [SVal] -> SVal
    svWordFromLE bs :: [SVal]
    bs = SVal -> Int -> [SVal] -> SVal
    go SVal
    zero 0 [SVal]
    bs
      where zero :: SVal
    zero = Kind -> Integer -> SVal
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    False ([SVal] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SVal]
    bs)) 0
            go :: SVal -> Int -> [SVal] -> SVal
    go !SVal
    acc _  []     = SVal
    acc
            go !SVal
    acc !Int
    i (x :: SVal
    x:xs :: [SVal]
    xs) = SVal -> Int -> [SVal] -> SVal
    go (SVal -> SVal -> SVal -> SVal
    svIte SVal
    x (SVal -> Int -> SVal
    svSetBit SVal
    acc Int
    i) SVal
    acc) (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) [SVal]
    xs

    -- | Un-bit-blast from little-endian representation to a word of the right size.
    -- The input is assumed to be unsigned.
    svWordFromBE :: [SVal] -> SVal
    svWordFromBE :: [SVal] -> SVal
    svWordFromBE = [SVal] -> SVal
    svWordFromLE ([SVal] -> SVal) -> ([SVal] -> [SVal]) -> [SVal] -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SVal] -> [SVal]
    forall a. [a] -> [a]
    reverse

    -- | Add a constant value:
    svAddConstant :: Integral a => SVal -> a -> SVal
    svAddConstant :: SVal -> a -> SVal
    svAddConstant x :: SVal
    x i :: a
    i = SVal
    x SVal -> SVal -> SVal
    `svPlus` Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x) (a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    i)

    -- | Increment:
    svIncrement :: SVal -> SVal
    svIncrement :: SVal -> SVal
    svIncrement x :: SVal
    x = SVal -> Integer -> SVal
    forall a. Integral a => SVal -> a -> SVal
    svAddConstant SVal
    x (1::Integer)

    -- | Decrement:
    svDecrement :: SVal -> SVal
    svDecrement :: SVal -> SVal
    svDecrement x :: SVal
    x = SVal -> Integer -> SVal
    forall a. Integral a => SVal -> a -> SVal
    svAddConstant SVal
    x (-1 :: Integer)

    -- | Quotient: Overloaded operation whose meaning depends on the kind at which
    -- it is used: For unbounded integers, it corresponds to the SMT-Lib
    -- "div" operator ("Euclidean" division, which always has a
    -- non-negative remainder). For unsigned bitvectors, it is "bvudiv";
    -- and for signed bitvectors it is "bvsdiv", which rounds toward zero.
    -- Division by 0 is defined s.t. @x/0 = 0@, which holds even when @x@ itself is @0@.
    svQuot :: SVal -> SVal -> SVal
    svQuot :: SVal -> SVal -> SVal
    svQuot x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    x = SVal
    x
      | SVal -> Bool
    isConcreteZero SVal
    y = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x) 0
      | SVal -> Bool
    isConcreteOne  SVal
    y = SVal
    x
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 (Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp Op
    Quot) CV -> CV -> Bool
    nonzeroCheck
                                    (String -> AlgReal -> AlgReal -> AlgReal
    noReal "quot") Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    quot' (String -> Float -> Float -> Float
    noFloat "quot") (String -> Double -> Double -> Double
    noDouble "quot") SVal
    x SVal
    y
      where
        quot' :: a -> a -> a
    quot' a :: a
    a b :: a
    b | SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KUnbounded = a -> a -> a
    forall a. Integral a => a -> a -> a
    div a
    a (a -> a
    forall a. Num a => a -> a
    abs a
    b) a -> a -> a
    forall a. Num a => a -> a -> a
    * a -> a
    forall a. Num a => a -> a
    signum a
    b
                  | Bool
    otherwise              = a -> a -> a
    forall a. Integral a => a -> a -> a
    quot a
    a a
    b

    -- | Remainder: Overloaded operation whose meaning depends on the kind at which
    -- it is used: For unbounded integers, it corresponds to the SMT-Lib
    -- "mod" operator (always non-negative). For unsigned bitvectors, it
    -- is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds
    -- toward zero (sign of remainder matches that of @x@). Division by 0 is
    -- defined s.t. @x/0 = 0@, which holds even when @x@ itself is @0@.
    svRem :: SVal -> SVal -> SVal
    svRem :: SVal -> SVal -> SVal
    svRem x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    x = SVal
    x
      | SVal -> Bool
    isConcreteZero SVal
    y = SVal
    x
      | SVal -> Bool
    isConcreteOne  SVal
    y = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x) 0
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 (Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp Op
    Rem) CV -> CV -> Bool
    nonzeroCheck
                                    (String -> AlgReal -> AlgReal -> AlgReal
    noReal "rem") Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    rem' (String -> Float -> Float -> Float
    noFloat "rem") (String -> Double -> Double -> Double
    noDouble "rem") SVal
    x SVal
    y
      where
        rem' :: a -> a -> a
    rem' a :: a
    a b :: a
    b | SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KUnbounded = a -> a -> a
    forall a. Integral a => a -> a -> a
    mod a
    a (a -> a
    forall a. Num a => a -> a
    abs a
    b)
                 | Bool
    otherwise              = a -> a -> a
    forall a. Integral a => a -> a -> a
    rem a
    a a
    b

    -- | Combination of quot and rem
    svQuotRem :: SVal -> SVal -> (SVal, SVal)
    svQuotRem :: SVal -> SVal -> (SVal, SVal)
    svQuotRem x :: SVal
    x y :: SVal
    y = (SVal
    x SVal -> SVal -> SVal
    `svQuot` SVal
    y, SVal
    x SVal -> SVal -> SVal
    `svRem` SVal
    y)

    -- | Optimize away x == true and x /= false to x; otherwise just do eqOpt
    eqOptBool :: Op -> SV -> SV -> SV -> Maybe SV
    eqOptBool :: Op -> SV -> SV -> SV -> Maybe SV
    eqOptBool op :: Op
    op w :: SV
    w x :: SV
    x y :: SV
    y
      | Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool Bool -> Bool -> Bool
    && Op
    op Op -> Op -> Bool
    forall a. Eq a => a -> a -> Bool
    == Op
    Equal    Bool -> Bool -> Bool
    && SV
    x SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV  = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    y         -- true  .== y     --> y
      | Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool Bool -> Bool -> Bool
    && Op
    op Op -> Op -> Bool
    forall a. Eq a => a -> a -> Bool
    == Op
    Equal    Bool -> Bool -> Bool
    && SV
    y SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV  = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    x         -- x     .== true  --> x
      | Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool Bool -> Bool -> Bool
    && Op
    op Op -> Op -> Bool
    forall a. Eq a => a -> a -> Bool
    == Op
    NotEqual Bool -> Bool -> Bool
    && SV
    x SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    y         -- false ./= y     --> y
      | Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool Bool -> Bool -> Bool
    && Op
    op Op -> Op -> Bool
    forall a. Eq a => a -> a -> Bool
    == Op
    NotEqual Bool -> Bool -> Bool
    && SV
    y SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    x         -- x     ./= false --> x
      | Bool
    True                                         = SV -> SV -> SV -> Maybe SV
    eqOpt SV
    w SV
    x SV
    y    -- fallback
      where k :: Kind
    k = SV -> Kind
    swKind SV
    x

    -- | Equality.
    svEqual :: SVal -> SVal -> SVal
    svEqual :: SVal -> SVal -> SVal
    svEqual a :: SVal
    a b :: SVal
    b
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isSet SVal
    a Bool -> Bool -> Bool
    && SVal -> Bool
    forall a. HasKind a => a -> Bool
    isSet SVal
    b
      = SVal -> SVal -> SVal
    svSetEqual SVal
    a SVal
    b
      | Bool
    True
      = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> SVal
    -> SVal
    -> SVal
    liftSym2B ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC (Op -> SV -> SV -> SV -> Maybe SV
    eqOptBool Op
    Equal SV
    trueSV) Op
    Equal) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Float -> Float -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Double -> Double -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) [CVal] -> [CVal] -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) [CVal] -> [CVal] -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Maybe CVal -> Maybe CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Either CVal CVal -> Either CVal CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Maybe Int, String) -> (Maybe Int, String) -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) SVal
    a SVal
    b

    -- | Inequality.
    svNotEqual :: SVal -> SVal -> SVal
    svNotEqual :: SVal -> SVal -> SVal
    svNotEqual a :: SVal
    a b :: SVal
    b
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isSet SVal
    a Bool -> Bool -> Bool
    && SVal -> Bool
    forall a. HasKind a => a -> Bool
    isSet SVal
    b
      = SVal -> SVal
    svNot (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    svEqual SVal
    a SVal
    b
      | Bool
    True
      = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> SVal
    -> SVal
    -> SVal
    liftSym2B ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC (Op -> SV -> SV -> SV -> Maybe SV
    eqOptBool Op
    NotEqual SV
    falseSV) Op
    NotEqual) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Float -> Float -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Double -> Double -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) [CVal] -> [CVal] -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) [CVal] -> [CVal] -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Maybe CVal -> Maybe CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Either CVal CVal -> Either CVal CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) (Maybe Int, String) -> (Maybe Int, String) -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) SVal
    a SVal
    b

    -- | Set equality. Note that we only do constant folding if we get both a regular or both a
    -- complement set. Otherwise we get a symbolic value even if they might be completely concrete.
    svSetEqual :: SVal -> SVal -> SVal
    svSetEqual :: SVal -> SVal -> SVal
    svSetEqual sa :: SVal
    sa sb :: SVal
    sb
      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isSet SVal
    sa Bool -> Bool -> Bool
    && SVal -> Bool
    forall a. HasKind a => a -> Bool
    isSet SVal
    sb Bool -> Bool -> Bool
    && SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    sa Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    sb)
      = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.svSetEqual: Called on ill-typed args: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    sa, SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    sb)
      | Just (RegularSet a :: Set CVal
    a)    <- SVal -> Maybe (RCSet CVal)
    getSet SVal
    sa, Just (RegularSet b :: Set CVal
    b)    <- SVal -> Maybe (RCSet CVal)
    getSet SVal
    sb
      = Bool -> SVal
    svBool (Set CVal
    a Set CVal -> Set CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Set CVal
    b)
      | Just (ComplementSet a :: Set CVal
    a) <- SVal -> Maybe (RCSet CVal)
    getSet SVal
    sa, Just (ComplementSet b :: Set CVal
    b) <- SVal -> Maybe (RCSet CVal)
    getSet SVal
    sb
      = Bool -> SVal
    svBool (Set CVal
    a Set CVal -> Set CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Set CVal
    b)
      | Bool
    True
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where getSet :: SVal -> Maybe (RCSet CVal)
    getSet (SVal _ (Left (CV _ (CSet s :: RCSet CVal
    s)))) = RCSet CVal -> Maybe (RCSet CVal)
    forall a. a -> Maybe a
    Just RCSet CVal
    s
            getSet _                               = Maybe (RCSet CVal)
    forall a. Maybe a
    Nothing

            r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SVal -> IO SV
    svToSV State
    st SVal
    sa
                      SV
    svb <- State -> SVal -> IO SV
    svToSV State
    st SVal
    sb
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (SetOp -> Op
    SetOp SetOp
    SetEqual) [SV
    sva, SV
    svb]

    -- | Strong equality. Only matters on floats, where it says @NaN@ equals @NaN@ and @+0@ and @-0@ are different.
    -- Otherwise equivalent to `svEqual`.
    svStrongEqual :: SVal -> SVal -> SVal
    svStrongEqual :: SVal -> SVal -> SVal
    svStrongEqual x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isFloat SVal
    x, Just f1 :: Float
    f1 <- SVal -> Maybe Float
    getF SVal
    x, Just f2 :: Float
    f2 <- SVal -> Maybe Float
    getF SVal
    y
      = Bool -> SVal
    svBool (Bool -> SVal) -> Bool -> SVal
    forall a b. (a -> b) -> a -> b
    $ Float
    f1 Float -> Float -> Bool
    forall a. RealFloat a => a -> a -> Bool
    `fpIsEqualObjectH` Float
    f2
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isDouble SVal
    x, Just f1 :: Double
    f1 <- SVal -> Maybe Double
    getD SVal
    x, Just f2 :: Double
    f2 <- SVal -> Maybe Double
    getD SVal
    y
      = Bool -> SVal
    svBool (Bool -> SVal) -> Bool -> SVal
    forall a b. (a -> b) -> a -> b
    $ Double
    f1 Double -> Double -> Bool
    forall a. RealFloat a => a -> a -> Bool
    `fpIsEqualObjectH` Double
    f2
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isFloat SVal
    x Bool -> Bool -> Bool
    || SVal -> Bool
    forall a. HasKind a => a -> Bool
    isDouble SVal
    x
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      | Bool
    True
      = SVal -> SVal -> SVal
    svEqual SVal
    x SVal
    y
      where getF :: SVal -> Maybe Float
    getF (SVal _ (Left (CV _ (CFloat f :: Float
    f)))) = Float -> Maybe Float
    forall a. a -> Maybe a
    Just Float
    f
            getF _                                 = Maybe Float
    forall a. Maybe a
    Nothing

            getD :: SVal -> Maybe Double
    getD (SVal _ (Left (CV _ (CDouble d :: Double
    d)))) = Double -> Maybe Double
    forall a. a -> Maybe a
    Just Double
    d
            getD _                                  = Maybe Double
    forall a. Maybe a
    Nothing

            r :: State -> IO SV
    r st :: State
    st = do SV
    sx <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                      SV
    sy <- State -> SVal -> IO SV
    svToSV State
    st SVal
    y
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    FP_ObjEqual) [SV
    sx, SV
    sy])

    -- | Less than.
    svLessThan :: SVal -> SVal -> SVal
    svLessThan :: SVal -> SVal -> SVal
    svLessThan x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteMax SVal
    x = SVal
    svFalse
      | SVal -> Bool
    isConcreteMin SVal
    y = SVal
    svFalse
      | Bool
    True            = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> SVal
    -> SVal
    -> SVal
    liftSym2B ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC (SV -> SV -> SV -> Maybe SV
    eqOpt SV
    falseSV) Op
    LessThan) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) Float -> Float -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) Double -> Double -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) String -> String -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) Maybe CVal -> Maybe CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) Either CVal CVal -> Either CVal CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) (String
    -> (Int -> Int -> Bool)
    -> (Maybe Int, String)
    -> (Maybe Int, String)
    -> Bool
    uiLift "<" Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    (<)) SVal
    x SVal
    y

    -- | Greater than.
    svGreaterThan :: SVal -> SVal -> SVal
    svGreaterThan :: SVal -> SVal -> SVal
    svGreaterThan x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteMin SVal
    x = SVal
    svFalse
      | SVal -> Bool
    isConcreteMax SVal
    y = SVal
    svFalse
      | Bool
    True            = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> SVal
    -> SVal
    -> SVal
    liftSym2B ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC (SV -> SV -> SV -> Maybe SV
    eqOpt SV
    falseSV) Op
    GreaterThan) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) Float -> Float -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) Double -> Double -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) String -> String -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) Maybe CVal -> Maybe CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) Either CVal CVal -> Either CVal CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (>) (String
    -> (Int -> Int -> Bool)
    -> (Maybe Int, String)
    -> (Maybe Int, String)
    -> Bool
    uiLift ">"  Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    (>)) SVal
    x SVal
    y

    -- | Less than or equal to.
    svLessEq :: SVal -> SVal -> SVal
    svLessEq :: SVal -> SVal -> SVal
    svLessEq x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteMin SVal
    x = SVal
    svTrue
      | SVal -> Bool
    isConcreteMax SVal
    y = SVal
    svTrue
      | Bool
    True            = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> SVal
    -> SVal
    -> SVal
    liftSym2B ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC (SV -> SV -> SV -> Maybe SV
    eqOpt SV
    trueSV) Op
    LessEq) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) Float -> Float -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) Double -> Double -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) String -> String -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) Maybe CVal -> Maybe CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) Either CVal CVal -> Either CVal CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=) (String
    -> (Int -> Int -> Bool)
    -> (Maybe Int, String)
    -> (Maybe Int, String)
    -> Bool
    uiLift "<=" Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=)) SVal
    x SVal
    y

    -- | Greater than or equal to.
    svGreaterEq :: SVal -> SVal -> SVal
    svGreaterEq :: SVal -> SVal -> SVal
    svGreaterEq x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteMax SVal
    x = SVal
    svTrue
      | SVal -> Bool
    isConcreteMin SVal
    y = SVal
    svTrue
      | Bool
    True            = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> SVal
    -> SVal
    -> SVal
    liftSym2B ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC (SV -> SV -> SV -> Maybe SV
    eqOpt SV
    trueSV) Op
    GreaterEq) CV -> CV -> Bool
    rationalCheck AlgReal -> AlgReal -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) Float -> Float -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) Double -> Double -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) String -> String -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) [CVal] -> [CVal] -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) Maybe CVal -> Maybe CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) Either CVal CVal -> Either CVal CVal -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) (String
    -> (Int -> Int -> Bool)
    -> (Maybe Int, String)
    -> (Maybe Int, String)
    -> Bool
    uiLift ">=" Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=)) SVal
    x SVal
    y

    -- | Bitwise and.
    svAnd :: SVal -> SVal -> SVal
    svAnd :: SVal -> SVal -> SVal
    svAnd x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    x = SVal
    x
      | SVal -> Bool
    isConcreteOnes SVal
    x = SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    y = SVal
    y
      | SVal -> Bool
    isConcreteOnes SVal
    y = SVal
    x
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC SV -> SV -> Maybe SV
    opt Op
    And) ((CV -> Bool) -> CV -> CV -> Bool
    forall a b. a -> b -> a
    const (Bool -> CV -> Bool
    forall a b. a -> b -> a
    const Bool
    True)) (String -> AlgReal -> AlgReal -> AlgReal
    noReal ".&.") Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    (.&.) (String -> Float -> Float -> Float
    noFloat ".&.") (String -> Double -> Double -> Double
    noDouble ".&.") SVal
    x SVal
    y
      where opt :: SV -> SV -> Maybe SV
    opt a :: SV
    a b :: SV
    b
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV Bool -> Bool -> Bool
    || SV
    b SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    falseSV
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV                  = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    b
              | SV
    b SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV                  = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    a
              | Bool
    True                         = Maybe SV
    forall a. Maybe a
    Nothing

    -- | Bitwise or.
    svOr :: SVal -> SVal -> SVal
    svOr :: SVal -> SVal -> SVal
    svOr x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    x = SVal
    y
      | SVal -> Bool
    isConcreteOnes SVal
    x = SVal
    x
      | SVal -> Bool
    isConcreteZero SVal
    y = SVal
    x
      | SVal -> Bool
    isConcreteOnes SVal
    y = SVal
    y
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC SV -> SV -> Maybe SV
    opt Op
    Or) ((CV -> Bool) -> CV -> CV -> Bool
    forall a b. a -> b -> a
    const (Bool -> CV -> Bool
    forall a b. a -> b -> a
    const Bool
    True))
                           (String -> AlgReal -> AlgReal -> AlgReal
    noReal ".|.") Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    (.|.) (String -> Float -> Float -> Float
    noFloat ".|.") (String -> Double -> Double -> Double
    noDouble ".|.") SVal
    x SVal
    y
      where opt :: SV -> SV -> Maybe SV
    opt a :: SV
    a b :: SV
    b
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV Bool -> Bool -> Bool
    || SV
    b SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    trueSV
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV               = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    b
              | SV
    b SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV               = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    a
              | Bool
    True                       = Maybe SV
    forall a. Maybe a
    Nothing

    -- | Bitwise xor.
    svXOr :: SVal -> SVal -> SVal
    svXOr :: SVal -> SVal -> SVal
    svXOr x :: SVal
    x y :: SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    x = SVal
    y
      | SVal -> Bool
    isConcreteOnes SVal
    x = SVal -> SVal
    svNot SVal
    y
      | SVal -> Bool
    isConcreteZero SVal
    y = SVal
    x
      | SVal -> Bool
    isConcreteOnes SVal
    y = SVal -> SVal
    svNot SVal
    x
      | Bool
    True             = (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC SV -> SV -> Maybe SV
    opt Op
    XOr) ((CV -> Bool) -> CV -> CV -> Bool
    forall a b. a -> b -> a
    const (Bool -> CV -> Bool
    forall a b. a -> b -> a
    const Bool
    True))
                           (String -> AlgReal -> AlgReal -> AlgReal
    noReal "xor") Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    xor (String -> Float -> Float -> Float
    noFloat "xor") (String -> Double -> Double -> Double
    noDouble "xor") SVal
    x SVal
    y
      where opt :: SV -> SV -> Maybe SV
    opt a :: SV
    a b :: SV
    b
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    b Bool -> Bool -> Bool
    && SV -> Kind
    swKind SV
    a Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    falseSV
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV                = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    b
              | SV
    b SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV                = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    a
              | Bool
    True                        = Maybe SV
    forall a. Maybe a
    Nothing

    -- | Bitwise complement.
    svNot :: SVal -> SVal
    svNot :: SVal -> SVal
    svNot = (State -> Kind -> SV -> IO SV)
    -> (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> SVal
    -> SVal
    liftSym1 ((SV -> Maybe SV) -> Op -> State -> Kind -> SV -> IO SV
    mkSymOp1SC SV -> Maybe SV
    opt Op
    Not)
                     (String -> AlgReal -> AlgReal
    noRealUnary "complement") Integer -> Integer
    forall a. Bits a => a -> a
    complement
                     (String -> Float -> Float
    noFloatUnary "complement") (String -> Double -> Double
    noDoubleUnary "complement")
      where opt :: SV -> Maybe SV
    opt a :: SV
    a
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    trueSV
              | SV
    a SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV  = SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    falseSV
              | Bool
    True         = Maybe SV
    forall a. Maybe a
    Nothing

    -- | Shift left by a constant amount. Translates to the "bvshl"
    -- operation in SMT-Lib.
    --
    -- NB. Haskell spec says the behavior is undefined if the shift amount
    -- is negative. We arbitrarily return the value unchanged if this is the case.
    svShl :: SVal -> Int -> SVal
    svShl :: SVal -> Int -> SVal
    svShl x :: SVal
    x i :: Int
    i
      | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0
      = SVal
    x
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x, Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x
      = Kind -> Integer -> SVal
    svInteger Kind
    k 0
      | Bool
    True
      = SVal
    x SVal -> SVal -> SVal
    `svShiftLeft` Kind -> Integer -> SVal
    svInteger Kind
    k (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i)
      where k :: Kind
    k = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x

    -- | Shift right by a constant amount. Translates to either "bvlshr"
    -- (logical shift right) or "bvashr" (arithmetic shift right) in
    -- SMT-Lib, depending on whether @x@ is a signed bitvector.
    --
    -- NB. Haskell spec says the behavior is undefined if the shift amount
    -- is negative. We arbitrarily return the value unchanged if this is the case.
    svShr :: SVal -> Int -> SVal
    svShr :: SVal -> Int -> SVal
    svShr x :: SVal
    x i :: Int
    i
      | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0
      = SVal
    x
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x, Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x
      = if Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    x)
           then SVal
    z
           else SVal -> SVal -> SVal -> SVal
    svIte (SVal
    x SVal -> SVal -> SVal
    `svLessThan` SVal
    z) SVal
    neg1 SVal
    z
      | Bool
    True
      = SVal
    x SVal -> SVal -> SVal
    `svShiftRight` Kind -> Integer -> SVal
    svInteger Kind
    k (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i)
      where k :: Kind
    k    = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x
            z :: SVal
    z    = Kind -> Integer -> SVal
    svInteger Kind
    k 0
            neg1 :: SVal
    neg1 = Kind -> Integer -> SVal
    svInteger Kind
    k (-1)

    -- | Rotate-left, by a constant.
    --
    -- NB. Haskell spec says the behavior is undefined if the shift amount
    -- is negative. We arbitrarily return the value unchanged if this is the case.
    svRol :: SVal -> Int -> SVal
    svRol :: SVal -> Int -> SVal
    svRol x :: SVal
    x i :: Int
    i
      | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0
      = SVal
    x
      | Bool
    True
      = case SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x of
               KBounded _ sz :: Int
    sz -> (State -> Kind -> SV -> IO SV)
    -> (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> SVal
    -> SVal
    liftSym1 (Op -> State -> Kind -> SV -> IO SV
    mkSymOp1 (Int -> Op
    Rol (Int
    i Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    sz)))
                                         (String -> AlgReal -> AlgReal
    noRealUnary "rotateL") (Bool -> Int -> Int -> Integer -> Integer
    rot Bool
    True Int
    sz Int
    i)
                                         (String -> Float -> Float
    noFloatUnary "rotateL") (String -> Double -> Double
    noDoubleUnary "rotateL") SVal
    x
               _ -> SVal -> Int -> SVal
    svShl SVal
    x Int
    i   -- for unbounded Integers, rotateL is the same as shiftL in Haskell

    -- | Rotate-right, by a constant.
    --
    -- NB. Haskell spec says the behavior is undefined if the shift amount
    -- is negative. We arbitrarily return the value unchanged if this is the case.
    svRor :: SVal -> Int -> SVal
    svRor :: SVal -> Int -> SVal
    svRor x :: SVal
    x i :: Int
    i
      | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0
      = SVal
    x
      | Bool
    True
      = case SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x of
          KBounded _ sz :: Int
    sz -> (State -> Kind -> SV -> IO SV)
    -> (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> SVal
    -> SVal
    liftSym1 (Op -> State -> Kind -> SV -> IO SV
    mkSymOp1 (Int -> Op
    Ror (Int
    i Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    sz)))
                                    (String -> AlgReal -> AlgReal
    noRealUnary "rotateR") (Bool -> Int -> Int -> Integer -> Integer
    rot Bool
    False Int
    sz Int
    i)
                                    (String -> Float -> Float
    noFloatUnary "rotateR") (String -> Double -> Double
    noDoubleUnary "rotateR") SVal
    x
          _ -> SVal -> Int -> SVal
    svShr SVal
    x Int
    i   -- for unbounded integers, rotateR is the same as shiftR in Haskell

    -- | Generic rotation. Since the underlying representation is just Integers, rotations has to be
    -- careful on the bit-size.
    rot :: Bool -> Int -> Int -> Integer -> Integer
    rot :: Bool -> Int -> Int -> Integer -> Integer
    rot toLeft :: Bool
    toLeft sz :: Int
    sz amt :: Int
    amt x :: Integer
    x
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 2 = Integer
    x
      | Bool
    True   = Integer -> Int -> Integer
    forall a. (Bits a, Num a) => a -> Int -> a
    norm Integer
    x Int
    y' Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    y  Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer -> Int -> Integer
    forall a. (Bits a, Num a) => a -> Int -> a
    norm (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    y') Int
    y
      where (y :: Int
    y, y' :: Int
    y') | Bool
    toLeft = (Int
    amt Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    sz, Int
    sz Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    y)
                    | Bool
    True   = (Int
    sz Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    y', Int
    amt Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    sz)
            norm :: a -> Int -> a
    norm v :: a
    v s :: Int
    s = a
    v a -> a -> a
    forall a. Bits a => a -> a -> a
    .&. ((1 a -> Int -> a
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    s) a -> a -> a
    forall a. Num a => a -> a -> a
    - 1)

    -- | Extract bit-sequences.
    svExtract :: Int -> Int -> SVal -> SVal
    svExtract :: Int -> Int -> SVal -> SVal
    svExtract i :: Int
    i j :: Int
    j x :: SVal
    x@(SVal (KBounded s :: Bool
    s _) _)
      | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    j
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> CVal -> CV
    CV Kind
    k (Integer -> CVal
    CInteger 0))
      | SVal _ (Left (CV _ (CInteger v :: Integer
    v))) <- SVal
    x
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! CV -> CV
    normCV (Kind -> CVal -> CV
    CV Kind
    k (Integer -> CVal
    CInteger (Integer
    v Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    j))))
      | Bool
    True
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    y))
      where k :: Kind
    k = Bool -> Int -> Kind
    KBounded Bool
    s (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    j Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1)
            y :: State -> IO SV
    y st :: State
    st = do SV
    sv <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Int -> Op
    Extract Int
    i Int
    j) [SV
    sv])
    svExtract _ _ _ = String -> SVal
    forall a. HasCallStack => String -> a
    error "extract: non-bitvector type"

    -- | Join two words, by concataneting
    svJoin :: SVal -> SVal -> SVal
    svJoin :: SVal -> SVal -> SVal
    svJoin x :: SVal
    x@(SVal (KBounded s :: Bool
    s i :: Int
    i) a :: Either CV (Cached SV)
    a) y :: SVal
    y@(SVal (KBounded _ j :: Int
    j) b :: Either CV (Cached SV)
    b)
      | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 = SVal
    y
      | Int
    j Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 = SVal
    x
      | Left (CV _ (CInteger m :: Integer
    m)) <- Either CV (Cached SV)
    a, Left (CV _ (CInteger n :: Integer
    n)) <- Either CV (Cached SV)
    b
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $! Kind -> CVal -> CV
    CV Kind
    k (Integer -> CVal
    CInteger (Integer
    m Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    j Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    n)))
      | Bool
    True
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    z))
      where
        k :: Kind
    k = Bool -> Int -> Kind
    KBounded Bool
    s (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    j)
        z :: State -> IO SV
    z st :: State
    st = do SV
    xsw <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                  SV
    ysw <- State -> SVal -> IO SV
    svToSV State
    st SVal
    y
                  State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    Join [SV
    xsw, SV
    ysw])
    svJoin _ _ = String -> SVal
    forall a. HasCallStack => String -> a
    error "svJoin: non-bitvector type"

    -- | If-then-else. This one will force branches.
    svIte :: SVal -> SVal -> SVal -> SVal
    svIte :: SVal -> SVal -> SVal -> SVal
    svIte t :: SVal
    t a :: SVal
    a b :: SVal
    b = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    a) Bool
    True SVal
    t SVal
    a SVal
    b

    -- | Lazy If-then-else. This one will delay forcing the branches unless it's really necessary.
    svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal
    svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal
    svLazyIte k :: Kind
    k t :: SVal
    t a :: SVal
    a b :: SVal
    b = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge Kind
    k Bool
    False SVal
    t SVal
    a SVal
    b

    -- | Merge two symbolic values, at kind @k@, possibly @force@'ing the branches to make
    -- sure they do not evaluate to the same result.
    svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge k :: Kind
    k force :: Bool
    force t :: SVal
    t a :: SVal
    a b :: SVal
    b
      | Just r :: Bool
    r <- SVal -> Maybe Bool
    svAsBool SVal
    t
      = if Bool
    r then SVal
    a else SVal
    b
      | Bool
    force, SVal -> SVal -> Bool
    rationalSBVCheck SVal
    a SVal
    b, SVal -> SVal -> Bool
    sameResult SVal
    a SVal
    b
      = SVal
    a
      | Bool
    True
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    c
      where sameResult :: SVal -> SVal -> Bool
    sameResult (SVal _ (Left c1 :: CV
    c1)) (SVal _ (Left c2 :: CV
    c2)) = CV
    c1 CV -> CV -> Bool
    forall a. Eq a => a -> a -> Bool
    == CV
    c2
            sameResult _                  _                  = Bool
    False

            c :: State -> IO SV
    c st :: State
    st = do SV
    swt <- State -> SVal -> IO SV
    svToSV State
    st SVal
    t
                      case () of
                        () | SV
    swt SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV  -> State -> SVal -> IO SV
    svToSV State
    st SVal
    a       -- these two cases should never be needed as we expect symbolicMerge to be
                        () | SV
    swt SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV -> State -> SVal -> IO SV
    svToSV State
    st SVal
    b       -- called with symbolic tests, but just in case..
                        () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is,
                                    when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it
                                    is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if
                                    repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to
                                    our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going
                                    to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached"
                                    under the incorrect assumptions. To wit, consider the following:

                                       foo x y = ite (y .== 0) k (k+1)
                                         where k = ite (y .== 0) x (x+1)

                                    When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd
                                    like to share @k@, which would evaluate (correctly) to @x@ under the given assumption. When we backtrack and evaluate the 'else'
                                    branch of the first ite, we'd see @k@ is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value
                                    is @x@, which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.

                                    A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is,
                                    in the above example, we should record that the value of @k@ was cached under the assumption that @y@ is 0. While sound, this
                                    approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself.
                                    To wit, consider:

                                       foo x y = ite (y .== 0) k (k+1)
                                         where k = x+5

                                    If we tracked the assumptions, we would recompute @k@ twice, since the branch assumptions would differ. Clearly, there is no need to
                                    re-compute @k@ in this case since its value is independent of @y@. Note that the whole SBV performance story is based on agressive sharing,
                                    and losing that would have other significant ramifications.

                                    The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather
                                    than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this
                                    properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies
                                    transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the
                                    whole purpose of sharing in the first place.

                                    Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating
                                    unreachable branches. I think the simplicity is more important at this point than efficiency.

                                    Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the
                                    first program above should be written like this:

                                      foo x y = ite (y .== 0) x (x+2)

                                    In general, the following transformations should be done whenever possible:

                                      ite e1 (ite e1 e2 e3) e4  --> ite e1 e2 e4
                                      ite e1 e2 (ite e1 e3 e4)  --> ite e1 e2 e4

                                    This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer
                                    the following:

                                      ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5)

                                    especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of
                                    recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether.
                                 -}
                                 let sta :: State
    sta = State
    st State -> (SVal -> SVal) -> State
    `extendSValPathCondition` SVal -> SVal -> SVal
    svAnd SVal
    t
                                 let stb :: State
    stb = State
    st State -> (SVal -> SVal) -> State
    `extendSValPathCondition` SVal -> SVal -> SVal
    svAnd (SVal -> SVal
    svNot SVal
    t)
                                 SV
    swa <- State -> SVal -> IO SV
    svToSV State
    sta SVal
    a -- evaluate 'then' branch
                                 SV
    swb <- State -> SVal -> IO SV
    svToSV State
    stb SVal
    b -- evaluate 'else' branch

                                 -- merge, but simplify for certain boolean cases:
                                 case () of
                                   () | SV
    swa SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    swb                      -> SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    swa                                     -- if t then a      else a     ==> a
                                   () | SV
    swa SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV Bool -> Bool -> Bool
    && SV
    swb SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV -> SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    swt                                     -- if t then true   else false ==> t
                                   () | SV
    swa SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV Bool -> Bool -> Bool
    && SV
    swb SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    Not [SV
    swt])                -- if t then false  else true  ==> not t
                                   () | SV
    swa SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV                   -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    Or  [SV
    swt, SV
    swb])           -- if t then true   else b     ==> t OR b
                                   () | SV
    swa SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV                  -> do SV
    swt' <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp Op
    Not [SV
    swt])
                                                                              State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    And [SV
    swt', SV
    swb])       -- if t then false  else b     ==> t' AND b
                                   () | SV
    swb SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV                   -> do SV
    swt' <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp Op
    Not [SV
    swt])
                                                                              State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    Or [SV
    swt', SV
    swa])        -- if t then a      else true  ==> t' OR a
                                   () | SV
    swb SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV                  -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    And [SV
    swt, SV
    swa])           -- if t then a      else false ==> t AND a
                                   ()                                   -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    Ite [SV
    swt, SV
    swa, SV
    swb])

    -- | Total indexing operation. @svSelect xs default index@ is
    -- intuitively the same as @xs !! index@, except it evaluates to
    -- @default@ if @index@ overflows. Translates to SMT-Lib tables.
    svSelect :: [SVal] -> SVal -> SVal -> SVal
    svSelect :: [SVal] -> SVal -> SVal -> SVal
    svSelect xs :: [SVal]
    xs err :: SVal
    err ind :: SVal
    ind
      | SVal _ (Left c :: CV
    c) <- SVal
    ind =
        case CV -> CVal
    cvVal CV
    c of
          CInteger i :: Integer
    i -> if Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0 Bool -> Bool -> Bool
    || Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= [SVal] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [SVal]
    xs
                        then SVal
    err
                        else [SVal]
    xs [SVal] -> Integer -> SVal
    forall i a. Integral i => [a] -> i -> a
    `genericIndex` Integer
    i
          _          -> String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "SBV.select: unsupported " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    ind) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " valued select/index expression"
    svSelect xsOrig :: [SVal]
    xsOrig err :: SVal
    err ind :: SVal
    ind = [SVal]
    xs [SVal] -> SVal -> SVal
    forall a b. a -> b -> b
    `seq` Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kElt (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r))
      where
        kInd :: Kind
    kInd = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    ind
        kElt :: Kind
    kElt = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    err
        -- Based on the index size, we need to limit the elements. For
        -- instance if the index is 8 bits, but there are 257 elements,
        -- that last element will never be used and we can chop it off.
        xs :: [SVal]
    xs = case Kind
    kInd of
               KBounded False i :: Int
    i -> Integer -> [SVal] -> [SVal]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake ((2::Integer) Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    i) [SVal]
    xsOrig
               KBounded True  i :: Int
    i -> Integer -> [SVal] -> [SVal]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake ((2::Integer) Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1)) [SVal]
    xsOrig
               KUnbounded       -> [SVal]
    xsOrig
               _                -> String -> [SVal]
    forall a. HasCallStack => String -> a
    error (String -> [SVal]) -> String -> [SVal]
    forall a b. (a -> b) -> a -> b
    $ "SBV.select: unsupported " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    kInd String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " valued select/index expression"
        r :: State -> IO SV
    r st :: State
    st = do [SV]
    sws <- (SVal -> IO SV) -> [SVal] -> IO [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (State -> SVal -> IO SV
    svToSV State
    st) [SVal]
    xs
                  SV
    swe <- State -> SVal -> IO SV
    svToSV State
    st SVal
    err
                  if (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    swe) [SV]
    sws  -- off-chance that all elts are the same
                     then SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    swe
                     else do Int
    idx <- State -> Kind -> Kind -> [SV] -> IO Int
    getTableIndex State
    st Kind
    kInd Kind
    kElt [SV]
    sws
                             SV
    swi <- State -> SVal -> IO SV
    svToSV State
    st SVal
    ind
                             let len :: Int
    len = [SVal] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SVal]
    xs
                             -- NB. No need to worry here that the index
                             -- might be < 0; as the SMTLib translation
                             -- takes care of that automatically
                             State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kElt (Op -> [SV] -> SBVExpr
    SBVApp ((Int, Kind, Kind, Int) -> SV -> SV -> Op
    LkUp (Int
    idx, Kind
    kInd, Kind
    kElt, Int
    len) SV
    swi SV
    swe) [])

    -- Change the sign of a bit-vector quantity. Fails if passed a non-bv
    svChangeSign :: Bool -> SVal -> SVal
    svChangeSign :: Bool -> SVal -> SVal
    svChangeSign s :: Bool
    s x :: SVal
    x
      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x)       = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": Received non bit-vector kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x)
      | Just n :: Integer
    n <- SVal -> Maybe Integer
    svAsInteger SVal
    x = Kind -> Integer -> SVal
    svInteger Kind
    k Integer
    n
      | Bool
    True                    = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    y))
      where
        nm :: String
    nm = if Bool
    s then "svSign" else "svUnsign"

        k :: Kind
    k = Bool -> Int -> Kind
    KBounded Bool
    s (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x)
        y :: State -> IO SV
    y st :: State
    st = do SV
    xsw <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                  State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Int -> Op
    Extract (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) 0) [SV
    xsw])

    -- | Convert a symbolic bitvector from unsigned to signed.
    svSign :: SVal -> SVal
    svSign :: SVal -> SVal
    svSign = Bool -> SVal -> SVal
    svChangeSign Bool
    True

    -- | Convert a symbolic bitvector from signed to unsigned.
    svUnsign :: SVal -> SVal
    svUnsign :: SVal -> SVal
    svUnsign = Bool -> SVal -> SVal
    svChangeSign Bool
    False

    -- | Convert a symbolic bitvector from one integral kind to another.
    svFromIntegral :: Kind -> SVal -> SVal
    svFromIntegral :: Kind -> SVal -> SVal
    svFromIntegral kTo :: Kind
    kTo x :: SVal
    x
      | Just v :: Integer
    v <- SVal -> Maybe Integer
    svAsInteger SVal
    x
      = Kind -> Integer -> SVal
    svInteger Kind
    kTo Integer
    v
      | Bool
    True
      = SVal
    result
      where result :: SVal
    result = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kTo (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    y))
            kFrom :: Kind
    kFrom  = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x
            y :: State -> IO SV
    y st :: State
    st   = do SV
    xsw <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                        State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kTo (Op -> [SV] -> SBVExpr
    SBVApp (Kind -> Kind -> Op
    KindCast Kind
    kFrom Kind
    kTo) [SV
    xsw])

    --------------------------------------------------------------------------------
    -- Derived operations

    -- | Convert an SVal from kind Bool to an unsigned bitvector of size 1.
    svToWord1 :: SVal -> SVal
    svToWord1 :: SVal -> SVal
    svToWord1 b :: SVal
    b = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
    svSymbolicMerge Kind
    k Bool
    True SVal
    b (Kind -> Integer -> SVal
    svInteger Kind
    k 1) (Kind -> Integer -> SVal
    svInteger Kind
    k 0)
      where k :: Kind
    k = Bool -> Int -> Kind
    KBounded Bool
    False 1

    -- | Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool.
    svFromWord1 :: SVal -> SVal
    svFromWord1 :: SVal -> SVal
    svFromWord1 x :: SVal
    x = SVal -> SVal -> SVal
    svNotEqual SVal
    x (Kind -> Integer -> SVal
    svInteger Kind
    k 0)
      where k :: Kind
    k = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x

    -- | Test the value of a bit. Note that we do an extract here
    -- as opposed to masking and checking against zero, as we found
    -- extraction to be much faster with large bit-vectors.
    svTestBit :: SVal -> Int -> SVal
    svTestBit :: SVal -> Int -> SVal
    svTestBit x :: SVal
    x i :: Int
    i
      | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x = SVal -> SVal
    svFromWord1 (Int -> Int -> SVal -> SVal
    svExtract Int
    i Int
    i SVal
    x)
      | Bool
    True            = SVal
    svFalse

    -- | Generalization of 'svShl', where the shift-amount is symbolic.
    svShiftLeft :: SVal -> SVal -> SVal
    svShiftLeft :: SVal -> SVal -> SVal
    svShiftLeft = Bool -> SVal -> SVal -> SVal
    svShift Bool
    True

    -- | Generalization of 'svShr', where the shift-amount is symbolic.
    --
    -- NB. If the shiftee is signed, then this is an arithmetic shift;
    -- otherwise it's logical.
    svShiftRight :: SVal -> SVal -> SVal
    svShiftRight :: SVal -> SVal -> SVal
    svShiftRight = Bool -> SVal -> SVal -> SVal
    svShift Bool
    False

    -- | Generic shifting of bounded quantities. The shift amount must be non-negative and within the bounds of the argument
    -- for bit vectors. For negative shift amounts, the result is returned unchanged. For overshifts, left-shift produces 0,
    -- right shift produces 0 or -1 depending on the result being signed.
    svShift :: Bool -> SVal -> SVal -> SVal
    svShift :: Bool -> SVal -> SVal -> SVal
    svShift toLeft :: Bool
    toLeft x :: SVal
    x i :: SVal
    i
      | Just r :: SVal
    r <- Maybe SVal
    constFoldValue
      = SVal
    r
      | Bool
    cannotOverShift
      = SVal -> SVal -> SVal -> SVal
    svIte (SVal
    i SVal -> SVal -> SVal
    `svLessThan` Kind -> Integer -> SVal
    svInteger Kind
    ki 0)                                         -- Negative shift, no change
              SVal
    x
              SVal
    regularShiftValue
      | Bool
    True
      = SVal -> SVal -> SVal -> SVal
    svIte (SVal
    i SVal -> SVal -> SVal
    `svLessThan` Kind -> Integer -> SVal
    svInteger Kind
    ki 0)                                         -- Negative shift, no change
              SVal
    x
              (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal -> SVal
    svIte (SVal
    i SVal -> SVal -> SVal
    `svGreaterEq` Kind -> Integer -> SVal
    svInteger Kind
    ki (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x)))     -- Overshift, by at least the bit-width of x
                      SVal
    overShiftValue
                      SVal
    regularShiftValue

      where nm :: String
    nm | Bool
    toLeft = "shiftLeft"
               | Bool
    True   = "shiftRight"

            kx :: Kind
    kx = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x
            ki :: Kind
    ki = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    i

            -- Constant fold the result if possible. If either quantity is unbounded, then we only support constants
            -- as there's no easy/meaningful way to map this combo to SMTLib. Should be rarely needed, if ever!
            -- We also perform basic sanity check here so that if we go past here, we know we have bitvectors only.
            constFoldValue :: Maybe SVal
    constFoldValue
              | Just iv :: Integer
    iv <- SVal -> Maybe Integer
    getConst SVal
    i, Integer
    iv Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
              = SVal -> Maybe SVal
    forall a. a -> Maybe a
    Just SVal
    x

              | Just xv :: Integer
    xv <- SVal -> Maybe Integer
    getConst SVal
    x, Integer
    xv Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
              = SVal -> Maybe SVal
    forall a. a -> Maybe a
    Just SVal
    x

              | Just xv :: Integer
    xv <- SVal -> Maybe Integer
    getConst SVal
    x, Just iv :: Integer
    iv <- SVal -> Maybe Integer
    getConst SVal
    i
              = SVal -> Maybe SVal
    forall a. a -> Maybe a
    Just (SVal -> Maybe SVal) -> SVal -> Maybe SVal
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kx (Either CV (Cached SV) -> SVal)
    -> (CV -> Either CV (Cached SV)) -> CV -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> SVal) -> CV -> SVal
    forall a b. (a -> b) -> a -> b
    $! CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    kx (Integer -> CVal
    CInteger (Integer
    xv Integer -> Int -> Integer
    `opC` Integer -> Int
    shiftAmount Integer
    iv))

              | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isUnbounded SVal
    x Bool -> Bool -> Bool
    || SVal -> Bool
    forall a. HasKind a => a -> Bool
    isUnbounded SVal
    i
              = String -> Maybe SVal
    forall a. String -> a
    bailOut (String -> Maybe SVal) -> String -> Maybe SVal
    forall a b. (a -> b) -> a -> b
    $ "Not yet implemented unbounded/non-constants shifts for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    kx, Kind
    ki) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", please file a request!"

              | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x Bool -> Bool -> Bool
    && SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    i)
              = String -> Maybe SVal
    forall a. String -> a
    bailOut (String -> Maybe SVal) -> String -> Maybe SVal
    forall a b. (a -> b) -> a -> b
    $ "Unexpected kinds: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    kx, Kind
    ki)

              | Bool
    True
              = Maybe SVal
    forall a. Maybe a
    Nothing

              where bailOut :: String -> a
    bailOut m :: String
    m = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "SBV." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    m

                    getConst :: SVal -> Maybe Integer
    getConst (SVal _ (Left (CV _ (CInteger val :: Integer
    val)))) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    val
                    getConst _                                     = Maybe Integer
    forall a. Maybe a
    Nothing

                    opC :: Integer -> Int -> Integer
    opC | Bool
    toLeft = Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    shiftL
                        | Bool
    True   = Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    shiftR

                    -- like fromIntegral, but more paranoid
                    shiftAmount :: Integer -> Int
                    shiftAmount :: Integer -> Int
    shiftAmount iv :: Integer
    iv
                      | Integer
    iv Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0                                            = 0
                      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isUnbounded SVal
    i, Integer
    iv Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    forall a. Bounded a => a
    maxBound :: Int) = String -> Int
    forall a. String -> a
    bailOut (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "Unsupported constant unbounded shift with amount: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    iv
                      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isUnbounded SVal
    x                                      = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    iv
                      | Integer
    iv Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    ub                              = Int
    ub
                      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x Bool -> Bool -> Bool
    && SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    i)                   = String -> Int
    forall a. String -> a
    bailOut (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "Unsupported kinds: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    kx, Kind
    ki)
                      | Bool
    True                                               = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    iv
                     where ub :: Int
    ub = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x

            -- Overshift is not possible if the bit-size of x won't even fit into the bit-vector size
            -- of i. Note that this is a *necessary* check, Consider for instance if we're shifting a
            -- 32-bit value using a 1-bit shift amount (which can happen if the value is 1 with minimal
            -- shift widths). We would compare 1 >= 32, but stuffing 32 into bit-vector of size 1 would
            -- overflow. See http://github.com/LeventErkok/sbv/issues/323 for this case. Thus, we
            -- make sure that the bit-vector would fit as a value.
            cannotOverShift :: Bool
    cannotOverShift = Integer
    maxRepresentable Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x)
              where maxRepresentable :: Integer
                    maxRepresentable :: Integer
    maxRepresentable
                      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    i = Int -> Integer
    forall a. Bits a => Int -> a
    bit (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1
                      | Bool
    True      = Int -> Integer
    forall a. Bits a => Int -> a
    bit (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    i    ) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1

            -- An overshift occurs if we're shifting by more than or equal to the bit-width of x
            --     For shift-left: this value is always 0
            --     For shift-right:
            --        If x is unsigned: 0
            --        If x is signed and is less than 0, then -1 else 0
            overShiftValue :: SVal
    overShiftValue | Bool
    toLeft    = SVal
    zx
                           | SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    x = SVal -> SVal -> SVal -> SVal
    svIte (SVal
    x SVal -> SVal -> SVal
    `svLessThan` SVal
    zx) SVal
    neg1 SVal
    zx
                           | Bool
    True      = SVal
    zx
              where zx :: SVal
    zx   = Kind -> Integer -> SVal
    svInteger Kind
    kx 0
                    neg1 :: SVal
    neg1 = Kind -> Integer -> SVal
    svInteger Kind
    kx (-1)

            -- Regular shift, we know that the shift value fits into the bit-width of x, since it's between 0 and sizeOf x. So, we can just
            -- turn it into a properly sized argument and ship it to SMTLib
            regularShiftValue :: SVal
    regularShiftValue = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kx (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    result
               where result :: State -> IO SV
    result st :: State
    st = do SV
    sw1 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                                    SV
    sw2 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    i

                                    let op :: Op
    op | Bool
    toLeft = Op
    Shl
                                           | Bool
    True   = Op
    Shr

                                    SV
    adjustedShift <- if Kind
    kx Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    ki
                                                     then SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sw2
                                                     else State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kx (Op -> [SV] -> SBVExpr
    SBVApp (Kind -> Kind -> Op
    KindCast Kind
    ki Kind
    kx) [SV
    sw2])

                                    State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kx (Op -> [SV] -> SBVExpr
    SBVApp Op
    op [SV
    sw1, SV
    adjustedShift])

    -- | Generalization of 'svRol', where the rotation amount is symbolic.
    -- If the first argument is not bounded, then the this is the same as shift.
    svRotateLeft :: SVal -> SVal -> SVal
    svRotateLeft :: SVal -> SVal -> SVal
    svRotateLeft x :: SVal
    x i :: SVal
    i
      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x)
      = SVal -> SVal -> SVal
    svShiftLeft SVal
    x SVal
    i
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    i Bool -> Bool -> Bool
    && Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    si Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    sx            -- wrap-around not possible
      = SVal -> SVal -> SVal -> SVal
    svIte (SVal -> SVal -> SVal
    svLessThan SVal
    i SVal
    zi)
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRor` Int
    k | Int
    k <- [0 .. Int -> Int
    forall a. Bits a => Int -> a
    bit Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z (SVal -> SVal
    svUNeg SVal
    i))
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRol` Int
    k | Int
    k <- [0 .. Int -> Int
    forall a. Bits a => Int -> a
    bit Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z         SVal
    i)
      | Bool
    True
      = SVal -> SVal -> SVal -> SVal
    svIte (SVal -> SVal -> SVal
    svLessThan SVal
    i SVal
    zi)
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRor` Int
    k | Int
    k <- [0 .. Int
    sx     Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z (SVal -> SVal
    svUNeg SVal
    i SVal -> SVal -> SVal
    `svRem` SVal
    n))
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRol` Int
    k | Int
    k <- [0 .. Int
    sx     Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z (       SVal
    i SVal -> SVal -> SVal
    `svRem` SVal
    n))
        where sx :: Int
    sx = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x
              si :: Int
    si = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    i
              z :: SVal
    z  = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x) 0
              zi :: SVal
    zi = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    i) 0
              n :: SVal
    n  = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    i) (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    sx)

    -- | A variant of 'svRotateLeft' that uses a barrel-rotate design, which can lead to
    -- better verification code. Only works when both arguments are finite and the second
    -- argument is unsigned.
    svBarrelRotateLeft :: SVal -> SVal -> SVal
    svBarrelRotateLeft :: SVal -> SVal -> SVal
    svBarrelRotateLeft x :: SVal
    x i :: SVal
    i
      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x Bool -> Bool -> Bool
    && SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    i Bool -> Bool -> Bool
    && Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    i))
      = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.Dynamic.svBarrelRotateLeft: Arguments must be bounded with second argument unsigned. Received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (SVal, SVal) -> String
    forall a. Show a => a -> String
    show (SVal
    x, SVal
    i)
      | Just iv :: Integer
    iv <- SVal -> Maybe Integer
    svAsInteger SVal
    i
      = SVal -> Int -> SVal
    svRol SVal
    x (Int -> SVal) -> Int -> SVal
    forall a b. (a -> b) -> a -> b
    $ Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer
    iv Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x))
      | Bool
    True
      = (SVal -> Int -> SVal) -> SVal -> SVal -> SVal
    barrelRotate SVal -> Int -> SVal
    svRol SVal
    x SVal
    i

    -- | A variant of 'svRotateLeft' that uses a barrel-rotate design, which can lead to
    -- better verification code. Only works when both arguments are finite and the second
    -- argument is unsigned.
    svBarrelRotateRight :: SVal -> SVal -> SVal
    svBarrelRotateRight :: SVal -> SVal -> SVal
    svBarrelRotateRight x :: SVal
    x i :: SVal
    i
      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x Bool -> Bool -> Bool
    && SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    i Bool -> Bool -> Bool
    && Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    i))
      = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.Dynamic.svBarrelRotateRight: Arguments must be bounded with second argument unsigned. Received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (SVal, SVal) -> String
    forall a. Show a => a -> String
    show (SVal
    x, SVal
    i)
      | Just iv :: Integer
    iv <- SVal -> Maybe Integer
    svAsInteger SVal
    i
      = SVal -> Int -> SVal
    svRor SVal
    x (Int -> SVal) -> Int -> SVal
    forall a b. (a -> b) -> a -> b
    $ Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer
    iv Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x))
      | Bool
    True
      = (SVal -> Int -> SVal) -> SVal -> SVal -> SVal
    barrelRotate SVal -> Int -> SVal
    svRor SVal
    x SVal
    i

    -- Barrel rotation, by bit-blasting the argument:
    barrelRotate :: (SVal -> Int -> SVal) -> SVal -> SVal -> SVal
    barrelRotate :: (SVal -> Int -> SVal) -> SVal -> SVal -> SVal
    barrelRotate f :: SVal -> Int -> SVal
    f a :: SVal
    a c :: SVal
    c = [(SVal, Integer)] -> SVal -> SVal
    loop [(SVal, Integer)]
    blasted SVal
    a
      where loop :: [(SVal, Integer)] -> SVal -> SVal
            loop :: [(SVal, Integer)] -> SVal -> SVal
    loop []              acc :: SVal
    acc = SVal
    acc
            loop ((b :: SVal
    b, v :: Integer
    v) : rest :: [(SVal, Integer)]
    rest) acc :: SVal
    acc = [(SVal, Integer)] -> SVal -> SVal
    loop [(SVal, Integer)]
    rest (SVal -> SVal -> SVal -> SVal
    svIte SVal
    b (SVal -> Int -> SVal
    f SVal
    acc (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    v)) SVal
    acc)

            sa :: Integer
    sa = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    a
            n :: SVal
    n  = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    c) Integer
    sa

            -- Reduce by the modulus amount, we need not care about the
            -- any part larger than the value of the bit-size of the
            -- argument as it is identity for rotations
            reducedC :: SVal
    reducedC = SVal
    c SVal -> SVal -> SVal
    `svRem` SVal
    n

            -- blast little-endian, and zip with bit-position
            blasted :: [(SVal, Integer)]
    blasted = ((SVal, Integer) -> Bool) -> [(SVal, Integer)] -> [(SVal, Integer)]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile (SVal, Integer) -> Bool
    forall a. (a, Integer) -> Bool
    significant ([(SVal, Integer)] -> [(SVal, Integer)])
    -> [(SVal, Integer)] -> [(SVal, Integer)]
    forall a b. (a -> b) -> a -> b
    $ [SVal] -> [Integer] -> [(SVal, Integer)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (SVal -> [SVal]
    svBlastLE SVal
    reducedC) [2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    i | Integer
    i <- [(0::Integer)..]]

            -- Any term whose bit-position is larger than our input size
            -- is insignificant, since the reduction would've put 0's in those
            -- bits. For instance, if a is 32 bits, and c is 5 bits, then we
            -- need not look at any position i s.t. 2^i > 32
            significant :: (a, Integer) -> Bool
    significant (_, pos :: Integer
    pos) = Integer
    pos Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    sa

    -- | Generalization of 'svRor', where the rotation amount is symbolic.
    -- If the first argument is not bounded, then the this is the same as shift.
    svRotateRight :: SVal -> SVal -> SVal
    svRotateRight :: SVal -> SVal -> SVal
    svRotateRight x :: SVal
    x i :: SVal
    i
      | Bool -> Bool
    not (SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    x)
      = SVal -> SVal -> SVal
    svShiftRight SVal
    x SVal
    i
      | SVal -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SVal
    i Bool -> Bool -> Bool
    && Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    si Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    sx                   -- wrap-around not possible
      = SVal -> SVal -> SVal -> SVal
    svIte (SVal -> SVal -> SVal
    svLessThan SVal
    i SVal
    zi)
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRol` Int
    k | Int
    k <- [0 .. Int -> Int
    forall a. Bits a => Int -> a
    bit Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z (SVal -> SVal
    svUNeg SVal
    i))
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRor` Int
    k | Int
    k <- [0 .. Int -> Int
    forall a. Bits a => Int -> a
    bit Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z         SVal
    i)
      | Bool
    True
      = SVal -> SVal -> SVal -> SVal
    svIte (SVal -> SVal -> SVal
    svLessThan SVal
    i SVal
    zi)
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRol` Int
    k | Int
    k <- [0 .. Int
    sx     Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z (SVal -> SVal
    svUNeg SVal
    i SVal -> SVal -> SVal
    `svRem` SVal
    n))
              ([SVal] -> SVal -> SVal -> SVal
    svSelect [SVal
    x SVal -> Int -> SVal
    `svRor` Int
    k | Int
    k <- [0 .. Int
    sx     Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]] SVal
    z (       SVal
    i SVal -> SVal -> SVal
    `svRem` SVal
    n))
        where sx :: Int
    sx = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x
              si :: Int
    si = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    i
              z :: SVal
    z  = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x) 0
              zi :: SVal
    zi = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    i) 0
              n :: SVal
    n  = Kind -> Integer -> SVal
    svInteger (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    i) (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    sx)

    --------------------------------------------------------------------------------
    -- | Overflow detection.
    svMkOverflow :: OvOp -> SVal -> SVal -> SVal
    svMkOverflow :: OvOp -> SVal -> SVal -> SVal
    svMkOverflow o :: OvOp
    o x :: SVal
    x y :: SVal
    y = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r))
        where r :: State -> IO SV
    r st :: State
    st = do SV
    sx <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                        SV
    sy <- State -> SVal -> IO SV
    svToSV State
    st SVal
    y
                        State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (OvOp -> Op
    OverflowOp OvOp
    o) [SV
    sx, SV
    sy]

    ---------------------------------------------------------------------------------
    -- * Symbolic Arrays
    ---------------------------------------------------------------------------------

    -- | Arrays in terms of SMT-Lib arrays
    data SArr = SArr (Kind, Kind) (Cached ArrayIndex)

    -- | Read the array element at @a@
    readSArr :: SArr -> SVal -> SVal
    readSArr :: SArr -> SVal -> SVal
    readSArr (SArr (_, bk :: Kind
    bk) f :: Cached ArrayIndex
    f) a :: SVal
    a = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    bk (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where r :: State -> IO SV
    r st :: State
    st = do ArrayIndex
    arr <- Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI Cached ArrayIndex
    f State
    st
                      SV
    i   <- State -> SVal -> IO SV
    svToSV State
    st SVal
    a
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    bk (Op -> [SV] -> SBVExpr
    SBVApp (ArrayIndex -> Op
    ArrRead ArrayIndex
    arr) [SV
    i])

    -- | Update the element at @a@ to be @b@
    writeSArr :: SArr -> SVal -> SVal -> SArr
    writeSArr :: SArr -> SVal -> SVal -> SArr
    writeSArr (SArr ainfo :: (Kind, Kind)
    ainfo f :: Cached ArrayIndex
    f) a :: SVal
    a b :: SVal
    b = (Kind, Kind) -> Cached ArrayIndex -> SArr
    SArr (Kind, Kind)
    ainfo (Cached ArrayIndex -> SArr) -> Cached ArrayIndex -> SArr
    forall a b. (a -> b) -> a -> b
    $ (State -> IO ArrayIndex) -> Cached ArrayIndex
    forall a. (State -> IO a) -> Cached a
    cache State -> IO ArrayIndex
    g
      where g :: State -> IO ArrayIndex
    g st :: State
    st = do ArrayIndex
    arr  <- Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI Cached ArrayIndex
    f State
    st
                      SV
    addr <- State -> SVal -> IO SV
    svToSV State
    st SVal
    a
                      SV
    val  <- State -> SVal -> IO SV
    svToSV State
    st SVal
    b
                      ArrayMap
    amap <- IORef ArrayMap -> IO ArrayMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef ArrayMap
    rArrayMap State
    st)

                      let j :: ArrayIndex
    j   = Int -> ArrayIndex
    ArrayIndex (Int -> ArrayIndex) -> Int -> ArrayIndex
    forall a b. (a -> b) -> a -> b
    $ ArrayMap -> Int
    forall a. IntMap a -> Int
    IMap.size ArrayMap
    amap
                          upd :: ArrayMap -> ArrayMap
    upd = Int -> (String, (Kind, Kind), ArrayContext) -> ArrayMap -> ArrayMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert (ArrayIndex -> Int
    unArrayIndex ArrayIndex
    j) ("array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    j, (Kind, Kind)
    ainfo, ArrayIndex -> SV -> SV -> ArrayContext
    ArrayMutate ArrayIndex
    arr SV
    addr SV
    val)

                      ArrayIndex
    j ArrayIndex -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` State
    -> (State -> IORef ArrayMap)
    -> (ArrayMap -> ArrayMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef ArrayMap
    rArrayMap ArrayMap -> ArrayMap
    upd (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef ArrayMap) -> (ArrayMap -> ArrayMap) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef ArrayMap
    rNewArrs ArrayMap -> ArrayMap
    upd
                      ArrayIndex -> IO ArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArrayIndex
    j

    -- | Merge two given arrays on the symbolic condition
    -- Intuitively: @mergeArrays cond a b = if cond then a else b@.
    -- Merging pushes the if-then-else choice down on to elements
    mergeSArr :: SVal -> SArr -> SArr -> SArr
    mergeSArr :: SVal -> SArr -> SArr -> SArr
    mergeSArr t :: SVal
    t (SArr ainfo :: (Kind, Kind)
    ainfo a :: Cached ArrayIndex
    a) (SArr _ b :: Cached ArrayIndex
    b) = (Kind, Kind) -> Cached ArrayIndex -> SArr
    SArr (Kind, Kind)
    ainfo (Cached ArrayIndex -> SArr) -> Cached ArrayIndex -> SArr
    forall a b. (a -> b) -> a -> b
    $ (State -> IO ArrayIndex) -> Cached ArrayIndex
    forall a. (State -> IO a) -> Cached a
    cache State -> IO ArrayIndex
    h
      where h :: State -> IO ArrayIndex
    h st :: State
    st = do ArrayIndex
    ai <- Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI Cached ArrayIndex
    a State
    st
                      ArrayIndex
    bi <- Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI Cached ArrayIndex
    b State
    st
                      SV
    ts <- State -> SVal -> IO SV
    svToSV State
    st SVal
    t
                      ArrayMap
    amap <- IORef ArrayMap -> IO ArrayMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef ArrayMap
    rArrayMap State
    st)

                      let k :: ArrayIndex
    k   = Int -> ArrayIndex
    ArrayIndex (Int -> ArrayIndex) -> Int -> ArrayIndex
    forall a b. (a -> b) -> a -> b
    $ ArrayMap -> Int
    forall a. IntMap a -> Int
    IMap.size ArrayMap
    amap
                          upd :: ArrayMap -> ArrayMap
    upd = Int -> (String, (Kind, Kind), ArrayContext) -> ArrayMap -> ArrayMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert (ArrayIndex -> Int
    unArrayIndex ArrayIndex
    k) ("array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    k, (Kind, Kind)
    ainfo, SV -> ArrayIndex -> ArrayIndex -> ArrayContext
    ArrayMerge SV
    ts ArrayIndex
    ai ArrayIndex
    bi)

                      ArrayIndex
    k ArrayIndex -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` State
    -> (State -> IORef ArrayMap)
    -> (ArrayMap -> ArrayMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef ArrayMap
    rArrayMap ArrayMap -> ArrayMap
    upd (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef ArrayMap) -> (ArrayMap -> ArrayMap) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef ArrayMap
    rNewArrs ArrayMap -> ArrayMap
    upd
                      ArrayIndex -> IO ArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArrayIndex
    k

    -- | Create a named new array
    newSArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr
    newSArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr
    newSArr st :: State
    st ainfo :: (Kind, Kind)
    ainfo mkNm :: Int -> String
    mkNm mbDef :: Maybe SVal
    mbDef = do
        ArrayMap
    amap <- IORef ArrayMap -> IO ArrayMap
    forall a. IORef a -> IO a
    R.readIORef (IORef ArrayMap -> IO ArrayMap) -> IORef ArrayMap -> IO ArrayMap
    forall a b. (a -> b) -> a -> b
    $ State -> IORef ArrayMap
    rArrayMap State
    st

        Maybe SV
    mbSWDef <- case Maybe SVal
    mbDef of
                     Nothing -> Maybe SV -> IO (Maybe SV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe SV
    forall a. Maybe a
    Nothing
                     Just sv :: SVal
    sv -> SV -> Maybe SV
    forall a. a -> Maybe a
    Just (SV -> Maybe SV) -> IO SV -> IO (Maybe SV)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> State -> SVal -> IO SV
    svToSV State
    st SVal
    sv

        let i :: ArrayIndex
    i   = Int -> ArrayIndex
    ArrayIndex (Int -> ArrayIndex) -> Int -> ArrayIndex
    forall a b. (a -> b) -> a -> b
    $ ArrayMap -> Int
    forall a. IntMap a -> Int
    IMap.size ArrayMap
    amap
            nm :: String
    nm  = Int -> String
    mkNm (ArrayIndex -> Int
    unArrayIndex ArrayIndex
    i)
            upd :: ArrayMap -> ArrayMap
    upd = Int -> (String, (Kind, Kind), ArrayContext) -> ArrayMap -> ArrayMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert (ArrayIndex -> Int
    unArrayIndex ArrayIndex
    i) (String
    nm, (Kind, Kind)
    ainfo, Maybe SV -> ArrayContext
    ArrayFree Maybe SV
    mbSWDef)

        String -> State -> String -> IO ()
    registerLabel "SArray declaration" State
    st String
    nm

        State
    -> (State -> IORef ArrayMap)
    -> (ArrayMap -> ArrayMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef ArrayMap
    rArrayMap ArrayMap -> ArrayMap
    upd (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ State
    -> (IncState -> IORef ArrayMap) -> (ArrayMap -> ArrayMap) -> IO ()
    forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
    modifyIncState State
    st IncState -> IORef ArrayMap
    rNewArrs ArrayMap -> ArrayMap
    upd
        SArr -> IO SArr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SArr -> IO SArr) -> SArr -> IO SArr
    forall a b. (a -> b) -> a -> b
    $ (Kind, Kind) -> Cached ArrayIndex -> SArr
    SArr (Kind, Kind)
    ainfo (Cached ArrayIndex -> SArr) -> Cached ArrayIndex -> SArr
    forall a b. (a -> b) -> a -> b
    $ (State -> IO ArrayIndex) -> Cached ArrayIndex
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO ArrayIndex) -> Cached ArrayIndex)
    -> (State -> IO ArrayIndex) -> Cached ArrayIndex
    forall a b. (a -> b) -> a -> b
    $ IO ArrayIndex -> State -> IO ArrayIndex
    forall a b. a -> b -> a
    const (IO ArrayIndex -> State -> IO ArrayIndex)
    -> IO ArrayIndex -> State -> IO ArrayIndex
    forall a b. (a -> b) -> a -> b
    $ ArrayIndex -> IO ArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArrayIndex
    i

    -- | Compare two arrays for equality
    eqSArr :: SArr -> SArr -> SVal
    eqSArr :: SArr -> SArr -> SVal
    eqSArr (SArr _ a :: Cached ArrayIndex
    a) (SArr _ b :: Cached ArrayIndex
    b) = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    c
      where c :: State -> IO SV
    c st :: State
    st = do ArrayIndex
    ai <- Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI Cached ArrayIndex
    a State
    st
                      ArrayIndex
    bi <- Cached ArrayIndex -> State -> IO ArrayIndex
    uncacheAI Cached ArrayIndex
    b State
    st
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp (ArrayIndex -> ArrayIndex -> Op
    ArrEq ArrayIndex
    ai ArrayIndex
    bi) [])

    -- | Arrays managed internally
    data SFunArr = SFunArr (Kind, Kind) (Cached FArrayIndex)

    -- | Convert a node-id to an SVal
    nodeIdToSVal :: Kind -> Int -> SVal
    nodeIdToSVal :: Kind -> Int -> SVal
    nodeIdToSVal k :: Kind
    k i :: Int
    i = SV -> SVal
    swToSVal (SV -> SVal) -> SV -> SVal
    forall a b. (a -> b) -> a -> b
    $ Kind -> NodeId -> SV
    SV Kind
    k (Int -> NodeId
    NodeId Int
    i)

    -- | Convert an 'SV' to an 'SVal'
    swToSVal :: SV -> SVal
    swToSVal :: SV -> SVal
    swToSVal sv :: SV
    sv@(SV k :: Kind
    k _) = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
    forall a b. (a -> b) -> a -> b
    $ IO SV -> State -> IO SV
    forall a b. a -> b -> a
    const (IO SV -> State -> IO SV) -> IO SV -> State -> IO SV
    forall a b. (a -> b) -> a -> b
    $ SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv

    -- | A variant of SVal equality, but taking into account of constants
    -- NB. The rationalCheck is paranid perhaps, but is necessary in case
    -- we have some funky polynomial roots in there. We do allow for
    -- floating-points here though. Why? Because the Eq instance of 'CV'
    -- does the right thing by using object equality. (i.e., it does
    -- the right thing for NaN/+0/-0 etc.) A straightforward equality
    -- here would be wrong for floats!
    svEqualWithConsts :: (SVal, Maybe CV) -> (SVal, Maybe CV) -> SVal
    svEqualWithConsts :: (SVal, Maybe CV) -> (SVal, Maybe CV) -> SVal
    svEqualWithConsts sv1 :: (SVal, Maybe CV)
    sv1 sv2 :: (SVal, Maybe CV)
    sv2 = case ((SVal, Maybe CV) -> Maybe CV
    grabCV (SVal, Maybe CV)
    sv1, (SVal, Maybe CV) -> Maybe CV
    grabCV (SVal, Maybe CV)
    sv2) of
                                   (Just cv :: CV
    cv, Just cv' :: CV
    cv') | CV -> CV -> Bool
    rationalCheck CV
    cv CV
    cv' -> if CV
    cv CV -> CV -> Bool
    forall a. Eq a => a -> a -> Bool
    == CV
    cv' then SVal
    svTrue else SVal
    svFalse
                                   _                                          -> (SVal, Maybe CV) -> SVal
    forall a b. (a, b) -> a
    fst (SVal, Maybe CV)
    sv1 SVal -> SVal -> SVal
    `svEqual` (SVal, Maybe CV) -> SVal
    forall a b. (a, b) -> a
    fst (SVal, Maybe CV)
    sv2
      where grabCV :: (SVal, Maybe CV) -> Maybe CV
    grabCV (_,                Just cv :: CV
    cv) = CV -> Maybe CV
    forall a. a -> Maybe a
    Just CV
    cv
            grabCV (SVal _ (Left cv :: CV
    cv), _      ) = CV -> Maybe CV
    forall a. a -> Maybe a
    Just CV
    cv
            grabCV _                           = Maybe CV
    forall a. Maybe a
    Nothing

    -- | Read the array element at @a@. For efficiency purposes, we create a memo-table
    -- as we go along, as otherwise we suffer significant performance penalties. See:
    -- <http://github.com/LeventErkok/sbv/issues/402> and
    -- <http://github.com/LeventErkok/sbv/issues/396>.
    readSFunArr :: SFunArr -> SVal -> SVal
    readSFunArr :: SFunArr -> SVal -> SVal
    readSFunArr (SFunArr (ak :: Kind
    ak, bk :: Kind
    bk) f :: Cached FArrayIndex
    f) address :: SVal
    address
      | SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    address Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    ak
      = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.readSFunArr: Impossible happened, accesing with address type: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    address) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", expected: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ak
      | Bool
    True
      = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    bk (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where r :: State -> IO SV
    r st :: State
    st = do FArrayIndex
    fArrayIndex <- Cached FArrayIndex -> State -> IO FArrayIndex
    uncacheFAI Cached FArrayIndex
    f State
    st
                      FArrayMap
    fArrMap     <- IORef FArrayMap -> IO FArrayMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef FArrayMap
    rFArrayMap State
    st)

                      CnstMap
    constMap <- IORef CnstMap -> IO CnstMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef CnstMap
    rconstMap State
    st)
                      let consts :: Map Int CV
    consts = [(Int, CV)] -> Map Int CV
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Int
    i, CV
    cv) | (cv :: CV
    cv, SV _ (NodeId i :: Int
    i)) <- CnstMap -> [(CV, SV)]
    forall k a. Map k a -> [(k, a)]
    Map.toList CnstMap
    constMap]

                      case FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    fArrayIndex Int -> FArrayMap -> Maybe (SVal -> SVal, IORef (IntMap SV))
    forall a. Int -> IntMap a -> Maybe a
    `IMap.lookup` FArrayMap
    fArrMap of
                        Nothing -> String -> IO SV
    forall a. HasCallStack => String -> a
    error (String -> IO SV) -> String -> IO SV
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.readSFunArr: Impossible happened while trying to access SFunArray, can't find index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FArrayIndex -> String
    forall a. Show a => a -> String
    show FArrayIndex
    fArrayIndex
                        Just (uninitializedRead :: SVal -> SVal
    uninitializedRead, rCache :: IORef (IntMap SV)
    rCache) -> do
                            IntMap SV
    memoTable  <- IORef (IntMap SV) -> IO (IntMap SV)
    forall a. IORef a -> IO a
    R.readIORef IORef (IntMap SV)
    rCache
                            SV _ (NodeId addressNodeId :: Int
    addressNodeId) <- State -> SVal -> IO SV
    svToSV State
    st SVal
    address

                            -- If we hit the cache, return the result right away. If we miss, we need to
                            -- walk through each element to "merge" all possible reads as we do not know
                            -- whether the symbolic access may end up the same as one of the earlier ones
                            -- in the cache.
                            case Int
    addressNodeId Int -> IntMap SV -> Maybe SV
    forall a. Int -> IntMap a -> Maybe a
    `IMap.lookup` IntMap SV
    memoTable of
                              Just v :: SV
    v  -> SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    v  -- cache hit!

                              Nothing -> -- cache miss; walk down the cache items to form the chain of reads:
                                         do let aInfo :: (SVal, Maybe CV)
    aInfo = (SVal
    address, Int
    addressNodeId Int -> Map Int CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map Int CV
    consts)

                                                find :: [(Int, SV)] -> SVal
                                                find :: [(Int, SV)] -> SVal
    find []             = SVal -> SVal
    uninitializedRead SVal
    address
                                                find ((i :: Int
    i, v :: SV
    v) : ivs :: [(Int, SV)]
    ivs) = SVal -> SVal -> SVal -> SVal
    svIte ((SVal, Maybe CV) -> (SVal, Maybe CV) -> SVal
    svEqualWithConsts (Kind -> Int -> SVal
    nodeIdToSVal Kind
    ak Int
    i, Int
    i Int -> Map Int CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map Int CV
    consts) (SVal, Maybe CV)
    aInfo) (SV -> SVal
    swToSVal SV
    v) ([(Int, SV)] -> SVal
    find [(Int, SV)]
    ivs)

                                                finalValue :: SVal
    finalValue = [(Int, SV)] -> SVal
    find (IntMap SV -> [(Int, SV)]
    forall a. IntMap a -> [(Int, a)]
    IMap.toAscList IntMap SV
    memoTable)

                                            SV
    finalSW <- State -> SVal -> IO SV
    svToSV State
    st SVal
    finalValue

                                            -- Cache the result, so next time we can retrieve it faster if we look it up with the same address!
                                            -- The following line is really the whole point of having caching in SFunArray!
                                            IORef (IntMap SV) -> (IntMap SV -> IntMap SV) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    R.modifyIORef' IORef (IntMap SV)
    rCache (Int -> SV -> IntMap SV -> IntMap SV
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert Int
    addressNodeId SV
    finalSW)

                                            SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    finalSW

    -- | Update the element at @address@ to be @b@
    writeSFunArr :: SFunArr -> SVal -> SVal -> SFunArr
    writeSFunArr :: SFunArr -> SVal -> SVal -> SFunArr
    writeSFunArr (SFunArr (ak :: Kind
    ak, bk :: Kind
    bk) f :: Cached FArrayIndex
    f) address :: SVal
    address b :: SVal
    b
      | SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    address Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    ak
      = String -> SFunArr
    forall a. HasCallStack => String -> a
    error (String -> SFunArr) -> String -> SFunArr
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.writeSFunArr: Impossible happened, accesing with address type: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    address) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", expected: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ak
      | SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    b Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    bk
      = String -> SFunArr
    forall a. HasCallStack => String -> a
    error (String -> SFunArr) -> String -> SFunArr
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.writeSFunArr: Impossible happened, accesing with address type: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    b) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", expected: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    bk
      | Bool
    True
      = (Kind, Kind) -> Cached FArrayIndex -> SFunArr
    SFunArr (Kind
    ak, Kind
    bk) (Cached FArrayIndex -> SFunArr) -> Cached FArrayIndex -> SFunArr
    forall a b. (a -> b) -> a -> b
    $ (State -> IO FArrayIndex) -> Cached FArrayIndex
    forall a. (State -> IO a) -> Cached a
    cache State -> IO FArrayIndex
    g
      where g :: State -> IO FArrayIndex
    g st :: State
    st = do FArrayIndex
    fArrayIndex <- Cached FArrayIndex -> State -> IO FArrayIndex
    uncacheFAI Cached FArrayIndex
    f State
    st
                      FArrayMap
    fArrMap     <- IORef FArrayMap -> IO FArrayMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef FArrayMap
    rFArrayMap State
    st)
                      CnstMap
    constMap    <- IORef CnstMap -> IO CnstMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef CnstMap
    rconstMap State
    st)

                      let consts :: Map Int CV
    consts = [(Int, CV)] -> Map Int CV
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Int
    i, CV
    cv) | (cv :: CV
    cv, SV _ (NodeId i :: Int
    i)) <- CnstMap -> [(CV, SV)]
    forall k a. Map k a -> [(k, a)]
    Map.toList CnstMap
    constMap]

                      case FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    fArrayIndex Int -> FArrayMap -> Maybe (SVal -> SVal, IORef (IntMap SV))
    forall a. Int -> IntMap a -> Maybe a
    `IMap.lookup` FArrayMap
    fArrMap of
                        Nothing          -> String -> IO FArrayIndex
    forall a. HasCallStack => String -> a
    error (String -> IO FArrayIndex) -> String -> IO FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.writeSFunArr: Impossible happened while trying to access SFunArray, can't find index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FArrayIndex -> String
    forall a. Show a => a -> String
    show FArrayIndex
    fArrayIndex

                        Just (aUi :: SVal -> SVal
    aUi, rCache :: IORef (IntMap SV)
    rCache) -> do
                           IntMap SV
    memoTable <- IORef (IntMap SV) -> IO (IntMap SV)
    forall a. IORef a -> IO a
    R.readIORef IORef (IntMap SV)
    rCache
                           SV _ (NodeId addressNodeId :: Int
    addressNodeId) <- State -> SVal -> IO SV
    svToSV State
    st SVal
    address
                           SV
    val                         <- State -> SVal -> IO SV
    svToSV State
    st SVal
    b

                           -- There are three cases:
                           --
                           --    (1) We hit the cache, and old value is the same as new: No write necessary, just return the array
                           --    (2) We hit the cache, values are different. Simply insert, overriding the old-memo table location
                           --    (3) We miss the cache: Now we have to walk through all accesses and update the memo table accordingly.
                           --        Why? Just because we missed the cache doesn't mean that it's not there with a different "symbolic"
                           --        address. So, we have to walk through and update each entry in case the address matches.
                           --
                           -- Below, we determine which case we're in and then insert the value at the end and continue
                           Either FArrayIndex (IntMap SV)
    cont <- case Int
    addressNodeId Int -> IntMap SV -> Maybe SV
    forall a. Int -> IntMap a -> Maybe a
    `IMap.lookup` IntMap SV
    memoTable of
                                     Just oldVal :: SV
    oldVal                    -- Cache hit
                                       | SV
    val SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    oldVal -> Either FArrayIndex (IntMap SV)
    -> IO (Either FArrayIndex (IntMap SV))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either FArrayIndex (IntMap SV)
     -> IO (Either FArrayIndex (IntMap SV)))
    -> Either FArrayIndex (IntMap SV)
    -> IO (Either FArrayIndex (IntMap SV))
    forall a b. (a -> b) -> a -> b
    $ FArrayIndex -> Either FArrayIndex (IntMap SV)
    forall a b. a -> Either a b
    Left FArrayIndex
    fArrayIndex   -- Case 1
                                       | Bool
    True          -> Either FArrayIndex (IntMap SV)
    -> IO (Either FArrayIndex (IntMap SV))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either FArrayIndex (IntMap SV)
     -> IO (Either FArrayIndex (IntMap SV)))
    -> Either FArrayIndex (IntMap SV)
    -> IO (Either FArrayIndex (IntMap SV))
    forall a b. (a -> b) -> a -> b
    $ IntMap SV -> Either FArrayIndex (IntMap SV)
    forall a b. b -> Either a b
    Right IntMap SV
    memoTable    -- Case 2

                                     Nothing           -> do        -- Cache miss

                                            let aInfo :: (SVal, Maybe CV)
    aInfo = (SVal
    address, Int
    addressNodeId Int -> Map Int CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map Int CV
    consts)

                                                -- NB. The order of modifications here is important as we
                                                -- keep the keys in ascending order. (Since we'll call fromAscList later on.)
                                                walk :: [(Int, SV)] -> [(Int, SV)] -> IO [(Int, SV)]
                                                walk :: [(Int, SV)] -> [(Int, SV)] -> IO [(Int, SV)]
    walk []           sofar :: [(Int, SV)]
    sofar = [(Int, SV)] -> IO [(Int, SV)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Int, SV)] -> IO [(Int, SV)]) -> [(Int, SV)] -> IO [(Int, SV)]
    forall a b. (a -> b) -> a -> b
    $ [(Int, SV)] -> [(Int, SV)]
    forall a. [a] -> [a]
    reverse [(Int, SV)]
    sofar
                                                walk ((i :: Int
    i, s :: SV
    s):iss :: [(Int, SV)]
    iss) sofar :: [(Int, SV)]
    sofar = Int -> SV -> IO SV
    modify Int
    i SV
    s IO SV -> (SV -> IO [(Int, SV)]) -> IO [(Int, SV)]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \s' :: SV
    s' -> [(Int, SV)] -> [(Int, SV)] -> IO [(Int, SV)]
    walk [(Int, SV)]
    iss ((Int
    i, SV
    s') (Int, SV) -> [(Int, SV)] -> [(Int, SV)]
    forall a. a -> [a] -> [a]
    : [(Int, SV)]
    sofar)

                                                -- At the cached address i, currently storing value s. Conditionally update it to `b` (new value)
                                                -- if the addresses match. Otherwise keep it the same.
                                                modify :: Int -> SV -> IO SV
                                                modify :: Int -> SV -> IO SV
    modify i :: Int
    i s :: SV
    s = State -> SVal -> IO SV
    svToSV State
    st (SVal -> IO SV) -> SVal -> IO SV
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal -> SVal
    svIte ((SVal, Maybe CV) -> (SVal, Maybe CV) -> SVal
    svEqualWithConsts (Kind -> Int -> SVal
    nodeIdToSVal Kind
    ak Int
    i, Int
    i Int -> Map Int CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map Int CV
    consts) (SVal, Maybe CV)
    aInfo) SVal
    b (SV -> SVal
    swToSVal SV
    s)

                                            IntMap SV -> Either FArrayIndex (IntMap SV)
    forall a b. b -> Either a b
    Right (IntMap SV -> Either FArrayIndex (IntMap SV))
    -> ([(Int, SV)] -> IntMap SV)
    -> [(Int, SV)]
    -> Either FArrayIndex (IntMap SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Int, SV)] -> IntMap SV
    forall a. [(Int, a)] -> IntMap a
    IMap.fromAscList ([(Int, SV)] -> Either FArrayIndex (IntMap SV))
    -> IO [(Int, SV)] -> IO (Either FArrayIndex (IntMap SV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Int, SV)] -> [(Int, SV)] -> IO [(Int, SV)]
    walk (IntMap SV -> [(Int, SV)]
    forall a. IntMap a -> [(Int, a)]
    IMap.toAscList IntMap SV
    memoTable) []

                           case Either FArrayIndex (IntMap SV)
    cont of
                             Left j :: FArrayIndex
    j   -> FArrayIndex -> IO FArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return FArrayIndex
    j  -- There was a hit, and value was unchanged, nothing to do

                             Right mt :: IntMap SV
    mt -> do        -- There was a hit, and the value was different; or there was a miss. Insert the new value
                                                   -- and create a new array. Note that we keep the aUi the same: Just because we modified
                                                   -- an array, it doesn't mean we change the uninitialized reads: they still come from the same place.
                                                   --
                                            IORef (IntMap SV)
    newMemoTable <- IntMap SV -> IO (IORef (IntMap SV))
    forall a. a -> IO (IORef a)
    R.newIORef (IntMap SV -> IO (IORef (IntMap SV)))
    -> IntMap SV -> IO (IORef (IntMap SV))
    forall a b. (a -> b) -> a -> b
    $ Int -> SV -> IntMap SV -> IntMap SV
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert Int
    addressNodeId SV
    val IntMap SV
    mt

                                            let j :: FArrayIndex
    j = Int -> FArrayIndex
    FArrayIndex (Int -> FArrayIndex) -> Int -> FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ FArrayMap -> Int
    forall a. IntMap a -> Int
    IMap.size FArrayMap
    fArrMap
                                                upd :: FArrayMap -> FArrayMap
    upd = Int -> (SVal -> SVal, IORef (IntMap SV)) -> FArrayMap -> FArrayMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert (FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    j) (SVal -> SVal
    aUi, IORef (IntMap SV)
    newMemoTable)

                                            FArrayIndex
    j FArrayIndex -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` State
    -> (State -> IORef FArrayMap)
    -> (FArrayMap -> FArrayMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef FArrayMap
    rFArrayMap FArrayMap -> FArrayMap
    upd (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
                                            FArrayIndex -> IO FArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return FArrayIndex
    j

    -- | Merge two given arrays on the symbolic condition
    -- Intuitively: @mergeArrays cond a b = if cond then a else b@.
    -- Merging pushes the if-then-else choice down on to elements
    mergeSFunArr :: SVal -> SFunArr -> SFunArr -> SFunArr
    mergeSFunArr :: SVal -> SFunArr -> SFunArr -> SFunArr
    mergeSFunArr t :: SVal
    t array1 :: SFunArr
    array1@(SFunArr ainfo :: (Kind, Kind)
    ainfo@(sourceKind :: Kind
    sourceKind, targetKind :: Kind
    targetKind) a :: Cached FArrayIndex
    a) array2 :: SFunArr
    array2@(SFunArr binfo :: (Kind, Kind)
    binfo b :: Cached FArrayIndex
    b)
      | (Kind, Kind)
    ainfo (Kind, Kind) -> (Kind, Kind) -> Bool
    forall a. Eq a => a -> a -> Bool
    /= (Kind, Kind)
    binfo
      = String -> SFunArr
    forall a. HasCallStack => String -> a
    error (String -> SFunArr) -> String -> SFunArr
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.mergeSFunArr: Impossible happened, merging incompatbile arrays: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ((Kind, Kind), (Kind, Kind)) -> String
    forall a. Show a => a -> String
    show ((Kind, Kind)
    ainfo, (Kind, Kind)
    binfo)
      | Just test :: Bool
    test <- SVal -> Maybe Bool
    svAsBool SVal
    t
      = if Bool
    test then SFunArr
    array1 else SFunArr
    array2
      | Bool
    True
      = (Kind, Kind) -> Cached FArrayIndex -> SFunArr
    SFunArr (Kind, Kind)
    ainfo (Cached FArrayIndex -> SFunArr) -> Cached FArrayIndex -> SFunArr
    forall a b. (a -> b) -> a -> b
    $ (State -> IO FArrayIndex) -> Cached FArrayIndex
    forall a. (State -> IO a) -> Cached a
    cache State -> IO FArrayIndex
    c
      where c :: State -> IO FArrayIndex
    c st :: State
    st = do FArrayIndex
    ai <- Cached FArrayIndex -> State -> IO FArrayIndex
    uncacheFAI Cached FArrayIndex
    a State
    st
                      FArrayIndex
    bi <- Cached FArrayIndex -> State -> IO FArrayIndex
    uncacheFAI Cached FArrayIndex
    b State
    st

                      CnstMap
    constMap <- IORef CnstMap -> IO CnstMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef CnstMap
    rconstMap State
    st)
                      let consts :: Map Int CV
    consts = [(Int, CV)] -> Map Int CV
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Int
    i, CV
    cv) | (cv :: CV
    cv, SV _ (NodeId i :: Int
    i)) <- CnstMap -> [(CV, SV)]
    forall k a. Map k a -> [(k, a)]
    Map.toList CnstMap
    constMap]

                      -- Catch the degenerate case of merging an array with itself. One
                      -- can argue this is pointless, but actually it comes up when one
                      -- is merging composite structures (through a Mergeable class instance)
                      -- that has an array component that didn't change. So, pays off in practice!
                      if FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    ai Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    bi
                         then FArrayIndex -> IO FArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return FArrayIndex
    ai  -- merging with itself, noop
                         else do FArrayMap
    fArrMap <- IORef FArrayMap -> IO FArrayMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef FArrayMap
    rFArrayMap State
    st)

                                 case (FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    ai Int -> FArrayMap -> Maybe (SVal -> SVal, IORef (IntMap SV))
    forall a. Int -> IntMap a -> Maybe a
    `IMap.lookup` FArrayMap
    fArrMap, FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    bi Int -> FArrayMap -> Maybe (SVal -> SVal, IORef (IntMap SV))
    forall a. Int -> IntMap a -> Maybe a
    `IMap.lookup` FArrayMap
    fArrMap) of
                                   (Nothing, _) -> String -> IO FArrayIndex
    forall a. HasCallStack => String -> a
    error (String -> IO FArrayIndex) -> String -> IO FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.mergeSFunArr: Impossible happened while trying to access SFunArray, can't find index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FArrayIndex -> String
    forall a. Show a => a -> String
    show FArrayIndex
    ai
                                   (_, Nothing) -> String -> IO FArrayIndex
    forall a. HasCallStack => String -> a
    error (String -> IO FArrayIndex) -> String -> IO FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.mergeSFunArr: Impossible happened while trying to access SFunArray, can't find index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FArrayIndex -> String
    forall a. Show a => a -> String
    show FArrayIndex
    bi
                                   (Just (aUi :: SVal -> SVal
    aUi, raCache :: IORef (IntMap SV)
    raCache), Just (bUi :: SVal -> SVal
    bUi, rbCache :: IORef (IntMap SV)
    rbCache)) -> do

                                       -- This is where the complication happens. We need to merge the caches. If the same
                                       -- key appears in both, then that's the easy case: Just merge the entries. But if
                                       -- a key only appears in one but not the other? Just like in the read/write cases,
                                       -- we have to consider the possibility that the missing key can be any one of the
                                       -- other elements in the cache. So, for each non-matching key in either memo-table,
                                       -- we traverse the other and create a chain of look-up values.
                                       IntMap SV
    aMemo <- IORef (IntMap SV) -> IO (IntMap SV)
    forall a. IORef a -> IO a
    R.readIORef IORef (IntMap SV)
    raCache
                                       IntMap SV
    bMemo <- IORef (IntMap SV) -> IO (IntMap SV)
    forall a. IORef a -> IO a
    R.readIORef IORef (IntMap SV)
    rbCache

                                       let aMemoT :: [(Int, SV)]
    aMemoT = IntMap SV -> [(Int, SV)]
    forall a. IntMap a -> [(Int, a)]
    IMap.toAscList IntMap SV
    aMemo
                                           bMemoT :: [(Int, SV)]
    bMemoT = IntMap SV -> [(Int, SV)]
    forall a. IntMap a -> [(Int, a)]
    IMap.toAscList IntMap SV
    bMemo

                                           -- gen takes a uninitialized-read creator, a key, and the choices from the "other"
                                           -- cache that this key may map to. And creates a new SV that corresponds to the
                                           -- merged value:
                                           gen :: (SVal -> SVal) -> Int -> [(Int, SV)] -> IO SV
                                           gen :: (SVal -> SVal) -> Int -> [(Int, SV)] -> IO SV
    gen mk :: SVal -> SVal
    mk k :: Int
    k choices :: [(Int, SV)]
    choices = State -> SVal -> IO SV
    svToSV State
    st (SVal -> IO SV) -> SVal -> IO SV
    forall a b. (a -> b) -> a -> b
    $ [(Int, SV)] -> SVal
    walk [(Int, SV)]
    choices
                                             where kInfo :: (SVal, Maybe CV)
    kInfo = (Kind -> Int -> SVal
    nodeIdToSVal Kind
    sourceKind Int
    k, Int
    k Int -> Map Int CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map Int CV
    consts)

                                                   walk :: [(Int, SV)] -> SVal
                                                   walk :: [(Int, SV)] -> SVal
    walk []             = SVal -> SVal
    mk ((SVal, Maybe CV) -> SVal
    forall a b. (a, b) -> a
    fst (SVal, Maybe CV)
    kInfo)
                                                   walk ((i :: Int
    i, v :: SV
    v) : ivs :: [(Int, SV)]
    ivs) = SVal -> SVal -> SVal -> SVal
    svIte ((SVal, Maybe CV) -> (SVal, Maybe CV) -> SVal
    svEqualWithConsts (Kind -> Int -> SVal
    nodeIdToSVal Kind
    sourceKind Int
    i, Int
    i Int -> Map Int CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map Int CV
    consts) (SVal, Maybe CV)
    kInfo)
                                                                               (SV -> SVal
    swToSVal SV
    v)
                                                                               ([(Int, SV)] -> SVal
    walk [(Int, SV)]
    ivs)

                                           -- Insert into an existing map the new key value by merging according to the test
                                           fill :: Int -> SV -> SV -> IMap.IntMap SV -> IO (IMap.IntMap SV)
                                           fill :: Int -> SV -> SV -> IntMap SV -> IO (IntMap SV)
    fill k :: Int
    k (SV _ (NodeId ni1 :: Int
    ni1)) (SV _ (NodeId ni2 :: Int
    ni2)) m :: IntMap SV
    m = do SV
    v <- State -> SVal -> IO SV
    svToSV State
    st (SVal -> SVal -> SVal -> SVal
    svIte SVal
    t SVal
    sval1 SVal
    sval2)
                                                                                                 IntMap SV -> IO (IntMap SV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntMap SV -> IO (IntMap SV)) -> IntMap SV -> IO (IntMap SV)
    forall a b. (a -> b) -> a -> b
    $ Int -> SV -> IntMap SV -> IntMap SV
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert Int
    k SV
    v IntMap SV
    m
                                             where sval1 :: SVal
    sval1 = Kind -> Int -> SVal
    nodeIdToSVal Kind
    targetKind Int
    ni1
                                                   sval2 :: SVal
    sval2 = Kind -> Int -> SVal
    nodeIdToSVal Kind
    targetKind Int
    ni2

                                           -- Walk down the memo-tables in tandem. If we find a common key: Simply fill it in. If we find
                                           -- a key only in one, generate the corresponding read from the other cache, and do the fill.
                                           merge :: [(Int, SV)] -> [(Int, SV)] -> IntMap SV -> IO (IntMap SV)
    merge []                  []                  sofar :: IntMap SV
    sofar = IntMap SV -> IO (IntMap SV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return IntMap SV
    sofar
                                           merge ((k1 :: Int
    k1, v1 :: SV
    v1) : as :: [(Int, SV)]
    as)     []                  sofar :: IntMap SV
    sofar = (SVal -> SVal) -> Int -> [(Int, SV)] -> IO SV
    gen SVal -> SVal
    bUi Int
    k1 [(Int, SV)]
    bMemoT IO SV -> (SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \v2 :: SV
    v2  -> Int -> SV -> SV -> IntMap SV -> IO (IntMap SV)
    fill Int
    k1 SV
    v1  SV
    v2 IntMap SV
    sofar  IO (IntMap SV) -> (IntMap SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [(Int, SV)] -> [(Int, SV)] -> IntMap SV -> IO (IntMap SV)
    merge [(Int, SV)]
    as []
                                           merge []                  ((k2 :: Int
    k2, v2 :: SV
    v2) : bs :: [(Int, SV)]
    bs)     sofar :: IntMap SV
    sofar = (SVal -> SVal) -> Int -> [(Int, SV)] -> IO SV
    gen SVal -> SVal
    aUi Int
    k2 [(Int, SV)]
    aMemoT IO SV -> (SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \v1 :: SV
    v1  -> Int -> SV -> SV -> IntMap SV -> IO (IntMap SV)
    fill Int
    k2 SV
    v1  SV
    v2 IntMap SV
    sofar  IO (IntMap SV) -> (IntMap SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [(Int, SV)] -> [(Int, SV)] -> IntMap SV -> IO (IntMap SV)
    merge [] [(Int, SV)]
    bs
                                           merge ass :: [(Int, SV)]
    ass@((k1 :: Int
    k1, v1 :: SV
    v1) : as :: [(Int, SV)]
    as) bss :: [(Int, SV)]
    bss@((k2 :: Int
    k2, v2 :: SV
    v2) : bs :: [(Int, SV)]
    bs) sofar :: IntMap SV
    sofar
                                             | Int
    k1 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    k2                                         = (SVal -> SVal) -> Int -> [(Int, SV)] -> IO SV
    gen SVal -> SVal
    bUi Int
    k1 [(Int, SV)]
    bMemoT IO SV -> (SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \nv2 :: SV
    nv2 -> Int -> SV -> SV -> IntMap SV -> IO (IntMap SV)
    fill Int
    k1 SV
    v1  SV
    nv2 IntMap SV
    sofar IO (IntMap SV) -> (IntMap SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [(Int, SV)] -> [(Int, SV)] -> IntMap SV -> IO (IntMap SV)
    merge [(Int, SV)]
    as  [(Int, SV)]
    bss
                                             | Int
    k1 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    k2                                         = (SVal -> SVal) -> Int -> [(Int, SV)] -> IO SV
    gen SVal -> SVal
    aUi Int
    k2 [(Int, SV)]
    aMemoT IO SV -> (SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \nv1 :: SV
    nv1 -> Int -> SV -> SV -> IntMap SV -> IO (IntMap SV)
    fill Int
    k2 SV
    nv1 SV
    v2  IntMap SV
    sofar IO (IntMap SV) -> (IntMap SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [(Int, SV)] -> [(Int, SV)] -> IntMap SV -> IO (IntMap SV)
    merge [(Int, SV)]
    ass [(Int, SV)]
    bs
                                             | Bool
    True                                            =                               Int -> SV -> SV -> IntMap SV -> IO (IntMap SV)
    fill Int
    k1 SV
    v1  SV
    v2  IntMap SV
    sofar IO (IntMap SV) -> (IntMap SV -> IO (IntMap SV)) -> IO (IntMap SV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [(Int, SV)] -> [(Int, SV)] -> IntMap SV -> IO (IntMap SV)
    merge [(Int, SV)]
    as  [(Int, SV)]
    bs

                                       IntMap SV
    mergedMap  <- [(Int, SV)] -> [(Int, SV)] -> IntMap SV -> IO (IntMap SV)
    merge [(Int, SV)]
    aMemoT [(Int, SV)]
    bMemoT IntMap SV
    forall a. IntMap a
    IMap.empty
                                       IORef (IntMap SV)
    memoMerged <- IntMap SV -> IO (IORef (IntMap SV))
    forall a. a -> IO (IORef a)
    R.newIORef IntMap SV
    mergedMap

                                       -- Craft a new uninitializer. Note that we do *not* create a new initializer here,
                                       -- but simply merge the two initializers which will inherit their original unread
                                       -- references should the test be a constant.
                                       let mkUninitialized :: SVal -> SVal
    mkUninitialized i :: SVal
    i = SVal -> SVal -> SVal -> SVal
    svIte SVal
    t (SVal -> SVal
    aUi SVal
    i) (SVal -> SVal
    bUi SVal
    i)

                                       -- Add it to our collection:
                                       let j :: FArrayIndex
    j   = Int -> FArrayIndex
    FArrayIndex (Int -> FArrayIndex) -> Int -> FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ FArrayMap -> Int
    forall a. IntMap a -> Int
    IMap.size FArrayMap
    fArrMap
                                           upd :: FArrayMap -> FArrayMap
    upd = Int -> (SVal -> SVal, IORef (IntMap SV)) -> FArrayMap -> FArrayMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert (FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    j) (SVal -> SVal
    mkUninitialized, IORef (IntMap SV)
    memoMerged)

                                       FArrayIndex
    j FArrayIndex -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` State
    -> (State -> IORef FArrayMap)
    -> (FArrayMap -> FArrayMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef FArrayMap
    rFArrayMap FArrayMap -> FArrayMap
    upd (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

                                       FArrayIndex -> IO FArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return FArrayIndex
    j

    -- | Create a named new array
    newSFunArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SFunArr
    newSFunArr :: State
    -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SFunArr
    newSFunArr st :: State
    st (ak :: Kind
    ak, bk :: Kind
    bk) mkNm :: Int -> String
    mkNm mbDef :: Maybe SVal
    mbDef = do
            FArrayMap
    fArrMap <- IORef FArrayMap -> IO FArrayMap
    forall a. IORef a -> IO a
    R.readIORef (State -> IORef FArrayMap
    rFArrayMap State
    st)
            IORef (IntMap SV)
    memoTable <- IntMap SV -> IO (IORef (IntMap SV))
    forall a. a -> IO (IORef a)
    R.newIORef IntMap SV
    forall a. IntMap a
    IMap.empty

            let j :: FArrayIndex
    j  = Int -> FArrayIndex
    FArrayIndex (Int -> FArrayIndex) -> Int -> FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ FArrayMap -> Int
    forall a. IntMap a -> Int
    IMap.size FArrayMap
    fArrMap
                nm :: String
    nm = Int -> String
    mkNm (FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    j)
                mkUninitialized :: SVal -> SVal
    mkUninitialized i :: SVal
    i = case Maybe SVal
    mbDef of
                                      Just def :: SVal
    def -> SVal
    def
                                      _        -> Kind -> String -> Maybe [String] -> [SVal] -> SVal
    svUninterpreted Kind
    bk (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "_uninitializedRead") Maybe [String]
    forall a. Maybe a
    Nothing [SVal
    i]

                upd :: FArrayMap -> FArrayMap
    upd = Int -> (SVal -> SVal, IORef (IntMap SV)) -> FArrayMap -> FArrayMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IMap.insert (FArrayIndex -> Int
    unFArrayIndex FArrayIndex
    j) (SVal -> SVal
    mkUninitialized, IORef (IntMap SV)
    memoTable)

            String -> State -> String -> IO ()
    registerLabel "SFunArray declaration" State
    st String
    nm
            FArrayIndex
    j FArrayIndex -> IO () -> IO ()
    forall a b. a -> b -> b
    `seq` State
    -> (State -> IORef FArrayMap)
    -> (FArrayMap -> FArrayMap)
    -> IO ()
    -> IO ()
    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
    modifyState State
    st State -> IORef FArrayMap
    rFArrayMap FArrayMap -> FArrayMap
    upd (() -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

            SFunArr -> IO SFunArr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SFunArr -> IO SFunArr) -> SFunArr -> IO SFunArr
    forall a b. (a -> b) -> a -> b
    $ (Kind, Kind) -> Cached FArrayIndex -> SFunArr
    SFunArr (Kind
    ak, Kind
    bk) (Cached FArrayIndex -> SFunArr) -> Cached FArrayIndex -> SFunArr
    forall a b. (a -> b) -> a -> b
    $ (State -> IO FArrayIndex) -> Cached FArrayIndex
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO FArrayIndex) -> Cached FArrayIndex)
    -> (State -> IO FArrayIndex) -> Cached FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ IO FArrayIndex -> State -> IO FArrayIndex
    forall a b. a -> b -> a
    const (IO FArrayIndex -> State -> IO FArrayIndex)
    -> IO FArrayIndex -> State -> IO FArrayIndex
    forall a b. (a -> b) -> a -> b
    $ FArrayIndex -> IO FArrayIndex
    forall (m :: * -> *) a. Monad m => a -> m a
    return FArrayIndex
    j

    --------------------------------------------------------------------------------
    -- Utility functions

    noUnint  :: (Maybe Int, String) -> a
    noUnint :: (Maybe Int, String) -> a
    noUnint x :: (Maybe Int, String)
    x = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "Unexpected operation called on uninterpreted/enumerated value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Maybe Int, String) -> String
    forall a. Show a => a -> String
    show (Maybe Int, String)
    x

    noUnint2 :: (Maybe Int, String) -> (Maybe Int, String) -> a
    noUnint2 :: (Maybe Int, String) -> (Maybe Int, String) -> a
    noUnint2 x :: (Maybe Int, String)
    x y :: (Maybe Int, String)
    y = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "Unexpected binary operation called on uninterpreted/enumerated values: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ((Maybe Int, String), (Maybe Int, String)) -> String
    forall a. Show a => a -> String
    show ((Maybe Int, String)
    x, (Maybe Int, String)
    y)

    noCharLift :: Char -> a
    noCharLift :: Char -> a
    noCharLift x :: Char
    x = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "Unexpected operation called on char: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Char -> String
    forall a. Show a => a -> String
    show Char
    x

    noStringLift :: String -> a
    noStringLift :: String -> a
    noStringLift x :: String
    x = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "Unexpected operation called on string: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    x

    noCharLift2 :: Char -> Char -> a
    noCharLift2 :: Char -> Char -> a
    noCharLift2 x :: Char
    x y :: Char
    y = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "Unexpected binary operation called on chars: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Char, Char) -> String
    forall a. Show a => a -> String
    show (Char
    x, Char
    y)

    noStringLift2 :: String -> String -> a
    noStringLift2 :: String -> String -> a
    noStringLift2 x :: String
    x y :: String
    y = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "Unexpected binary operation called on strings: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, String) -> String
    forall a. Show a => a -> String
    show (String
    x, String
    y)

    liftSym1 :: (State -> Kind -> SV -> IO SV) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> SVal -> SVal
    liftSym1 :: (State -> Kind -> SV -> IO SV)
    -> (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> SVal
    -> SVal
    liftSym1 _   opCR :: AlgReal -> AlgReal
    opCR opCI :: Integer -> Integer
    opCI opCF :: Float -> Float
    opCF opCD :: Double -> Double
    opCD   (SVal k :: Kind
    k (Left a :: CV
    a)) = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (CV -> Either CV (Cached SV)) -> CV -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left  (CV -> SVal) -> CV -> SVal
    forall a b. (a -> b) -> a -> b
    $! (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> (Char -> Char)
    -> (String -> String)
    -> ((Maybe Int, String) -> (Maybe Int, String))
    -> CV
    -> CV
    mapCV AlgReal -> AlgReal
    opCR Integer -> Integer
    opCI Float -> Float
    opCF Double -> Double
    opCD Char -> Char
    forall a. Char -> a
    noCharLift String -> String
    forall a. String -> a
    noStringLift (Maybe Int, String) -> (Maybe Int, String)
    forall a. (Maybe Int, String) -> a
    noUnint CV
    a
    liftSym1 opS :: State -> Kind -> SV -> IO SV
    opS _    _    _    _    a :: SVal
    a@(SVal k :: Kind
    k _)        = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    c
       where c :: State -> IO SV
    c st :: State
    st = do SV
    sva <- State -> SVal -> IO SV
    svToSV State
    st SVal
    a
                       State -> Kind -> SV -> IO SV
    opS State
    st Kind
    k SV
    sva

    {- A note on constant folding.

    There are cases where we miss out on certain constant foldings. On May 8 2018, Matt Peddie pointed this
    out, as the C code he was getting had redundancies. I was aware that could be missing constant foldings
    due to missed out optimizations, or some other code snafu, but till Matt pointed it out I haven't realized
    that we could be hiding constants inside an if-then-else. The example is:

         proveWith z3{verbose=True} $ \x -> 0 .< ite (x .== (x::SWord8)) 1 (2::SWord8)

    If you try this, you'll see that it generates (shortened):

        (define-fun s1 () (_ BitVec 8) #x00)
        (define-fun s2 () (_ BitVec 8) #x01)
        (define-fun s3 () Bool (bvult s1 s2))

    But clearly we have all the info for s3 to be computed! The issue here is that the reduction of @x .== x@ to @true@
    happens after we start computing the if-then-else, hence we are already committed to an SV at that point. The call
    to ite eventually recognizes this, but at that point it picks up the now constants from SV's, missing the constant
    folding opportunity.

    We can fix this, by looking up the constants table in liftSV2, along the lines of:

        liftSV2 :: (CV -> CV -> Bool) -> (CV -> CV -> CV) -> (State -> Kind -> SV -> SV -> IO SV) -> Kind -> SVal -> SVal -> Cached SV
        liftSV2 okCV opCV opS k a b = cache c
          where c st = do sw1 <- svToSV st a
                          sw2 <- svToSV st b
                          cmap <- readIORef (rconstMap st)
                          let cv1  = [cv | ((_, cv), sv) <- M.toList cmap, sv == sv1]
                              cv2  = [cv | ((_, cv), sv) <- M.toList cmap, sv == sv2]
                          case (cv1, cv2) of
                            ([x], [y]) | okCV x y -> newConst st $ opCV x y
                            _                     -> opS st k sv1 sv2

    (with obvious modifications to call sites to get the proper arguments.)

    But this means that we have to grab the constant list for every symbolicly lifted operation, also do the
    same for other places, etc.; for the rare opportunity of catching a @x .== x@ optimization. Even then, the
    constants for the branches would still be generated. (i.e., in the above example we would still generate
    @s1@ and @s2@, but would skip @s3@.)

    It seems to me that the price to pay is rather high, as this is hardly the most common case; so we're opting
    here to ignore these cases.

    See http://github.com/LeventErkok/sbv/issues/379 for some further discussion.
    -}
    liftSV2 :: (State -> Kind -> SV -> SV -> IO SV) -> Kind -> SVal -> SVal -> Cached SV
    liftSV2 :: (State -> Kind -> SV -> SV -> IO SV)
    -> Kind -> SVal -> SVal -> Cached SV
    liftSV2 opS :: State -> Kind -> SV -> SV -> IO SV
    opS k :: Kind
    k a :: SVal
    a b :: SVal
    b = (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    c
      where c :: State -> IO SV
    c st :: State
    st = do SV
    sw1 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    a
                      SV
    sw2 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    b
                      State -> Kind -> SV -> SV -> IO SV
    opS State
    st Kind
    k SV
    sw1 SV
    sw2

    liftSym2 :: (State -> Kind -> SV -> SV -> IO SV)
             -> (CV      -> CV      -> Bool)
             -> (AlgReal -> AlgReal -> AlgReal)
             -> (Integer -> Integer -> Integer)
             -> (Float   -> Float   -> Float)
             -> (Double  -> Double  -> Double)
             -> SVal     -> SVal    -> SVal
    liftSym2 :: (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> SVal
    -> SVal
    -> SVal
    liftSym2 _   okCV :: CV -> CV -> Bool
    okCV opCR :: AlgReal -> AlgReal -> AlgReal
    opCR opCI :: Integer -> Integer -> Integer
    opCI opCF :: Float -> Float -> Float
    opCF opCD :: Double -> Double -> Double
    opCD   (SVal k :: Kind
    k (Left a :: CV
    a)) (SVal _ (Left b :: CV
    b)) | CV -> CV -> Bool
    okCV CV
    a CV
    b = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (CV -> Either CV (Cached SV)) -> CV -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left  (CV -> SVal) -> CV -> SVal
    forall a b. (a -> b) -> a -> b
    $! (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> (Char -> Char -> Char)
    -> (String -> String -> String)
    -> ((Maybe Int, String)
        -> (Maybe Int, String) -> (Maybe Int, String))
    -> CV
    -> CV
    -> CV
    mapCV2 AlgReal -> AlgReal -> AlgReal
    opCR Integer -> Integer -> Integer
    opCI Float -> Float -> Float
    opCF Double -> Double -> Double
    opCD Char -> Char -> Char
    forall a. Char -> Char -> a
    noCharLift2 String -> String -> String
    forall a. String -> String -> a
    noStringLift2 (Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
    forall a. (Maybe Int, String) -> (Maybe Int, String) -> a
    noUnint2 CV
    a CV
    b
    liftSym2 opS :: State -> Kind -> SV -> SV -> IO SV
    opS _    _    _    _    _    a :: SVal
    a@(SVal k :: Kind
    k _)        b :: SVal
    b                            = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $  (State -> Kind -> SV -> SV -> IO SV)
    -> Kind -> SVal -> SVal -> Cached SV
    liftSV2 State -> Kind -> SV -> SV -> IO SV
    opS Kind
    k SVal
    a SVal
    b

    liftSym2B :: (State -> Kind -> SV -> SV -> IO SV)
              -> (CV                  -> CV                  -> Bool)
              -> (AlgReal             -> AlgReal             -> Bool)
              -> (Integer             -> Integer             -> Bool)
              -> (Float               -> Float               -> Bool)
              -> (Double              -> Double              -> Bool)
              -> (Char                -> Char                -> Bool)
              -> (String              -> String              -> Bool)
              -> ([CVal]              -> [CVal]              -> Bool)
              -> ([CVal]              -> [CVal]              -> Bool)
              -> (Maybe  CVal         -> Maybe  CVal         -> Bool)
              -> (Either CVal CVal    -> Either CVal CVal    -> Bool)
              -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
              -> SVal                 -> SVal                -> SVal
    liftSym2B :: (State -> Kind -> SV -> SV -> IO SV)
    -> (CV -> CV -> Bool)
    -> (AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> SVal
    -> SVal
    -> SVal
    liftSym2B _   okCV :: CV -> CV -> Bool
    okCV opCR :: AlgReal -> AlgReal -> Bool
    opCR opCI :: Integer -> Integer -> Bool
    opCI opCF :: Float -> Float -> Bool
    opCF opCD :: Double -> Double -> Bool
    opCD opCC :: Char -> Char -> Bool
    opCC opCS :: String -> String -> Bool
    opCS opCSeq :: [CVal] -> [CVal] -> Bool
    opCSeq opCTup :: [CVal] -> [CVal] -> Bool
    opCTup opCMaybe :: Maybe CVal -> Maybe CVal -> Bool
    opCMaybe opCEither :: Either CVal CVal -> Either CVal CVal -> Bool
    opCEither opUI :: (Maybe Int, String) -> (Maybe Int, String) -> Bool
    opUI (SVal _ (Left a :: CV
    a)) (SVal _ (Left b :: CV
    b)) | CV -> CV -> Bool
    okCV CV
    a CV
    b = Bool -> SVal
    svBool ((AlgReal -> AlgReal -> Bool)
    -> (Integer -> Integer -> Bool)
    -> (Float -> Float -> Bool)
    -> (Double -> Double -> Bool)
    -> (Char -> Char -> Bool)
    -> (String -> String -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> ([CVal] -> [CVal] -> Bool)
    -> (Maybe CVal -> Maybe CVal -> Bool)
    -> (Either CVal CVal -> Either CVal CVal -> Bool)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool)
    -> CV
    -> CV
    -> Bool
    forall b.
    (AlgReal -> AlgReal -> b)
    -> (Integer -> Integer -> b)
    -> (Float -> Float -> b)
    -> (Double -> Double -> b)
    -> (Char -> Char -> b)
    -> (String -> String -> b)
    -> ([CVal] -> [CVal] -> b)
    -> ([CVal] -> [CVal] -> b)
    -> (Maybe CVal -> Maybe CVal -> b)
    -> (Either CVal CVal -> Either CVal CVal -> b)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> b)
    -> CV
    -> CV
    -> b
    liftCV2 AlgReal -> AlgReal -> Bool
    opCR Integer -> Integer -> Bool
    opCI Float -> Float -> Bool
    opCF Double -> Double -> Bool
    opCD Char -> Char -> Bool
    opCC String -> String -> Bool
    opCS [CVal] -> [CVal] -> Bool
    opCSeq [CVal] -> [CVal] -> Bool
    opCTup Maybe CVal -> Maybe CVal -> Bool
    opCMaybe Either CVal CVal -> Either CVal CVal -> Bool
    opCEither (Maybe Int, String) -> (Maybe Int, String) -> Bool
    opUI CV
    a CV
    b)
    liftSym2B opS :: State -> Kind -> SV -> SV -> IO SV
    opS _    _    _    _    _    _    _    _      _      _        _         _    a :: SVal
    a                 b :: SVal
    b                            = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> Kind -> SV -> SV -> IO SV)
    -> Kind -> SVal -> SVal -> Cached SV
    liftSV2 State -> Kind -> SV -> SV -> IO SV
    opS Kind
    KBool SVal
    a SVal
    b

    -- | Create a symbolic two argument operation; with shortcut optimizations
    mkSymOpSC :: (SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC :: (SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC shortCut :: SV -> SV -> Maybe SV
    shortCut op :: Op
    op st :: State
    st k :: Kind
    k a :: SV
    a b :: SV
    b = IO SV -> (SV -> IO SV) -> Maybe SV -> IO SV
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    op [SV
    a, SV
    b])) SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV -> SV -> Maybe SV
    shortCut SV
    a SV
    b)

    -- | Create a symbolic two argument operation; no shortcut optimizations
    mkSymOp :: Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp :: Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOp = (SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
    mkSymOpSC ((SV -> Maybe SV) -> SV -> SV -> Maybe SV
    forall a b. a -> b -> a
    const (Maybe SV -> SV -> Maybe SV
    forall a b. a -> b -> a
    const Maybe SV
    forall a. Maybe a
    Nothing))

    mkSymOp1SC :: (SV -> Maybe SV) -> Op -> State -> Kind -> SV -> IO SV
    mkSymOp1SC :: (SV -> Maybe SV) -> Op -> State -> Kind -> SV -> IO SV
    mkSymOp1SC shortCut :: SV -> Maybe SV
    shortCut op :: Op
    op st :: State
    st k :: Kind
    k a :: SV
    a = IO SV -> (SV -> IO SV) -> Maybe SV -> IO SV
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp Op
    op [SV
    a])) SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV -> Maybe SV
    shortCut SV
    a)

    mkSymOp1 :: Op -> State -> Kind -> SV -> IO SV
    mkSymOp1 :: Op -> State -> Kind -> SV -> IO SV
    mkSymOp1 = (SV -> Maybe SV) -> Op -> State -> Kind -> SV -> IO SV
    mkSymOp1SC (Maybe SV -> SV -> Maybe SV
    forall a b. a -> b -> a
    const Maybe SV
    forall a. Maybe a
    Nothing)

    -- | eqOpt says the references are to the same SV, thus we can optimize. Note that
    -- we explicitly disallow KFloat/KDouble here. Why? Because it's *NOT* true that
    -- NaN == NaN, NaN >= NaN, and so-forth. So, we have to make sure we don't optimize
    -- floats and doubles, in case the argument turns out to be NaN.
    eqOpt :: SV -> SV -> SV -> Maybe SV
    eqOpt :: SV -> SV -> SV -> Maybe SV
    eqOpt w :: SV
    w x :: SV
    x y :: SV
    y = case SV -> Kind
    swKind SV
    x of
                    KFloat  -> Maybe SV
    forall a. Maybe a
    Nothing
                    KDouble -> Maybe SV
    forall a. Maybe a
    Nothing
                    _       -> if SV
    x SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    y then SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    w else Maybe SV
    forall a. Maybe a
    Nothing

    -- For uninterpreted/enumerated values, we carefully lift through the constructor index for comparisons:
    uiLift :: String -> (Int -> Int -> Bool) -> (Maybe Int, String) -> (Maybe Int, String) -> Bool
    uiLift :: String
    -> (Int -> Int -> Bool)
    -> (Maybe Int, String)
    -> (Maybe Int, String)
    -> Bool
    uiLift _ cmp :: Int -> Int -> Bool
    cmp (Just i :: Int
    i, _) (Just j :: Int
    j, _) = Int
    i Int -> Int -> Bool
    `cmp` Int
    j
    uiLift w :: String
    w _   a :: (Maybe Int, String)
    a           b :: (Maybe Int, String)
    b           = String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.Core.Operations: Impossible happened while trying to lift " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " over " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ((Maybe Int, String), (Maybe Int, String)) -> String
    forall a. Show a => a -> String
    show ((Maybe Int, String)
    a, (Maybe Int, String)
    b)

    -- | Predicate to check if a value is concrete
    isConcrete :: SVal -> Bool
    isConcrete :: SVal -> Bool
    isConcrete (SVal _ Left{}) = Bool
    True
    isConcrete _               = Bool
    False

    -- | Predicate for optimizing word operations like (+) and (*).
    -- NB. We specifically do *not* match for Double/Float; because
    -- FP-arithmetic doesn't obey traditional rules. For instance,
    -- 0 * x = 0 fails if x happens to be NaN or +/- Infinity. So,
    -- we merely return False when given a floating-point value here.
    isConcreteZero :: SVal -> Bool
    isConcreteZero :: SVal -> Bool
    isConcreteZero (SVal _     (Left (CV _     (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
    isConcreteZero (SVal KReal (Left (CV KReal (CAlgReal v :: AlgReal
    v)))) = AlgReal -> Bool
    isExactRational AlgReal
    v Bool -> Bool -> Bool
    && AlgReal
    v AlgReal -> AlgReal -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
    isConcreteZero _                                           = Bool
    False

    -- | Predicate for optimizing word operations like (+) and (*).
    -- NB. See comment on 'isConcreteZero' for why we don't match
    -- for Float/Double values here.
    isConcreteOne :: SVal -> Bool
    isConcreteOne :: SVal -> Bool
    isConcreteOne (SVal _     (Left (CV _     (CInteger 1)))) = Bool
    True
    isConcreteOne (SVal KReal (Left (CV KReal (CAlgReal v :: AlgReal
    v)))) = AlgReal -> Bool
    isExactRational AlgReal
    v Bool -> Bool -> Bool
    && AlgReal
    v AlgReal -> AlgReal -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1
    isConcreteOne _                                           = Bool
    False

    -- | Predicate for optimizing bitwise operations. The unbounded integer case of checking
    -- against -1 might look dubious, but that's how Haskell treats 'Integer' as a member
    -- of the Bits class, try @(-1 :: Integer) `testBit` i@ for any @i@ and you'll get 'True'.
    isConcreteOnes :: SVal -> Bool
    isConcreteOnes :: SVal -> Bool
    isConcreteOnes (SVal _ (Left (CV (KBounded b :: Bool
    b w :: Int
    w) (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == if Bool
    b then -1 else Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1
    isConcreteOnes (SVal _ (Left (CV KUnbounded     (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == -1  -- see comment above
    isConcreteOnes (SVal _ (Left (CV KBool          (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1
    isConcreteOnes _                                                = Bool
    False

    -- | Predicate for optimizing comparisons.
    isConcreteMax :: SVal -> Bool
    isConcreteMax :: SVal -> Bool
    isConcreteMax (SVal _ (Left (CV (KBounded False w :: Int
    w) (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1
    isConcreteMax (SVal _ (Left (CV (KBounded True  w :: Int
    w) (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Integer
    forall a. Bits a => Int -> a
    bit (Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1
    isConcreteMax (SVal _ (Left (CV KBool              (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1
    isConcreteMax _                                                    = Bool
    False

    -- | Predicate for optimizing comparisons.
    isConcreteMin :: SVal -> Bool
    isConcreteMin :: SVal -> Bool
    isConcreteMin (SVal _ (Left (CV (KBounded False _) (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
    isConcreteMin (SVal _ (Left (CV (KBounded True  w :: Int
    w) (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == - Int -> Integer
    forall a. Bits a => Int -> a
    bit (Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)
    isConcreteMin (SVal _ (Left (CV KBool              (CInteger n :: Integer
    n)))) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
    isConcreteMin _                                                    = Bool
    False

    -- | Most operations on concrete rationals require a compatibility check to avoid faulting
    -- on algebraic reals.
    rationalCheck :: CV -> CV -> Bool
    rationalCheck :: CV -> CV -> Bool
    rationalCheck a :: CV
    a b :: CV
    b = case (CV -> CVal
    cvVal CV
    a, CV -> CVal
    cvVal CV
    b) of
                         (CAlgReal x :: AlgReal
    x, CAlgReal y :: AlgReal
    y) -> AlgReal -> Bool
    isExactRational AlgReal
    x Bool -> Bool -> Bool
    && AlgReal -> Bool
    isExactRational AlgReal
    y
                         _                        -> Bool
    True

    -- | Quot/Rem operations require a nonzero check on the divisor.
    --
    nonzeroCheck :: CV -> CV -> Bool
    nonzeroCheck :: CV -> CV -> Bool
    nonzeroCheck _ b :: CV
    b = CV -> CVal
    cvVal CV
    b CVal -> CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer -> CVal
    CInteger 0

    -- | Same as rationalCheck, except for SBV's
    rationalSBVCheck :: SVal -> SVal -> Bool
    rationalSBVCheck :: SVal -> SVal -> Bool
    rationalSBVCheck (SVal KReal (Left a :: CV
    a)) (SVal KReal (Left b :: CV
    b)) = CV -> CV -> Bool
    rationalCheck CV
    a CV
    b
    rationalSBVCheck _                     _                     = Bool
    True

    noReal :: String -> AlgReal -> AlgReal -> AlgReal
    noReal :: String -> AlgReal -> AlgReal -> AlgReal
    noReal o :: String
    o a :: AlgReal
    a b :: AlgReal
    b = String -> AlgReal
    forall a. HasCallStack => String -> a
    error (String -> AlgReal) -> String -> AlgReal
    forall a b. (a -> b) -> a -> b
    $ "SBV.AlgReal." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": Unexpected arguments: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (AlgReal, AlgReal) -> String
    forall a. Show a => a -> String
    show (AlgReal
    a, AlgReal
    b)

    noFloat :: String -> Float -> Float -> Float
    noFloat :: String -> Float -> Float -> Float
    noFloat o :: String
    o a :: Float
    a b :: Float
    b = String -> Float
    forall a. HasCallStack => String -> a
    error (String -> Float) -> String -> Float
    forall a b. (a -> b) -> a -> b
    $ "SBV.Float." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": Unexpected arguments: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Float, Float) -> String
    forall a. Show a => a -> String
    show (Float
    a, Float
    b)

    noDouble :: String -> Double -> Double -> Double
    noDouble :: String -> Double -> Double -> Double
    noDouble o :: String
    o a :: Double
    a b :: Double
    b = String -> Double
    forall a. HasCallStack => String -> a
    error (String -> Double) -> String -> Double
    forall a b. (a -> b) -> a -> b
    $ "SBV.Double." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": Unexpected arguments: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Double, Double) -> String
    forall a. Show a => a -> String
    show (Double
    a, Double
    b)

    noRealUnary :: String -> AlgReal -> AlgReal
    noRealUnary :: String -> AlgReal -> AlgReal
    noRealUnary o :: String
    o a :: AlgReal
    a = String -> AlgReal
    forall a. HasCallStack => String -> a
    error (String -> AlgReal) -> String -> AlgReal
    forall a b. (a -> b) -> a -> b
    $ "SBV.AlgReal." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": Unexpected argument: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ AlgReal -> String
    forall a. Show a => a -> String
    show AlgReal
    a

    noFloatUnary :: String -> Float -> Float
    noFloatUnary :: String -> Float -> Float
    noFloatUnary o :: String
    o a :: Float
    a = String -> Float
    forall a. HasCallStack => String -> a
    error (String -> Float) -> String -> Float
    forall a b. (a -> b) -> a -> b
    $ "SBV.Float." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": Unexpected argument: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Float -> String
    forall a. Show a => a -> String
    show Float
    a

    noDoubleUnary :: String -> Double -> Double
    noDoubleUnary :: String -> Double -> Double
    noDoubleUnary o :: String
    o a :: Double
    a = String -> Double
    forall a. HasCallStack => String -> a
    error (String -> Double) -> String -> Double
    forall a b. (a -> b) -> a -> b
    $ "SBV.Double." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": Unexpected argument: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Double -> String
    forall a. Show a => a -> String
    show Double
    a

    -- | Given a composite structure, figure out how to compare for less than
    svStructuralLessThan :: SVal -> SVal -> SVal
    svStructuralLessThan :: SVal -> SVal -> SVal
    svStructuralLessThan x :: SVal
    x y :: SVal
    y
       | SVal -> Bool
    isConcrete SVal
    x Bool -> Bool -> Bool
    && SVal -> Bool
    isConcrete SVal
    y
       = SVal
    x SVal -> SVal -> SVal
    `svLessThan` SVal
    y
       | KTuple{} <- Kind
    kx
       = SVal -> SVal -> SVal
    tupleLT SVal
    x SVal
    y
       | KMaybe{}  <- Kind
    kx
       = SVal -> SVal -> SVal
    maybeLT SVal
    x SVal
    y
       | KEither{} <- Kind
    kx
       = SVal -> SVal -> SVal
    eitherLT SVal
    x SVal
    y
       | Bool
    True
       = SVal
    x SVal -> SVal -> SVal
    `svLessThan` SVal
    y
       where kx :: Kind
    kx = SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x

    -- | Structural less-than for tuples
    tupleLT :: SVal -> SVal -> SVal
    tupleLT :: SVal -> SVal -> SVal
    tupleLT x :: SVal
    x y :: SVal
    y = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
      where ks :: [Kind]
    ks = case SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x of
                   KTuple xs :: [Kind]
    xs -> [Kind]
    xs
                   k :: Kind
    k         -> String -> [Kind]
    forall a. HasCallStack => String -> a
    error (String -> [Kind]) -> String -> [Kind]
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: Impossible happened, tupleLT called with: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, SVal, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, SVal
    x, SVal
    y)

            n :: Int
    n = [Kind] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    ks

            res :: State -> IO SV
    res st :: State
    st = do SV
    sx <- State -> SVal -> IO SV
    svToSV State
    st SVal
    x
                        SV
    sy <- State -> SVal -> IO SV
    svToSV State
    st SVal
    y

                        let chkElt :: Int -> Kind -> (SVal, SVal)
    chkElt i :: Int
    i ek :: Kind
    ek = let xi :: SVal
    xi = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    ek (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
    forall a b. (a -> b) -> a -> b
    $ \_ -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    ek (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Int -> Int -> Op
    TupleAccess Int
    i Int
    n) [SV
    sx]
                                              yi :: SVal
    yi = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    ek (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
    forall a b. (a -> b) -> a -> b
    $ \_ -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    ek (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Int -> Int -> Op
    TupleAccess Int
    i Int
    n) [SV
    sy]
                                              lt :: SVal
    lt = SVal
    xi SVal -> SVal -> SVal
    `svStructuralLessThan` SVal
    yi
                                              eq :: SVal
    eq = SVal
    xi SVal -> SVal -> SVal
    `svEqual`              SVal
    yi
                                           in (SVal
    lt, SVal
    eq)

                            walk :: [(SVal, SVal)] -> SVal
    walk []                  = SVal
    svFalse
                            walk [(lti :: SVal
    lti, _)]          = SVal
    lti
                            walk ((lti :: SVal
    lti, eqi :: SVal
    eqi) : rest :: [(SVal, SVal)]
    rest) = SVal
    lti SVal -> SVal -> SVal
    `svOr` (SVal
    eqi SVal -> SVal -> SVal
    `svAnd` [(SVal, SVal)] -> SVal
    walk [(SVal, SVal)]
    rest)

                        State -> SVal -> IO SV
    svToSV State
    st (SVal -> IO SV) -> SVal -> IO SV
    forall a b. (a -> b) -> a -> b
    $ [(SVal, SVal)] -> SVal
    walk ([(SVal, SVal)] -> SVal) -> [(SVal, SVal)] -> SVal
    forall a b. (a -> b) -> a -> b
    $ (Int -> Kind -> (SVal, SVal)) -> [Int] -> [Kind] -> [(SVal, SVal)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> Kind -> (SVal, SVal)
    chkElt [1..] [Kind]
    ks

    -- | Structural less-than for maybes
    maybeLT :: SVal -> SVal -> SVal
    maybeLT :: SVal -> SVal -> SVal
    maybeLT x :: SVal
    x y :: SVal
    y = SVal -> (SVal -> SVal) -> SVal -> SVal
    sMaybeCase (       SVal -> (SVal -> SVal) -> SVal -> SVal
    sMaybeCase SVal
    svFalse (SVal -> SVal -> SVal
    forall a b. a -> b -> a
    const SVal
    svTrue)    SVal
    y)
                             (\jx :: SVal
    jx -> SVal -> (SVal -> SVal) -> SVal -> SVal
    sMaybeCase SVal
    svFalse (SVal
    jx SVal -> SVal -> SVal
    `svStructuralLessThan`) SVal
    y)
                             SVal
    x
      where ka :: Kind
    ka = case SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x of
                   KMaybe k' :: Kind
    k' -> Kind
    k'
                   k :: Kind
    k         -> String -> Kind
    forall a. HasCallStack => String -> a
    error (String -> Kind) -> String -> Kind
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: Impossible happened, maybeLT called with: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, SVal, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, SVal
    x, SVal
    y)

            sMaybeCase :: SVal -> (SVal -> SVal) -> SVal -> SVal
    sMaybeCase brNothing :: SVal
    brNothing brJust :: SVal -> SVal
    brJust s :: SVal
    s = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
               where res :: State -> IO SV
    res st :: State
    st = do SV
    sv <- State -> SVal -> IO SV
    svToSV State
    st SVal
    s

                                 let justVal :: SVal
    justVal = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    ka (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
    forall a b. (a -> b) -> a -> b
    $ \_ -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    ka (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp Op
    MaybeAccess [SV
    sv]
                                     justRes :: SVal
    justRes = SVal -> SVal
    brJust SVal
    justVal

                                 SV
    br1 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    brNothing
                                 SV
    br2 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    justRes

                                 -- Do we have a value?
                                 SV
    noVal <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Kind -> Bool -> Op
    MaybeIs Kind
    ka Bool
    False) [SV
    sv]
                                 State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp Op
    Ite [SV
    noVal, SV
    br1, SV
    br2]

    -- | Structural less-than for either
    eitherLT :: SVal -> SVal -> SVal
    eitherLT :: SVal -> SVal -> SVal
    eitherLT x :: SVal
    x y :: SVal
    y = (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
    sEitherCase (\lx :: SVal
    lx -> (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
    sEitherCase (SVal
    lx SVal -> SVal -> SVal
    `svStructuralLessThan`) (SVal -> SVal -> SVal
    forall a b. a -> b -> a
    const SVal
    svTrue)              SVal
    y)
                               (\rx :: SVal
    rx -> (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
    sEitherCase (SVal -> SVal -> SVal
    forall a b. a -> b -> a
    const SVal
    svFalse)             (SVal
    rx SVal -> SVal -> SVal
    `svStructuralLessThan`) SVal
    y)
                               SVal
    x
      where (ka :: Kind
    ka, kb :: Kind
    kb) = case SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    x of
                         KEither k1 :: Kind
    k1 k2 :: Kind
    k2 -> (Kind
    k1, Kind
    k2)
                         k :: Kind
    k             -> String -> (Kind, Kind)
    forall a. HasCallStack => String -> a
    error (String -> (Kind, Kind)) -> String -> (Kind, Kind)
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: Impossible happened, eitherLT called with: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, SVal, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, SVal
    x, SVal
    y)

            sEitherCase :: (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
    sEitherCase brA :: SVal -> SVal
    brA brB :: SVal -> SVal
    brB sab :: SVal
    sab = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
              where res :: State -> IO SV
    res st :: State
    st = do SV
    abv <- State -> SVal -> IO SV
    svToSV State
    st SVal
    sab

                                let leftVal :: SVal
    leftVal  = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    ka (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
    forall a b. (a -> b) -> a -> b
    $ \_ -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    ka (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Bool -> Op
    EitherAccess Bool
    False) [SV
    abv]
                                    rightVal :: SVal
    rightVal = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kb (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
    forall a b. (a -> b) -> a -> b
    $ \_ -> State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kb (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Bool -> Op
    EitherAccess Bool
    True)  [SV
    abv]

                                    leftRes :: SVal
    leftRes  = SVal -> SVal
    brA SVal
    leftVal
                                    rightRes :: SVal
    rightRes = SVal -> SVal
    brB SVal
    rightVal

                                SV
    br1 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    leftRes
                                SV
    br2 <- State -> SVal -> IO SV
    svToSV State
    st SVal
    rightRes

                                --  Which branch are we in? Return the appropriate value:
                                SV
    onLeft <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp (Kind -> Kind -> Bool -> Op
    EitherIs Kind
    ka Kind
    kb Bool
    False) [SV
    abv]
                                State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (SBVExpr -> IO SV) -> SBVExpr -> IO SV
    forall a b. (a -> b) -> a -> b
    $ Op -> [SV] -> SBVExpr
    SBVApp Op
    Ite [SV
    onLeft, SV
    br1, SV
    br2]

    {-# ANN svIte     ("HLint: ignore Eta reduce" :: String)         #-}
    {-# ANN svLazyIte ("HLint: ignore Eta reduce" :: String)         #-}
    {-# ANN module    ("HLint: ignore Reduce duplication" :: String) #-}