-----------------------------------------------------------------------------
-- |
-- 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, svFloatingPoint, 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, svZeroExtend, svSignExtend
  , 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
  , svFloatAsSWord32, svDoubleAsSWord64, svFloatingPointAsSWord 
  -- ** Basic array operations
  , SArr(..), readSArr, writeSArr, mergeSArr, newSArr, eqSArr
  -- Utils
  , mkSymOp
  )
  where

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

import qualified Data.IORef         as R    (readIORef)
import qualified Data.IntMap.Strict as IMap (size, insert)

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

import Data.Ratio

import Data.SBV.Utils.Numeric (fpIsEqualObjectH, floatToWord, doubleToWord)

import LibBF

--------------------------------------------------------------------------------
-- 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 Double
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 generalized floating point
svFloatingPoint :: FP -> SVal
svFloatingPoint :: FP -> SVal
svFloatingPoint f :: FP
f@(FP Int
eb Int
sb BigFloat
_) = 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 (FP -> CVal
CFP FP
f))
  where k :: Kind
k  = Int -> Int -> Kind
KFP Int
eb Int
sb

-- | 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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> 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
(+) FP -> FP -> FP
forall a. Num a => a -> a -> a
(+) Rational -> Rational -> Rational
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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> 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
(*) FP -> FP -> FP
forall a. Num a => a -> a -> a
(*) Rational -> Rational -> Rational
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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> SVal
-> SVal
-> SVal
liftSym2 (Op -> State -> Kind -> SV -> SV -> IO SV
mkSymOp Op
Minus) [CV -> CV -> Bool
rationalCheck] (-) (-) (-) (-) (-) (-) SVal
x SVal
y

