-----------------------------------------------------------------------------
-- |
-- 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, delete)

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 Bool
b = if Bool
b then SVal
svTrue else SVal
svFalse

-- | Convert from an Integer.
svInteger :: Kind -> Integer -> SVal
svInteger :: Kind -> Integer -> SVal
svInteger Kind
k 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 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 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 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 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 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 Kind
_ (Left CV
cv)) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (CV -> Bool
cvToBool CV
cv)
svAsBool SVal
_                  = Maybe Bool
forall a. Maybe a
Nothing

-- | Extract an integer from a concrete value.
svAsInteger :: SVal -> Maybe Integer
svAsInteger :: SVal -> Maybe Integer
svAsInteger (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
n)))) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
svAsInteger SVal
_                                   = 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 Kind
KReal (Left (CV Kind
KReal (CAlgReal (AlgRational Bool
True 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 SVal
_                                                              = 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 Kind
KReal (Left (CV Kind
KReal (CAlgReal (AlgRational Bool
True 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 SVal
_                                                              = 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 SVal
bf Maybe SVal
mbs SVal
bt
  | Just SVal
bs <- Maybe SVal
mbs, Just Integer
f <- SVal -> Maybe Integer
svAsInteger SVal
bf, Just Integer
s <- SVal -> Maybe Integer
svAsInteger SVal
bs, Just 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 Integer
f <- SVal -> Maybe Integer
svAsInteger SVal
bf,                           Just 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 SVal
x 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 SVal
x 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 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
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 a
x a
0 = a
x
         idiv a
x 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 SVal
b SVal
e
  | Just Integer
x <- SVal -> Maybe Integer
svAsInteger SVal
e
  = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then let go :: a -> SVal -> SVal
go a
n SVal
v
                        | a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
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` a
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` a
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
$ String
"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
$ String
"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 (\SVal
use 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 (\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) Integer
1

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

-- | Set a given bit at index
svSetBit :: SVal -> Int -> SVal
svSetBit :: SVal -> Int -> SVal
svSetBit SVal
x 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 [SVal]
bs = SVal -> Int -> [SVal] -> SVal
go SVal
zero Int
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)) Integer
0
        go :: SVal -> Int -> [SVal] -> SVal
go !SVal
acc Int
_  []     = SVal
acc
        go !SVal
acc !Int
i (SVal
x:[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
+Int
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 SVal
x 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 SVal
x = SVal -> Integer -> SVal
forall a. Integral a => SVal -> a -> SVal
svAddConstant SVal
x (Integer
1::Integer)

-- | Decrement:
svDecrement :: SVal -> SVal
svDecrement :: SVal -> SVal
svDecrement SVal
x = SVal -> Integer -> SVal
forall a. Integral a => SVal -> a -> SVal
svAddConstant SVal
x (-Integer
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 SVal
x 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) Integer
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 String
"quot") Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
quot' (String -> Float -> Float -> Float
noFloat String
"quot") (String -> Double -> Double -> Double
noDouble String
"quot") SVal
x SVal
y
  where
    quot' :: a -> a -> a
quot' a
a 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 SVal
x 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) Integer
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 String
"rem") Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
rem' (String -> Float -> Float -> Float
noFloat String
"rem") (String -> Double -> Double -> Double
noDouble String
"rem") SVal
x SVal
y
  where
    rem' :: a -> a -> a
rem' a
a 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 SVal
x 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 SV
w SV
x 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 SVal
a 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 SVal
a 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 SVal
sa 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
$ String
"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 Set CVal
a)    <- SVal -> Maybe (RCSet CVal)
getSet SVal
sa, Just (RegularSet 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 Set CVal
a) <- SVal -> Maybe (RCSet CVal)
getSet SVal
sa, Just (ComplementSet 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 Kind
_ (Left (CV Kind
_ (CSet RCSet CVal
s)))) = RCSet CVal -> Maybe (RCSet CVal)
forall a. a -> Maybe a
Just RCSet CVal
s
        getSet SVal
_                               = Maybe (RCSet CVal)
forall a. Maybe a
Nothing

        r :: State -> IO SV
r 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 SVal
x SVal
y
  | SVal -> Bool
forall a. HasKind a => a -> Bool
isFloat SVal
x, Just Float
f1 <- SVal -> Maybe Float
getF SVal
x, Just 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 Double
f1 <- SVal -> Maybe Double
getD SVal
x, Just 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 Kind
_ (Left (CV Kind
_ (CFloat Float
f)))) = Float -> Maybe Float
forall a. a -> Maybe a
Just Float
f
        getF SVal
_                                 = Maybe Float
forall a. Maybe a
Nothing

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

        r :: State -> IO SV
r 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 SVal
x 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 String
"<" 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 SVal
x 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 String
">"  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 SVal
x 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 String
"<=" 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 SVal
x 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 String
">=" 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 SVal
x 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 String
".&.") Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.&.) (String -> Float -> Float -> Float
noFloat String
".&.") (String -> Double -> Double -> Double
noDouble String
".&.") SVal
x SVal
y
  where opt :: SV -> SV -> Maybe SV