-- | Unary minus. We handle arbitrary-FP's specially here, just for the negated literals.
svUNeg :: SVal -> SVal
svUNeg :: SVal -> SVal
svUNeg = (State -> Kind -> SV -> IO SV)
-> (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (FP -> FP)
-> (Rational -> Rational)
-> 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 FP -> FP
forall a. Num a => a -> a
negate Rational -> Rational
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)
-> (FP -> FP)
-> (Rational -> Rational)
-> 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 FP -> FP
forall a. Num a => a -> a
abs Rational -> Rational
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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> 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
(/) FP -> FP -> FP
forall a. Fractional a => a -> a -> a
(/) Rational -> Rational -> Rational
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 or a floating point type.
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 or a floating point type.
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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> 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") (String -> FP -> FP -> FP
noFP String
"quot") (String -> Rational -> Rational -> Rational
noRat 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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> 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") (String -> FP -> FP -> FP
noFP String
"rem") (String -> Rational -> Rational -> Rational
noRat 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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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
(==) FP -> FP -> Bool
forall a. Eq a => a -> a -> Bool
(==) Rational -> Rational -> 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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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
(/=) FP -> FP -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Rational -> Rational -> 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
isFP SVal
x,     Just FP
f1 <- SVal -> Maybe FP
getFP SVal
x, Just FP
f2 <- SVal -> Maybe FP
getFP SVal
y = Bool -> SVal
svBool (Bool -> SVal) -> Bool -> SVal
forall a b. (a -> b) -> a -> b
$ FP
f1 FP -> FP -> Bool
forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` FP
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 Bool -> Bool -> Bool
|| SVal -> Bool
forall a. HasKind a => a -> Bool
isFP 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

        getFP :: SVal -> Maybe FP
getFP (SVal Kind
_ (Left (CV Kind
_ (CFP FP
f))))    = FP -> Maybe FP
forall a. a -> Maybe a
Just FP
f
        getFP SVal
_                                 = Maybe FP
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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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
(<) FP -> FP -> Bool
forall a. Ord a => a -> a -> Bool
(<) Rational -> Rational -> 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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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
(>) FP -> FP -> Bool
forall a. Ord a => a -> a -> Bool
(>) Rational -> Rational -> 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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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
(<=) FP -> FP -> Bool
forall a. Ord a => a -> a -> Bool
(<=) Rational -> Rational -> 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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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
(>=) FP -> FP -> Bool
forall a. Ord a => a -> a -> Bool
(>=) Rational -> Rational -> 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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> SVal
-> SVal
-> SVal
liftSym2 ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
mkSymOpSC SV -> SV -> Maybe SV
opt Op
And) [] (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
".&.") (String -> FP -> FP -> FP
noFP String
".&.") (String -> Rational -> Rational -> Rational
noRat 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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> SVal
-> SVal
-> SVal
liftSym2 ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
mkSymOpSC SV -> SV -> Maybe SV
opt Op
Or) []
                       (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
".|.") (String -> FP -> FP -> FP
noFP String
".|.") (String -> Rational -> Rational -> Rational
noRat 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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> SVal
-> SVal
-> SVal
liftSym2 ((SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV
mkSymOpSC SV -> SV -> Maybe SV
opt Op
XOr) []
                       (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") (String -> FP -> FP -> FP
noFP String
"xor") (String -> Rational -> Rational -> Rational
noRat 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)
-> (FP -> FP)
-> (Rational -> Rational)
-> 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") (String -> FP -> FP
noFPUnary String
"complement") (String -> Rational -> Rational
noRatUnary 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)
-> (FP -> FP)
-> (Rational -> Rational)
-> 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") (String -> FP -> FP
noFPUnary String
"rotateL") (String -> Rational -> Rational
noRatUnary 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)
-> (FP -> FP)
-> (Rational -> Rational)
-> 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") (String -> FP -> FP
noFPUnary String
"rotateR") (String -> Rational -> Rational
noRatUnary 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
i Int
j v :: SVal
v@(SVal Kind
KFloat Either CV (Cached SV)
_)  = Int -> Int -> SVal -> SVal
svExtract Int
i Int
j (SVal -> SVal
svFloatAsSWord32  SVal
v)
svExtract Int
i Int
j v :: SVal
v@(SVal Kind
KDouble Either CV (Cached SV)
_) = Int -> Int -> SVal -> SVal
svExtract Int
i Int
j (SVal -> SVal
svDoubleAsSWord64 SVal
v)
svExtract Int
i Int
j v :: SVal
v@(SVal KFP{} Either CV (Cached SV)
_)   = Int -> Int -> SVal -> SVal
svExtract Int
i Int
j (SVal -> SVal
svFloatingPointAsSWord SVal
v)
svExtract Int
_ Int
_ SVal
_ = String -> SVal
forall a. HasCallStack => String -> a
error String
"extract: non-bitvector/float 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
s' Int
j) Either CV (Cached SV)
b)
  | Bool
s Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
s'
  = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"svJoin: received differently signed values: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SVal, SVal) -> String
forall a. Show a => a -> String
show (SVal
x, SVal
y)
  | 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
  = let val :: Integer
val
         | Bool
s -- signed, arithmetic doesn't work; blast and come back
         = let xbits :: [Bool]
xbits = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
xi | Int
xi <- [Int
0 .. Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
               ybits :: [Bool]
ybits = [Integer
n Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
yi | Int
yi <- [Int
0 .. Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
               rbits :: [(Int, Bool)]
rbits = [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([Bool]
ybits [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
xbits)
           in (Integer -> (Int, Bool) -> Integer)
-> Integer -> [(Int, Bool)] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Integer
acc (Int
idx, Bool
set) -> if Bool
set then Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
acc Int
idx else Integer
acc) Integer
0 [(Int, Bool)]
rbits
         | Bool
True -- unsigned, go fast
         = 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
    in 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
val)))
  | 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"

-- | Zero-extend by given number of bits.
svZeroExtend :: Int -> SVal -> SVal
svZeroExtend :: Int -> SVal -> SVal
svZeroExtend = Bool -> (Int -> Op) -> Int -> SVal -> SVal
svExtend Bool
True Int -> Op
ZeroExtend

-- | Sign-extend by given number of bits.
svSignExtend :: Int -> SVal -> SVal
svSignExtend :: Int -> SVal -> SVal
svSignExtend = Bool -> (Int -> Op) -> Int -> SVal -> SVal
svExtend Bool
False Int -> Op
SignExtend

svExtend :: Bool -> (Int -> Op) -> Int -> SVal -> SVal
svExtend :: Bool -> (Int -> Op) -> Int -> SVal -> SVal
svExtend Bool
isZeroExtend Int -> Op
extender Int
i x :: SVal
x@(SVal (KBounded Bool
s Int
sz) Either CV (Cached SV)
a)
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"svExtend: Received negative extension amount: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
  = SVal
x
  | Left (CV Kind
_ (CInteger Integer
cv)) <- Either CV (Cached SV)
a
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k' (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> CV
normCV (Kind -> CVal -> CV
CV Kind
k' (Integer -> CVal
CInteger (Bool -> Integer -> Integer
replBit (Bool -> Bool
not Bool
isZeroExtend Bool -> Bool -> Bool
&& (Integer
cv Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` (Int
szInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))) Integer
cv)))))
  | 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
szInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i)
        z :: State -> IO SV
z 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 -> Op
extender Int
i) [SV
xsw])

        replBit :: Bool -> Integer -> Integer
        replBit :: Bool -> Integer -> Integer
replBit Bool
b = Int -> Integer -> Integer
forall a. Bits a => Int -> a -> a
go Int
sz
          where stop :: Int
stop = Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
                go :: Int -> a -> a
go Int
k a
v | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
stop = a
v
                       | Bool
b         = Int -> a -> a
go (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (a
v a -> Int -> a
forall a. Bits a => a -> Int -> a
`setBit`   Int
k)
                       | Bool
True      = Int -> a -> a
go (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (a
v a -> Int -> a
forall a. Bits a => a -> Int -> a
`clearBit` Int
k)

svExtend Bool
_ Int -> Op
_ Int
_ SVal
_ = String -> SVal
forall a. HasCallStack => String -> a
error String
"svExtend: 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) [])

--------------------------------------------------------------------------------
-- 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) -> (FP -> FP) ->(Rational -> Rational) -> SVal -> SVal
liftSym1 :: (State -> Kind -> SV -> IO SV)
-> (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (FP -> FP)
-> (Rational -> Rational)
-> SVal
-> SVal
liftSym1 State -> Kind -> SV -> IO SV
_   AlgReal -> AlgReal
opCR Integer -> Integer
opCI Float -> Float
opCF Double -> Double
opCD FP -> FP
opFP Rational -> Rational
opRA   (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)
-> (FP -> FP)
-> (Rational -> Rational)
-> (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 FP -> FP
opFP Rational -> Rational
opRA 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
_    FP -> FP
_    Rational -> Rational
_    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)
         -> (FP       -> FP      -> FP)
         -> (Rational -> Rational-> Rational)
         -> 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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> 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 FP -> FP -> FP
opFP Rational -> Rational -> Rational
opRA (SVal Kind
k (Left CV
a)) (SVal Kind
_ (Left CV
b)) | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [CV -> CV -> Bool
f CV
a CV
b | CV -> CV -> Bool
f <- [CV -> CV -> Bool]
okCV] = 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)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> (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 FP -> FP -> FP
opFP Rational -> Rational -> Rational
opRA 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
_    FP -> FP -> FP
_  Rational -> Rational -> Rational
_      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)
          -> (FP                  -> FP                  -> Bool)
          -> (Rational            -> Rational            -> 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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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 FP -> FP -> Bool
opAF Rational -> Rational -> Bool
opAR 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)
-> (FP -> FP -> Bool)
-> (Rational -> Rational -> 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)
-> (FP -> FP -> b)
-> (Rational -> Rational -> 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 FP -> FP -> Bool
opAF Rational -> Rational -> Bool
opAR 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
_    FP -> FP -> Bool
_    Rational -> Rational -> 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/KFloat 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
                KFP{}   -> 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)

noFP :: String -> FP -> FP -> FP
noFP :: String -> FP -> FP -> FP
noFP String
o FP
a FP
b = String -> FP
forall a. HasCallStack => String -> a
error (String -> FP) -> String -> FP
forall a b. (a -> b) -> a -> b
$ String
"SBV.FPR." 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]
++ (FP, FP) -> String
forall a. Show a => a -> String
show (FP
a, FP
b)