opt SV
a 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 SVal
x 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 String
".|.") Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.|.) (String -> Float -> Float -> Float
noFloat String
".|.") (String -> Double -> Double -> Double
noDouble String
".|.") SVal
x SVal
y
  where opt :: SV -> SV -> Maybe SV
opt SV
a 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 SVal
x 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 String
"xor") Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
xor (String -> Float -> Float -> Float
noFloat String
"xor") (String -> Double -> Double -> Double
noDouble String
"xor") SVal
x SVal
y
  where opt :: SV -> SV -> Maybe SV
opt SV
a 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 String
"complement") Integer -> Integer
forall a. Bits a => a -> a
complement
                 (String -> Float -> Float
noFloatUnary String
"complement") (String -> Double -> Double
noDoubleUnary String
"complement")
  where opt :: SV -> Maybe SV
opt 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 SVal
x Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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 Integer
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 SVal
x Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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 Integer
0
        neg1 :: SVal
neg1 = Kind -> Integer -> SVal
svInteger Kind
k (-Integer
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 SVal
x Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
  = SVal
x
  | Bool
True
  = case SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
x of
           KBounded Bool
_ 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 String
"rotateL") (Bool -> Int -> Int -> Integer -> Integer
rot Bool
True Int
sz Int
i)
                                     (String -> Float -> Float
noFloatUnary String
"rotateL") (String -> Double -> Double
noDoubleUnary String
"rotateL") SVal
x
           Kind
_ -> 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 SVal
x Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
  = SVal
x
  | Bool
True
  = case SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
x of
      KBounded Bool
_ 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 String
"rotateR") (Bool -> Int -> Int -> Integer -> Integer
rot Bool
False Int
sz Int
i)
                                (String -> Float -> Float
noFloatUnary String
"rotateR") (String -> Double -> Double
noDoubleUnary String
"rotateR") SVal
x
      Kind
_ -> 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 Bool
toLeft Int
sz Int
amt Integer
x
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
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 (Int
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 a
v Int
s = a
v a -> a -> a
forall a. Bits a => 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
- a
1)

-- | Extract bit-sequences.
svExtract :: Int -> Int -> SVal -> SVal
svExtract :: Int -> Int -> SVal -> SVal
svExtract Int
i Int
j x :: SVal
x@(SVal (KBounded Bool
s Int
_) Either CV (Cached SV)
_)
  | 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 Integer
0))
  | SVal Kind