noRat:: String -> Rational -> Rational -> Rational
noRat :: String -> Rational -> Rational -> Rational
noRat String
o Rational
a Rational
b = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ String
"SBV.Rational." 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]
++ (Rational, Rational) -> String
forall a. Show a => a -> String
show (Rational
a, Rational
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

noFPUnary :: String -> FP -> FP
noFPUnary :: String -> FP -> FP
noFPUnary String
o FP
a = String -> FP
forall a. HasCallStack => String -> a
error (String -> FP) -> String -> FP
forall a b. (a -> b) -> a -> b
$ String
"SBV.FPR." 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]
++ FP -> String
forall a. Show a => a -> String
show FP
a

noRatUnary :: String -> Rational -> Rational
noRatUnary :: String -> Rational -> Rational
noRatUnary String
o Rational
a = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ String
"SBV.Rational." 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]
++ Rational -> String
forall a. Show a => a -> String
show Rational
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]

-- | Convert an 'Data.SBV.SFloat' to an 'Data.SBV.SWord32', preserving the bit-correspondence. Note that since the
-- representation for @NaN@s are not unique, this function will return a symbolic value when given a
-- concrete @NaN@.
--
-- Implementation note: Since there's no corresponding function in SMTLib for conversion to
-- bit-representation due to partiality, we use a translation trick by allocating a new word variable,
-- converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map
-- it to a simple conversion.
svFloatAsSWord32 :: SVal -> SVal
svFloatAsSWord32 :: SVal -> SVal
svFloatAsSWord32 (SVal Kind
KFloat (Left (CV Kind
KFloat (CFloat Float
f))))
   | Bool -> Bool
not (Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
f)
   = let w32 :: Kind
w32 = Bool -> Int -> Kind
KBounded Bool
False Int
32
     in Kind -> Either CV (Cached SV) -> SVal
SVal Kind
w32 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ 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
w32 (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger (Word32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Float -> Word32
floatToWord Float
f))
svFloatAsSWord32 fVal :: SVal
fVal@(SVal Kind
KFloat Either CV (Cached SV)
_)
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
w32 (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 w32 :: Kind
w32  = Bool -> Int -> Kind
KBounded Bool
False Int
32
        y :: State -> IO SV
y State
st = do Bool
cg <- State -> IO Bool
isCodeGenMode State
st
                  if Bool
cg
                     then do SV
f <- State -> SVal -> IO SV
svToSV State
st SVal
fVal
                             State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
w32 (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret Kind
KFloat Kind
w32)) [SV
f])
                     else do SV
n   <- State -> Kind -> IO SV
internalVariable State
st Kind
w32
                             SV
ysw <- State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KFloat (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret Kind
w32 Kind
KFloat)) [SV
n])
                             State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint State
st Bool
False [] (SVal -> IO ()) -> SVal -> IO ()
forall a b. (a -> b) -> a -> b
$ SVal
fVal SVal -> SVal -> SVal
`svStrongEqual` Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KFloat (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
_ -> SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
ysw)))
                             SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
n
svFloatAsSWord32 (SVal Kind
k Either CV (Cached SV)
_) = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"svFloatAsSWord32: non-float type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

-- | Convert an 'Data.SBV.SDouble' to an 'Data.SBV.SWord64', preserving the bit-correspondence. Note that since the
-- representation for @NaN@s are not unique, this function will return a symbolic value when given a
-- concrete @NaN@.
--
-- Implementation note: Since there's no corresponding function in SMTLib for conversion to
-- bit-representation due to partiality, we use a translation trick by allocating a new word variable,
-- converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map
-- it to a simple conversion.
svDoubleAsSWord64 :: SVal -> SVal
svDoubleAsSWord64 :: SVal -> SVal
svDoubleAsSWord64 (SVal Kind
KDouble (Left (CV Kind
KDouble (CDouble Double
f))))
   | Bool -> Bool