_ (Left (CV Kind
_ (CInteger 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
+ Int
1)
        y :: State -> IO SV
y 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 Int
_ Int
_ SVal
_ = String -> SVal
forall a. HasCallStack => String -> a
error String
"extract: non-bitvector type"

-- | Join two words, by concatenating
svJoin :: SVal -> SVal -> SVal
svJoin :: SVal -> SVal -> SVal
svJoin x :: SVal
x@(SVal (KBounded Bool
s Int
i) Either CV (Cached SV)
a) y :: SVal
y@(SVal (KBounded Bool
_ Int
j) Either CV (Cached SV)
b)
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = SVal
y
  | Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = SVal
x
  | Left (CV Kind
_ (CInteger Integer
m)) <- Either CV (Cached SV)
a, Left (CV Kind
_ (CInteger 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 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 SVal
_ SVal
_ = String -> SVal
forall a. HasCallStack => String -> a
error String
"svJoin: non-bitvector type"

-- | If-then-else. This one will force branches.
svIte :: SVal -> SVal -> SVal -> SVal
svIte :: SVal -> SVal -> SVal -> SVal
svIte SVal
t SVal
a 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 Kind
k SVal
t SVal
a 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 Kind
k Bool
force SVal
t SVal
a SVal
b
  | Just 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 Kind
_ (Left CV
c1)) (SVal Kind
_ (Left CV
c2)) = CV
c1 CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
c2
        sameResult SVal
_                  SVal
_                  = Bool
False

        c :: State -> IO SV
c 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 aggressive 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 altogether.
                             -}
                             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 [SVal]
xs SVal
err SVal
ind
  | SVal Kind
_ (Left CV
c) <- SVal
ind =
    case CV -> CVal
cvVal CV
c of
      CInteger Integer
i -> if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
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
      CVal
_          -> String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" valued select/index expression"
svSelect [SVal]
xsOrig SVal
err SVal
ind = [SVal]
xs [SVal] -> SVal -> SVal
`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 Bool
False Int
i -> Integer -> [SVal] -> [SVal]
forall i a. Integral i => i -> [a] -> [a]
genericTake ((Integer
2::Integer) Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
i) [SVal]
xsOrig
           KBounded Bool
True  Int
i -> Integer -> [SVal] -> [SVal]
forall i a. Integral i => i -> [a] -> [a]
genericTake ((Integer
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
-Int
1)) [SVal]
xsOrig
           Kind
KUnbounded       -> [SVal]
xsOrig
           Kind
_                -> String -> [SVal]
forall a. HasCallStack => String -> a
error (String -> [SVal]) -> String -> [SVal]
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" valued select/index expression"
    r :: State -> IO SV
r 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 Bool
s 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
$ String
"Data.SBV." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 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 String
"svSign" else String
"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 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
- Int
1) Int
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 Kind
kTo SVal
x
  | Just 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 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 SVal
b = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge Kind
k Bool
True SVal
b (Kind -> Integer -> SVal
svInteger Kind
k Integer
1) (Kind -> Integer -> SVal
svInteger Kind
k Integer
0)
  where k :: Kind
k = Bool -> Int -> Kind
KBounded Bool
False Int
1

-- | Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool.
svFromWord1 :: SVal -> SVal
svFromWord1 :: SVal -> SVal
svFromWord1 SVal
x = SVal -> SVal -> SVal
svNotEqual SVal
x (Kind -> Integer -> SVal
svInteger Kind
k Integer
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 SVal
x 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 Bool
toLeft SVal
x SVal
i
  | Just 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 Integer
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 Integer
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 = String
"shiftLeft"
           | Bool
True   = String
"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 Integer
iv <- SVal -> Maybe Integer
getConst SVal
i, Integer
iv Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
          = SVal -> Maybe SVal
forall a. a -> Maybe a
Just SVal
x

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

          | Just Integer
xv <- SVal -> Maybe Integer
getConst SVal
x, Just 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
$ String
"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]
++ String
", 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
$ String
"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 String
m = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m

                getConst :: SVal -> Maybe Integer
getConst (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
val)))) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
val
                getConst SVal
_                                     = 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 Integer
iv
                  | Integer
iv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0                                            = Int
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
$ String
"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
$ String
"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
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
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
- Integer
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 Integer
0
                neg1 :: SVal
neg1 = Kind -> Integer -> SVal
svInteger Kind
kx (-Integer
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 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 SVal
x 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 <- [Int
0 .. Int -> Int
forall a. Bits a => Int -> a
bit Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]] SVal
z (SVal -> SVal
svUNeg SVal
i))
          ([SVal] -> SVal -> SVal -> SVal
svSelect [SVal
x SVal -> Int -> SVal
`svRol` Int
k | Int
k <- [Int
0 .. Int -> Int
forall a. Bits a => Int -> a
bit Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 <- [Int
0 .. Int
sx     Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 <- [Int
0 .. Int
sx     Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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) Integer
0
          zi :: SVal
zi = Kind -> Integer -> SVal
svInteger (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
i) Integer
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 SVal
x 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
$ String
"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 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 SVal
x 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
$ String
"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 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 SVal -> Int -> SVal
f SVal
a SVal
c = [(SVal, Integer)] -> SVal -> SVal
loop [(SVal, Integer)]
blasted SVal
a
  where loop :: [(SVal, Integer)] -> SVal -> SVal
        loop :: [(SVal, Integer)] -> SVal -> SVal
loop []              SVal
acc = SVal
acc
        loop ((SVal
b, Integer
v) : [(SVal, Integer)]
rest) 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) [Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
i | Integer
i <- [(Integer
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 (a
_, 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 SVal
x 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 <- [Int
0 .. Int -> Int
forall a. Bits a => Int -> a
bit Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]] SVal
z (SVal -> SVal
svUNeg SVal
i))
          ([SVal] -> SVal -> SVal -> SVal
svSelect [SVal
x SVal -> Int -> SVal
`svRor` Int
k | Int
k <- [Int
0 .. Int -> Int
forall a. Bits a => Int -> a
bit Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 <- [Int
0 .. Int
sx     Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 <- [Int
0 .. Int
sx     Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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) Integer
0
          zi :: SVal
zi = Kind -> Integer -> SVal
svInteger (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
i) Integer
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 OvOp
o SVal
x 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 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 (Kind
_, Kind
bk) Cached ArrayIndex
f) 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 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 (Kind, Kind)
ainfo Cached ArrayIndex
f) SVal
a 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 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) (String
"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 ()
`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 SVal
t (SArr (Kind, Kind)
ainfo Cached ArrayIndex
a) (SArr (Kind, Kind)
_ 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 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) (String
"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 ()
`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 State
st (Kind, Kind)
ainfo Int -> String
mkNm 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
                 Maybe SVal
Nothing -> Maybe SV -> IO (Maybe SV)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SV
forall a. Maybe a
Nothing
                 Just 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 String
"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 (Kind, Kind)
_ Cached ArrayIndex
a) (SArr (Kind, Kind)
_ 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 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 Kind
k 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 Kind
k NodeId
_) = 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 paranoid 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 (SVal, Maybe CV)
sv1 (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, Just 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
                               (Maybe CV, Maybe CV)
_                                          -> (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 (SVal
_,                Just CV
cv) = CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv
        grabCV (SVal Kind
_ (Left CV
cv), Maybe CV
_      ) = CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv
        grabCV (SVal, Maybe CV)
_                           = 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 (Kind
ak, Kind
bk) Cached FArrayIndex
f) 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
$ String
"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]
++ String
", 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 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, SV Kind
_ (NodeId 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
                    Maybe (SVal -> SVal, IORef (IntMap SV))
Nothing -> String -> IO SV
forall a. HasCallStack => String -> a
error (String -> IO SV) -> String -> IO SV
forall a b. (a -> b) -> a -> b
$ String
"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 (SVal -> SVal
uninitializedRead, 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 Kind
_ (NodeId 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 SV
v  -> SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
v  -- cache hit!

                          Maybe SV
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 ((Int
i, SV
v) : [(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 (Kind
ak, Kind
bk) Cached FArrayIndex
f) SVal
address 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
$ String
"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]
++ String
", 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
$ String
"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]
++ String
", 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 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, SV Kind
_ (NodeId 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
                    Maybe (SVal -> SVal, IORef (IntMap SV))
Nothing          -> String -> IO FArrayIndex
forall a. HasCallStack => String -> a
error (String -> IO FArrayIndex) -> String -> IO FArrayIndex
forall a b. (a -> b) -> a -> b
$ String
"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 (SVal -> SVal
aUi, 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 Kind
_ (NodeId Int
addressNodeId) <- State -> SVal -> IO SV
svToSV State
st SVal
address
                       SV
val                         <- State -> SVal -> IO SV
svToSV State
st SVal
b

                       -- There are two 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 OR we miss the cache. We need to insert this value into
                       --        the cache, overriding the original if it was there. Note that we also have to walk the cache
                       --        to update each element, as this write can symbolically be the same as some other addresses.
                       --
                       -- 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 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

                                 Maybe SV
_                 -> do        -- Cache miss, or value is different.

                                        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 []           [(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 ((Int
i, SV
s):[(Int, SV)]
iss) [(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
>>= \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 Int
i 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 (Int -> IntMap SV -> IntMap SV
forall a. Int -> IntMap a -> IntMap a
IMap.delete Int
addressNodeId IntMap SV
memoTable)) []

                       case Either FArrayIndex (IntMap SV)
cont of
                         Left 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 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 ()
`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 SVal
t array1 :: SFunArr
array1@(SFunArr ainfo :: (Kind, Kind)
ainfo@(Kind
sourceKind, Kind
targetKind) Cached FArrayIndex
a) array2 :: SFunArr
array2@(SFunArr (Kind, Kind)
binfo 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
$ String
"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 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 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, SV Kind
_ (NodeId 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
                               (Maybe (SVal -> SVal, IORef (IntMap SV))
Nothing, Maybe (SVal -> SVal, IORef (IntMap SV))
_) -> String -> IO FArrayIndex
forall a. HasCallStack => String -> a
error (String -> IO FArrayIndex) -> String -> IO FArrayIndex
forall a b. (a -> b) -> a -> b
$ String
"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
                               (Maybe (SVal -> SVal, IORef (IntMap SV))
_, Maybe (SVal -> SVal, IORef (IntMap SV))
Nothing) -> String -> IO FArrayIndex
forall a. HasCallStack => String -> a
error (String -> IO FArrayIndex) -> String -> IO FArrayIndex
forall a b. (a -> b) -> a -> b
$ String
"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 (SVal -> SVal
aUi, IORef (IntMap SV)
raCache), Just (SVal -> SVal
bUi, 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 SVal -> SVal
mk Int
k [(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 ((Int
i, SV
v) : [(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 Int
k (SV Kind
_ (NodeId Int
ni1)) (SV Kind
_ (NodeId Int
ni2)) 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 []                  []                  IntMap SV
sofar = IntMap SV -> IO (IntMap SV)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap SV
sofar
                                       merge ((Int
k1, SV
v1) : [(Int, SV)]
as)     []                  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
>>= \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 []                  ((Int
k2, SV
v2) : [(Int, SV)]
bs)     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
>>= \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@((Int
k1, SV
v1) : [(Int, SV)]
as) bss :: [(Int, SV)]
bss@((Int
k2, SV
v2) : [(Int, SV)]
bs) 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
>>= \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
>>= \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 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 ()
`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 State
st (Kind
ak, Kind
bk) Int -> String
mkNm 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 SVal
i = case Maybe SVal
mbDef of
                                  Just SVal
def -> SVal
def
                                  Maybe SVal
_        -> Kind -> String -> Maybe [String] -> [SVal] -> SVal
svUninterpreted Kind
bk (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_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 String
"SFunArray declaration" State
st String
nm
        FArrayIndex
j FArrayIndex -> IO () -> IO ()
`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 (Maybe Int, String)
x = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"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 (Maybe Int, String)
x (Maybe Int, String)
y = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"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 Char
x = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"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 String
x = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"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 Char
x Char
y = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"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 String
x String
y = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"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 State -> Kind -> SV -> IO SV
_   AlgReal -> AlgReal
opCR Integer -> Integer
opCI Float -> Float
opCF Double -> Double
opCD   (SVal Kind
k (Left 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 State -> Kind -> SV -> IO SV
opS AlgReal -> AlgReal
_    Integer -> Integer
_    Float -> Float
_    Double -> Double
_    a :: SVal
a@(SVal Kind
k Either CV (Cached SV)
_)        = 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 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 symbolically 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 State -> Kind -> SV -> SV -> IO SV
opS Kind
k SVal
a 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 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 State -> Kind -> SV -> SV -> IO SV
_   CV -> CV -> Bool
okCV AlgReal -> AlgReal -> AlgReal
opCR Integer -> Integer -> Integer
opCI Float -> Float -> Float
opCF Double -> Double -> Double
opCD   (SVal Kind
k (Left CV
a)) (SVal Kind
_ (Left 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 State -> Kind -> SV -> SV -> IO SV
opS CV -> CV -> Bool
_    AlgReal -> AlgReal -> AlgReal
_    Integer -> Integer -> Integer
_    Float -> Float -> Float
_    Double -> Double -> Double
_    a :: SVal
a@(SVal Kind
k Either CV (Cached SV)
_)        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 State -> Kind -> SV -> SV -> IO SV
_   CV -> CV -> Bool
okCV 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 (SVal Kind
_ (Left CV
a)) (SVal Kind
_ (Left 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 State -> Kind -> SV -> SV -> IO SV
opS 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
a                 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 SV -> SV -> Maybe SV
shortCut Op
op State
st Kind
k SV
a 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 SV -> Maybe SV
shortCut Op
op State
st Kind
k 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 SV
w SV
x SV
y = case SV -> Kind
swKind SV
x of
                Kind
KFloat  -> Maybe SV
forall a. Maybe a
Nothing
                Kind
KDouble -> Maybe SV
forall a. Maybe a
Nothing
                Kind
_       -> 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 String
_ Int -> Int -> Bool
cmp (Just Int
i, String
_) (Just Int
j, String
_) = Int
i Int -> Int -> Bool
`cmp` Int
j
uiLift String
w Int -> Int -> Bool
_   (Maybe Int, String)
a           (Maybe Int, String)
b           = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" 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 Kind
_ Left{}) = Bool
True
isConcrete SVal
_               = 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 Kind
_     (Left (CV Kind
_     (CInteger Integer
n)))) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
isConcreteZero (SVal Kind
KReal (Left (CV Kind
KReal (CAlgReal AlgReal
v)))) = AlgReal -> Bool
isExactRational AlgReal
v Bool -> Bool -> Bool
&& AlgReal
v AlgReal -> AlgReal -> Bool
forall a. Eq a => a -> a -> Bool
== AlgReal
0
isConcreteZero SVal
_                                           = 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 Kind
_     (Left (CV Kind
_     (CInteger Integer
1)))) = Bool
True
isConcreteOne (SVal Kind
KReal (Left (CV Kind
KReal (CAlgReal AlgReal
v)))) = AlgReal -> Bool
isExactRational AlgReal
v Bool -> Bool -> Bool
&& AlgReal
v AlgReal -> AlgReal -> Bool
forall a. Eq a => a -> a -> Bool
== AlgReal
1
isConcreteOne SVal
_                                           = 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 Kind
_ (Left (CV (KBounded Bool
b Int
w) (CInteger Integer
n)))) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== if Bool
b then -Integer
1 else Int -> Integer
forall a. Bits a => Int -> a
bit Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
isConcreteOnes (SVal Kind
_ (Left (CV Kind
KUnbounded     (CInteger Integer
n)))) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -Integer
1  -- see comment above
isConcreteOnes (SVal Kind
_ (Left (CV Kind
KBool          (CInteger Integer
n)))) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
isConcreteOnes SVal
_                                                = Bool
False

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

-- | Predicate for optimizing comparisons.
isConcreteMin :: SVal -> Bool
isConcreteMin :: SVal -> Bool
isConcreteMin (SVal Kind
_ (Left (CV (KBounded Bool
False Int
_) (CInteger Integer
n)))) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
isConcreteMin (SVal Kind
_ (Left (CV (KBounded Bool
True  Int
w) (CInteger 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
- Int
1)
isConcreteMin (SVal Kind
_ (Left (CV Kind
KBool              (CInteger Integer
n)))) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
isConcreteMin SVal
_                                                    = 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 CV
a CV
b = case (CV -> CVal
cvVal CV
a, CV -> CVal
cvVal CV
b) of
                     (CAlgReal AlgReal
x, CAlgReal AlgReal
y) -> AlgReal -> Bool
isExactRational AlgReal
x Bool -> Bool -> Bool
&& AlgReal -> Bool
isExactRational AlgReal
y
                     (CVal, CVal)
_                        -> Bool
True

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

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

noReal :: String -> AlgReal -> AlgReal -> AlgReal
noReal :: String -> AlgReal -> AlgReal -> AlgReal
noReal String
o AlgReal
a AlgReal
b = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ String
"SBV.AlgReal." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 String
o Float
a Float
b = String -> Float
forall a. HasCallStack => String -> a
error (String -> Float) -> String -> Float
forall a b. (a -> b) -> a -> b
$ String
"SBV.Float." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 String
o Double
a Double
b = String -> Double
forall a. HasCallStack => String -> a
error (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ String
"SBV.Double." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 String
o AlgReal
a = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ String
"SBV.AlgReal." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 String
o Float
a = String -> Float
forall a. HasCallStack => String -> a
error (String -> Float) -> String -> Float
forall a b. (a -> b) -> a -> b
$ String
"SBV.Float." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 String
o Double
a = String -> Double
forall a. HasCallStack => String -> a
error (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ String
"SBV.Double." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 SVal
x 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 SVal
x 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 [Kind]
xs -> [Kind]
xs
               Kind
k         -> String -> [Kind]
forall a. HasCallStack => String -> a
error (String -> [Kind]) -> String -> [Kind]
forall a b. (a -> b) -> a -> b
$ String
"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 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 Int
i 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
_ -> 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
_ -> 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 [(SVal
lti, SVal
_)]          = SVal
lti
                        walk ((SVal
lti, SVal
eqi) : [(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 [Int
1..] [Kind]
ks

-- | Structural less-than for maybes
maybeLT :: SVal -> SVal -> SVal
maybeLT :: SVal -> SVal -> SVal
maybeLT SVal
x 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)
                         (\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 Kind
k' -> Kind
k'
               Kind
k         -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"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 SVal
brNothing SVal -> SVal
brJust 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 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
_ -> 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 SVal
x SVal
y = (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
sEitherCase (\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)
                           (\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 (Kind
ka, Kind
kb) = case SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
x of
                     KEither Kind
k1 Kind
k2 -> (Kind
k1, Kind
k2)
                     Kind
k             -> String -> (Kind, Kind)
forall a. HasCallStack => String -> a
error (String -> (Kind, Kind)) -> String -> (Kind, Kind)
forall a b. (a -> b) -> a -> b
$ String
"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 SVal -> SVal
brA SVal -> SVal
brB 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 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
_ -> 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
_ -> 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) #-}