not (Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
f)
   = let w64 :: Kind
w64 = Bool -> Int -> Kind
KBounded Bool
False Int
64
     in Kind -> Either CV (Cached SV) -> SVal
SVal Kind
w64 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ 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
w64 (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Double -> Word64
doubleToWord Double
f))
svDoubleAsSWord64 fVal :: SVal
fVal@(SVal Kind
KDouble Either CV (Cached SV)
_)
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
w64 (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 w64 :: Kind
w64  = Bool -> Int -> Kind
KBounded Bool
False Int
64
        y :: State -> IO SV
y State
st = do Bool
cg <- State -> IO Bool
isCodeGenMode State
st
                  if Bool
cg
                     then do SV
f <- State -> SVal -> IO SV
svToSV State
st SVal
fVal
                             State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
w64 (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret Kind
KDouble Kind
w64)) [SV
f])
                     else do SV
n   <- State -> Kind -> IO SV
internalVariable State
st Kind
w64
                             SV
ysw <- State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KDouble (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret Kind
w64 Kind
KDouble)) [SV
n])
                             State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint State
st Bool
False [] (SVal -> IO ()) -> SVal -> IO ()
forall a b. (a -> b) -> a -> b
$ SVal
fVal SVal -> SVal -> SVal
`svStrongEqual` Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KDouble (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
_ -> SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
ysw)))
                             SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
n
svDoubleAsSWord64 (SVal Kind
k Either CV (Cached SV)
_) = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"svDoubleAsSWord64: non-float type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

-- | Convert a float to the word containing the corresponding bit pattern
svFloatingPointAsSWord :: SVal -> SVal
svFloatingPointAsSWord :: SVal -> SVal
svFloatingPointAsSWord (SVal (KFP Int
eb Int
sb) (Left (CV Kind
_ (CFP f :: FP
f@(FP Int
_ Int
_ BigFloat
fpV)))))
  | Bool -> Bool
not (FP -> Bool
forall a. RealFloat a => a -> Bool
isNaN FP
f)
  = let wN :: Kind
wN = Bool -> Int -> Kind
KBounded Bool
False (Int
eb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sb)
    in Kind -> Either CV (Cached SV) -> SVal
SVal Kind
wN (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ 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
wN (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger (Integer -> CVal) -> Integer -> CVal
forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> Integer
bfToBits (Int -> Int -> RoundMode -> BFOpts
forall a. Integral a => a -> a -> RoundMode -> BFOpts
mkBFOpts Int
eb Int
sb RoundMode
NearEven) BigFloat
fpV
svFloatingPointAsSWord fVal :: SVal
fVal@(SVal kFrom :: Kind
kFrom@(KFP Int
eb Int
sb) Either CV (Cached SV)
_)
  = 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))
  where kTo :: Kind
kTo   = Bool -> Int -> Kind
KBounded Bool
False (Int
eb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sb)
        y :: State -> IO SV
y State
st = do Bool
cg <- State -> IO Bool
isCodeGenMode State
st
                  if Bool
cg
                     then do SV
f <- State -> SVal -> IO SV
svToSV State
st SVal
fVal
                             State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kTo (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret Kind
kFrom Kind
kTo)) [SV
f])
                     else do SV
n   <- State -> Kind -> IO SV
internalVariable State
st Kind
kTo
                             SV
ysw <- State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kFrom (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret Kind
kTo Kind
kFrom)) [SV
n])
                             State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint State
st Bool
False [] (SVal -> IO ()) -> SVal -> IO ()
forall a b. (a -> b) -> a -> b
$ SVal
fVal SVal -> SVal -> SVal
`svStrongEqual` Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kFrom (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
_ -> SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
ysw)))
                             SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
n
svFloatingPointAsSWord (SVal Kind
k Either CV (Cached SV)
_) = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"svFloatingPointAsSWord: non-float type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

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