-----------------------------------------------------------------------------
-- |
-- 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 (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 (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 (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$! 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 (forall a b. a -> Either a b
Left 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 (forall a b. a -> Either a b
Left 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 (forall a b. a -> Either a b
Left 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 (forall a b. a -> Either a b
Left 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 (forall a b. a -> Either a b
Left 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 (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$! Kind -> CVal -> CV
CV Kind
KReal (AlgReal -> CVal
CAlgReal (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)) = forall a. a -> Maybe a
Just (CV -> Bool
cvToBool CV
cv)
svAsBool SVal
_                  = 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)))) = forall a. a -> Maybe a
Just Integer
n
svAsInteger SVal
_                                   = 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))))) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ratio a -> a
numerator Rational
r
svNumerator SVal
_                                                              = 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))))) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ratio a -> a
denominator Rational
r
svDenominator SVal
_                                                              = 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 forall a. Eq a => a -> a -> Bool
/= Integer
f = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Kind -> Integer -> SVal
svInteger (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         = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf SVal
bf)) [Integer
f    .. Integer
t]
  | Bool
True                                                                                                 = 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] forall a. Num a => a -> a -> a
(+) forall a. Num a => a -> a -> a
(+) forall a. Num a => a -> a -> a
(+) forall a. Num a => a -> a -> a
(+) forall a. Num a => a -> a -> a
(+) 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] forall a. Num a => a -> a -> a
(*) forall a. Num a => a -> a -> a
(*) forall a. Num a => a -> a -> a
(*) forall a. Num a => a -> a -> a
(*) forall a. Num a => a -> a -> a
(*) 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) forall a. Num a => a -> a
negate forall a. Num a => a -> a
negate forall a. Num a => a -> a
negate forall a. Num a => a -> a
negate forall a. Num a => a -> a
negate 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) forall a. Num a => a -> a
abs forall a. Num a => a -> a
abs forall a. Num a => a -> a
abs forall a. Num a => a -> a
abs forall a. Num a => a -> a
abs 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] forall a. Fractional a => a -> a -> a
(/) forall {p}. Integral p => p -> p -> p
idiv forall a. Fractional a => a -> a -> a
(/) forall a. Fractional a => a -> a -> a
(/) forall a. Fractional a => a -> a -> a
(/) forall a. Fractional a => a -> a -> a
(/)
   where idiv :: p -> p -> p
idiv p
x p
0 = p
x
         idiv p
x p
y = p
x forall {p}. Integral p => p -> p -> p
`div` p
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 forall a. Ord a => a -> a -> Bool
>= Integer
0 then let go :: t -> SVal -> SVal
go t
n SVal
v
                        | t
n forall a. Eq a => a -> a -> Bool
== t
0 = SVal
one
                        | forall a. Integral a => a -> Bool
even t
n =             t -> SVal -> SVal
go (t
n forall {p}. Integral p => p -> p -> p
`div` t
2) (SVal -> SVal -> SVal
svTimes SVal
v SVal
v)
                        | Bool
True   = SVal -> SVal -> SVal
svTimes SVal
v forall a b. (a -> b) -> a -> b
$ t -> SVal -> SVal
go (t
n forall {p}. Integral p => p -> p -> p
`div` t
2) (SVal -> SVal -> SVal
svTimes SVal
v SVal
v)
                   in  forall {t}. Integral t => t -> SVal -> SVal
go Integer
x SVal
b
              else forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"svExp: exponentiation: negative exponent: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
x
  | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded SVal
e) Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
hasSign SVal
e
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"svExp: exponentiation only works with unsigned bounded symbolic exponents, kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HasKind a => a -> Kind
kindOf SVal
e)
  | Bool
True
  = [SVal] -> SVal
prod forall a b. (a -> b) -> a -> b
$ 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)
                   (forall a. (a -> a) -> a -> [a]
iterate (\SVal
x -> SVal -> SVal -> SVal
svTimes SVal
x SVal
x) SVal
b)
  where prod :: [SVal] -> SVal
prod = 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 (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 = forall a b. (a -> b) -> [a] -> [b]
map (SVal -> Int -> SVal
svTestBit SVal
x) [Int
0 .. forall a. HasKind a => a -> Int
intSizeOf SVal
x 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 (forall a. HasKind a => a -> Kind
kindOf SVal
x) (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 = forall a. [a] -> [a]
reverse 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 (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
iforall 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse

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

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

-- | Decrement:
svDecrement :: SVal -> SVal
svDecrement :: SVal -> SVal
svDecrement SVal
x = 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 (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") forall {p}. Integral p => p -> p -> p
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 | forall a. HasKind a => a -> Kind
kindOf SVal
x forall a. Eq a => a -> a -> Bool
== Kind
KUnbounded = forall {p}. Integral p => p -> p -> p
div a
a (forall a. Num a => a -> a
abs a
b) forall a. Num a => a -> a -> a
* forall a. Num a => a -> a
signum a
b
              | Bool
otherwise              = forall {p}. Integral p => p -> p -> p
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 (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") forall {p}. Integral p => p -> p -> p
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 | forall a. HasKind a => a -> Kind
kindOf SVal
x forall a. Eq a => a -> a -> Bool
== Kind
KUnbounded = forall {p}. Integral p => p -> p -> p
mod a
a (forall a. Num a => a -> a
abs a
b)
             | Bool
otherwise              = forall {p}. Integral p => p -> p -> p
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 forall a. Eq a => a -> a -> Bool
== Kind
KBool Bool -> Bool -> Bool
&& Op
op forall a. Eq a => a -> a -> Bool
== Op
Equal    Bool -> Bool -> Bool
&& SV
x forall a. Eq a => a -> a -> Bool
== SV
trueSV  = forall a. a -> Maybe a
Just SV
y         -- true  .== y     --> y
  | Kind
k forall a. Eq a => a -> a -> Bool
== Kind
KBool Bool -> Bool -> Bool
&& Op
op forall a. Eq a => a -> a -> Bool
== Op
Equal    Bool -> Bool -> Bool
&& SV
y forall a. Eq a => a -> a -> Bool
== SV
trueSV  = forall a. a -> Maybe a
Just SV
x         -- x     .== true  --> x
  | Kind
k forall a. Eq a => a -> a -> Bool
== Kind
KBool Bool -> Bool -> Bool
&& Op
op forall a. Eq a => a -> a -> Bool
== Op
NotEqual Bool -> Bool -> Bool
&& SV
x forall a. Eq a => a -> a -> Bool
== SV
falseSV = forall a. a -> Maybe a
Just SV
y         -- false ./= y     --> y
  | Kind
k forall a. Eq a => a -> a -> Bool
== Kind
KBool Bool -> Bool -> Bool
&& Op
op forall a. Eq a => a -> a -> Bool
== Op
NotEqual Bool -> Bool -> Bool
&& SV
y forall a. Eq a => a -> a -> Bool
== SV
falseSV = 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
  | forall a. HasKind a => a -> Bool
isSet SVal
a Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> Bool
(==) forall a. Eq a => a -> a -> 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
  | forall a. HasKind a => a -> Bool
isSet SVal
a Bool -> Bool -> Bool
&& forall a. HasKind a => a -> Bool
isSet SVal
b
  = SVal -> SVal
svNot 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 forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> Bool
(/=) forall a. Eq a => a -> a -> 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 (forall a. HasKind a => a -> Bool
isSet SVal
sa Bool -> Bool -> Bool
&& forall a. HasKind a => a -> Bool
isSet SVal
sb Bool -> Bool -> Bool
&& forall a. HasKind a => a -> Kind
kindOf SVal
sa forall a. Eq a => a -> a -> Bool
== forall a. HasKind a => a -> Kind
kindOf SVal
sb)
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.svSetEqual: Called on ill-typed args: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HasKind a => a -> Kind
kindOf SVal
sa, 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 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 forall a. Eq a => a -> a -> Bool
== Set CVal
b)
  | Bool
True
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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)))) = forall a. a -> Maybe a
Just RCSet CVal
s
        getSet SVal
_                               = 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 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 | 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 forall a b. (a -> b) -> a -> b
$ Float
f1 forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Float
f2
                  | 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 forall a b. (a -> b) -> a -> b
$ Double
f1 forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Double
f2
                  | 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 forall a b. (a -> b) -> a -> b
$ FP
f1 forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` FP
f2
                  | forall a. HasKind a => a -> Bool
isFloat SVal
x Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
isDouble SVal
x Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
isFP SVal
x                  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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)))) = forall a. a -> Maybe a
Just Float
f
        getF SVal
_                                 = forall a. Maybe a
Nothing

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

        getFP :: SVal -> Maybe FP
getFP (SVal Kind
_ (Left (CV Kind
_ (CFP FP
f))))    = forall a. a -> Maybe a
Just FP
f
        getFP SVal
_                                 = 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 forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) forall a. Ord a => a -> a -> Bool
(<) (String
-> (Int -> Int -> Bool)
-> (Maybe Int, String)
-> (Maybe Int, String)
-> Bool
uiLift String
"<" 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 forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) forall a. Ord a => a -> a -> Bool
(>) (String
-> (Int -> Int -> Bool)
-> (Maybe Int, String)
-> (Maybe Int, String)
-> Bool
uiLift String
">"  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 forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) forall a. Ord a => a -> a -> Bool
(<=) (String
-> (Int -> Int -> Bool)
-> (Maybe Int, String)
-> (Maybe Int, String)
-> Bool
uiLift String
"<=" 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 forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) forall a. Ord a => a -> a -> Bool
(>=) (String
-> (Int -> Int -> Bool)
-> (Maybe Int, String)
-> (Maybe Int, String)
-> Bool
uiLift String
">=" 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
".&.") 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 forall a. Eq a => a -> a -> Bool
== SV
falseSV Bool -> Bool -> Bool
|| SV
b forall a. Eq a => a -> a -> Bool
== SV
falseSV = forall a. a -> Maybe a
Just SV
falseSV
          | SV
a forall a. Eq a => a -> a -> Bool
== SV
trueSV                  = forall a. a -> Maybe a
Just SV
b
          | SV
b forall a. Eq a => a -> a -> Bool
== SV
trueSV                  = forall a. a -> Maybe a
Just SV
a
          | Bool
True                         = 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
".|.") 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 forall a. Eq a => a -> a -> Bool
== SV
trueSV Bool -> Bool -> Bool
|| SV
b forall a. Eq a => a -> a -> Bool
== SV
trueSV = forall a. a -> Maybe a
Just SV
trueSV
          | SV
a forall a. Eq a => a -> a -> Bool
== SV
falseSV               = forall a. a -> Maybe a
Just SV
b
          | SV
b forall a. Eq a => a -> a -> Bool
== SV
falseSV               = forall a. a -> Maybe a
Just SV
a
          | Bool
True                       = 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") 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 forall a. Eq a => a -> a -> Bool
== SV
b Bool -> Bool -> Bool
&& SV -> Kind
swKind SV
a forall a. Eq a => a -> a -> Bool
== Kind
KBool = forall a. a -> Maybe a
Just SV
falseSV
          | SV
a forall a. Eq a => a -> a -> Bool
== SV
falseSV                = forall a. a -> Maybe a
Just SV
b
          | SV
b forall a. Eq a => a -> a -> Bool
== SV
falseSV                = forall a. a -> Maybe a
Just SV
a
          | Bool
True                        = 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") 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 forall a. Eq a => a -> a -> Bool
== SV
falseSV = forall a. a -> Maybe a
Just SV
trueSV
          | SV
a forall a. Eq a => a -> a -> Bool
== SV
trueSV  = forall a. a -> Maybe a
Just SV
falseSV
          | Bool
True         = 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 forall a. Ord a => a -> a -> Bool
<= Int
0
  = SVal
x
  | forall a. HasKind a => a -> Bool
isBounded SVal
x, Int
i forall a. Ord a => a -> a -> Bool
>= 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 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
  where k :: Kind
k = 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 forall a. Ord a => a -> a -> Bool
<= Int
0
  = SVal
x
  | forall a. HasKind a => a -> Bool
isBounded SVal
x, Int
i forall a. Ord a => a -> a -> Bool
>= forall a. HasKind a => a -> Int
intSizeOf SVal
x
  = if Bool -> Bool
not (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 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
  where k :: Kind
k    = 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 forall a. Ord a => a -> a -> Bool
<= Int
0
  = SVal
x
  | Bool
True
  = case 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 forall {p}. Integral p => p -> p -> p
`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 forall a. Ord a => a -> a -> Bool
<= Int
0
  = SVal
x
  | Bool
True
  = case 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 forall {p}. Integral p => p -> p -> p
`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 forall a. Ord a => a -> a -> Bool
< Int
2 = Integer
x
  | Bool
True   = forall {a}. (Bits a, Num a) => a -> Int -> a
norm Integer
x Int
y' forall a. Bits a => a -> Int -> a
`shiftL` Int
y  forall a. Bits a => a -> a -> a
.|. forall {a}. (Bits a, Num a) => a -> Int -> a
norm (Integer
x forall a. Bits a => a -> Int -> a
`shiftR` Int
y') Int
y
  where (Int
y, Int
y') | Bool
toLeft = (Int
amt forall {p}. Integral p => p -> p -> p
`mod` Int
sz, Int
sz forall a. Num a => a -> a -> a
- Int
y)
                | Bool
True   = (Int
sz forall a. Num a => a -> a -> a
- Int
y', Int
amt forall {p}. Integral p => p -> p -> p
`mod` Int
sz)
        norm :: a -> Int -> a
norm a
v Int
s = a
v forall a. Bits a => a -> a -> a
.&. ((a
1 forall a. Bits a => a -> Int -> a
`shiftL` Int
s) 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 forall a. Ord a => a -> a -> Bool
< Int
j
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (forall a b. a -> Either a b
Left 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 (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$! CV -> CV
normCV (Kind -> CVal -> CV
CV Kind
k (Integer -> CVal
CInteger (Integer
v forall a. Bits a => a -> Int -> a
`shiftR` Int
j))))
  | Bool
True
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y))
  where k :: Kind
k = Bool -> Int -> Kind
KBounded Bool
s (Int
i forall a. Num a => a -> a -> a
- Int
j 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
_ = 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 forall a. Eq a => a -> a -> Bool
/= Bool
s'
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"svJoin: received differently signed values: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SVal
x, SVal
y)
  | Int
i forall a. Eq a => a -> a -> Bool
== Int
0 = SVal
y
  | Int
j 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 forall a. Bits a => a -> Int -> Bool
`testBit` Int
xi | Int
xi <- [Int
0 .. Int
iforall a. Num a => a -> a -> a
-Int
1]]
               ybits :: [Bool]
ybits = [Integer
n forall a. Bits a => a -> Int -> Bool
`testBit` Int
yi | Int
yi <- [Int
0 .. Int
jforall a. Num a => a -> a -> a
-Int
1]]
               rbits :: [(Int, Bool)]
rbits = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([Bool]
ybits forall a. [a] -> [a] -> [a]
++ [Bool]
xbits)
           in forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Integer
acc (Int
idx, Bool
set) -> if Bool
set then 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 forall a. Bits a => a -> Int -> a
`shiftL` Int
j forall a. Bits a => a -> a -> a
.|. Integer
n
    in Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (forall a b. a -> Either a b
Left 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 (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
z))
  where
    k :: Kind
k = Bool -> Int -> Kind
KBounded Bool
s (Int
i 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
_ = 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 forall a. Ord a => a -> a -> Bool
< Int
0
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"svExtend: Received negative extension amount: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
  | Int
i 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' (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 forall a. Bits a => a -> Int -> Bool
`testBit` (Int
szforall a. Num a => a -> a -> a
-Int
1))) Integer
cv)))))
  | Bool
True
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k' (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
z))
  where k' :: Kind
k' = Bool -> Int -> Kind
KBounded Bool
s (Int
szforall 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 = forall {t}. Bits t => Int -> t -> t
go Int
sz
          where stop :: Int
stop = Int
sz forall a. Num a => a -> a -> a
+ Int
i
                go :: Int -> t -> t
go Int
k t
v | Int
k forall a. Eq a => a -> a -> Bool
== Int
stop = t
v
                       | Bool
b         = Int -> t -> t
go (Int
kforall a. Num a => a -> a -> a
+Int
1) (t
v forall a. Bits a => a -> Int -> a
`setBit`   Int
k)
                       | Bool
True      = Int -> t -> t
go (Int
kforall a. Num a => a -> a -> a
+Int
1) (t
v forall a. Bits a => a -> Int -> a
`clearBit` Int
k)

svExtend Bool
_ Int -> Op
_ Int
_ 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 (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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 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 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 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 forall a. Eq a => a -> a -> Bool
== SV
swb                      -> forall (m :: * -> *) a. Monad m => a -> m a
return SV
swa                                     -- if t then a      else a     ==> a
                               () | SV
swa forall a. Eq a => a -> a -> Bool
== SV
trueSV Bool -> Bool -> Bool
&& SV
swb forall a. Eq a => a -> a -> Bool
== SV
falseSV -> forall (m :: * -> *) a. Monad m => a -> m a
return SV
swt                                     -- if t then true   else false ==> t
                               () | SV
swa forall a. Eq a => a -> a -> Bool
== SV
falseSV Bool -> Bool -> Bool
&& SV
swb 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 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 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 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 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 forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
i forall a. Ord a => a -> a -> Bool
>= forall i a. Num i => [a] -> i
genericLength [SVal]
xs
                    then SVal
err
                    else [SVal]
xs forall i a. Integral i => [a] -> i -> a
`genericIndex` Integer
i
      CVal
_          -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.select: unsupported " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HasKind a => a -> Kind
kindOf SVal
ind) forall a. [a] -> [a] -> [a]
++ String
" valued select/index expression"
svSelect [SVal]
xsOrig SVal
err SVal
ind = [SVal]
xs seq :: forall a b. a -> b -> b
`seq` Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kElt (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r))
  where
    kInd :: Kind
kInd = forall a. HasKind a => a -> Kind
kindOf SVal
ind
    kElt :: Kind
kElt = 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 -> forall i a. Integral i => i -> [a] -> [a]
genericTake ((Integer
2::Integer) forall a b. (Num a, Integral b) => a -> b -> a
^ Int
i) [SVal]
xsOrig
           KBounded Bool
True  Int
i -> forall i a. Integral i => i -> [a] -> [a]
genericTake ((Integer
2::Integer) forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
iforall a. Num a => a -> a -> a
-Int
1)) [SVal]
xsOrig
           Kind
KUnbounded       -> [SVal]
xsOrig
           Kind
_                -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.select: unsupported " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
kInd forall a. [a] -> [a] -> [a]
++ String
" valued select/index expression"
    r :: State -> IO SV
r State
st = do [SV]
sws <- 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 forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== SV
swe) [SV]
sws  -- off-chance that all elts are the same
                 then 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 = 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 (forall a. HasKind a => a -> Bool
isBounded SVal
x)       = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV." forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
": Received non bit-vector kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (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 (forall a b. b -> Either a b
Right (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 (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 (forall a. HasKind a => a -> Int
intSizeOf SVal
x 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 (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y))
        kFrom :: Kind
kFrom  = 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 = 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 forall a. Ord a => a -> a -> Bool
< 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
          forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal -> SVal
svIte (SVal
i SVal -> SVal -> SVal
`svGreaterEq` Kind -> Integer -> SVal
svInteger Kind
ki (forall a b. (Integral a, Num b) => a -> b
fromIntegral (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 = forall a. HasKind a => a -> Kind
kindOf SVal
x
        ki :: Kind
ki = 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 forall a. Eq a => a -> a -> Bool
== Integer
0
          = forall a. a -> Maybe a
Just SVal
x

          | Just Integer
xv <- SVal -> Maybe Integer
getConst SVal
x, Integer
xv forall a. Eq a => a -> a -> Bool
== Integer
0
          = 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
          = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$! CV -> CV
normCV 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))

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

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

          | Bool
True
          = forall a. Maybe a
Nothing

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

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

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

                -- like fromIntegral, but more paranoid
                shiftAmount :: Integer -> Int
                shiftAmount :: Integer -> Int
shiftAmount Integer
iv
                  | Integer
iv forall a. Ord a => a -> a -> Bool
<= Integer
0                                            = Int
0
                  | forall a. HasKind a => a -> Bool
isUnbounded SVal
i, Integer
iv forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Int) = forall {a}. String -> a
bailOut forall a b. (a -> b) -> a -> b
$ String
"Unsupported constant unbounded shift with amount: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
iv
                  | forall a. HasKind a => a -> Bool
isUnbounded SVal
x                                      = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
iv
                  | Integer
iv forall a. Ord a => a -> a -> Bool
>= forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
ub                              = Int
ub
                  | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded SVal
x Bool -> Bool -> Bool
&& forall a. HasKind a => a -> Bool
isBounded SVal
i)                   = forall {a}. String -> a
bailOut forall a b. (a -> b) -> a -> b
$ String
"Unsupported kinds: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind
kx, Kind
ki)
                  | Bool
True                                               = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
iv
                 where ub :: Int
ub = 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 forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. HasKind a => a -> Int
intSizeOf SVal
x)
          where maxRepresentable :: Integer
                maxRepresentable :: Integer
maxRepresentable
                  | forall a. HasKind a => a -> Bool
hasSign SVal
i = forall a. Bits a => Int -> a
bit (forall a. HasKind a => a -> Int
intSizeOf SVal
i forall a. Num a => a -> a -> a
- Int
1) forall a. Num a => a -> a -> a
- Integer
1
                  | Bool
True      = forall a. Bits a => Int -> a
bit (forall a. HasKind a => a -> Int
intSizeOf SVal
i    ) 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
                       | 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== Kind
ki
                                                 then 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 (forall a. HasKind a => a -> Bool
isBounded SVal
x)
  = SVal -> SVal -> SVal
svShiftLeft SVal
x SVal
i
  | forall a. HasKind a => a -> Bool
isBounded SVal
i Bool -> Bool -> Bool
&& forall a. Bits a => Int -> a
bit Int
si forall a. Ord a => a -> a -> Bool
<= 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 .. forall a. Bits a => Int -> a
bit Int
si 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 .. forall a. Bits a => Int -> a
bit Int
si 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     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     forall a. Num a => a -> a -> a
- Int
1]] SVal
z (       SVal
i SVal -> SVal -> SVal
`svRem` SVal
n))
    where sx :: Int
sx = forall a. HasKind a => a -> Int
intSizeOf SVal
x
          si :: Int
si = forall a. HasKind a => a -> Int
intSizeOf SVal
i
          z :: SVal
z  = Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf SVal
x) Integer
0
          zi :: SVal
zi = Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf SVal
i) Integer
0
          n :: SVal
n  = Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf SVal
i) (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 (forall a. HasKind a => a -> Bool
isBounded SVal
x Bool -> Bool -> Bool
&& forall a. HasKind a => a -> Bool
isBounded SVal
i Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. HasKind a => a -> Bool
hasSign SVal
i))
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.Dynamic.svBarrelRotateLeft: Arguments must be bounded with second argument unsigned. Received: " forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
iv forall {p}. Integral p => p -> p -> p
`rem` forall a b. (Integral a, Num b) => a -> b
fromIntegral (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 (forall a. HasKind a => a -> Bool
isBounded SVal
x Bool -> Bool -> Bool
&& forall a. HasKind a => a -> Bool
isBounded SVal
i Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. HasKind a => a -> Bool
hasSign SVal
i))
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.Dynamic.svBarrelRotateRight: Arguments must be bounded with second argument unsigned. Received: " forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
iv forall {p}. Integral p => p -> p -> p
`rem` forall a b. (Integral a, Num b) => a -> b
fromIntegral (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 (forall a. Num a => Integer -> a
fromInteger Integer
v)) SVal
acc)

        sa :: Integer
sa = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> Int
intSizeOf SVal
a
        n :: SVal
n  = Kind -> Integer -> SVal
svInteger (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 = forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall {a}. (a, Integer) -> Bool
significant forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (SVal -> [SVal]
svBlastLE SVal
reducedC) [Integer
2forall 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 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 (forall a. HasKind a => a -> Bool
isBounded SVal
x)
  = SVal -> SVal -> SVal
svShiftRight SVal
x SVal
i
  | forall a. HasKind a => a -> Bool
isBounded SVal
i Bool -> Bool -> Bool
&& forall a. Bits a => Int -> a
bit Int
si forall a. Ord a => a -> a -> Bool
<= 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 .. forall a. Bits a => Int -> a
bit Int
si 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 .. forall a. Bits a => Int -> a
bit Int
si 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     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     forall a. Num a => a -> a -> a
- Int
1]] SVal
z (       SVal
i SVal -> SVal -> SVal
`svRem` SVal
n))
    where sx :: Int
sx = forall a. HasKind a => a -> Int
intSizeOf SVal
x
          si :: Int
si = forall a. HasKind a => a -> Int
intSizeOf SVal
i
          z :: SVal
z  = Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf SVal
x) Integer
0
          zi :: SVal
zi = Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf SVal
i) Integer
0
          n :: SVal
n  = Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf SVal
i) (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 (forall a b. b -> Either a b
Right (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 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> IO a
R.readIORef (State -> IORef ArrayMap
rArrayMap State
st)

                  let j :: ArrayIndex
j   = Int -> ArrayIndex
ArrayIndex forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> Int
IMap.size ArrayMap
amap
                      upd :: ArrayMap -> ArrayMap
upd = forall a. Int -> a -> IntMap a -> IntMap a
IMap.insert (ArrayIndex -> Int
unArrayIndex ArrayIndex
j) (String
"array_" forall a. [a] -> [a] -> [a]
++ 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 seq :: forall a b. a -> b -> b
`seq` forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef ArrayMap
rArrayMap ArrayMap -> ArrayMap
upd forall a b. (a -> b) -> a -> b
$ forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef ArrayMap
rNewArrs ArrayMap -> ArrayMap
upd
                  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 forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> IO a
R.readIORef (State -> IORef ArrayMap
rArrayMap State
st)

                  let k :: ArrayIndex
k   = Int -> ArrayIndex
ArrayIndex forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> Int
IMap.size ArrayMap
amap
                      upd :: ArrayMap -> ArrayMap
upd = forall a. Int -> a -> IntMap a -> IntMap a
IMap.insert (ArrayIndex -> Int
unArrayIndex ArrayIndex
k) (String
"array_" forall a. [a] -> [a] -> [a]
++ 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 seq :: forall a b. a -> b -> b
`seq` forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef ArrayMap
rArrayMap ArrayMap -> ArrayMap
upd forall a b. (a -> b) -> a -> b
$ forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef ArrayMap
rNewArrs ArrayMap -> ArrayMap
upd
                  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 <- forall a. IORef a -> IO a
R.readIORef forall a b. (a -> b) -> a -> b
$ State -> IORef ArrayMap
rArrayMap State
st

    Maybe SV
mbSWDef <- case Maybe SVal
mbDef of
                 Maybe SVal
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                 Just SVal
sv -> forall a. a -> Maybe a
Just 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 forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> Int
IMap.size ArrayMap
amap
        nm :: String
nm  = Int -> String
mkNm (ArrayIndex -> Int
unArrayIndex ArrayIndex
i)
        upd :: ArrayMap -> ArrayMap
upd = 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

    forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef ArrayMap
rArrayMap ArrayMap -> ArrayMap
upd forall a b. (a -> b) -> a -> b
$ forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef ArrayMap
rNewArrs ArrayMap -> ArrayMap
upd
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Kind, Kind) -> Cached ArrayIndex -> SArr
SArr (Kind, Kind)
ainfo forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 :: forall a. (Maybe Int, String) -> a
noUnint (Maybe Int, String)
x = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected operation called on uninterpreted/enumerated value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Maybe Int, String)
x

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

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

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

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

noStringLift2 :: String -> String -> a
noStringLift2 :: forall a. String -> String -> a
noStringLift2 String
x String
y = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected binary operation called on strings: " forall a. [a] -> [a] -> [a]
++ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left  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 forall a. Char -> a
noCharLift forall {a}. String -> a
noStringLift 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 = 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)) | 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left  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 forall a. Char -> Char -> a
noCharLift2 forall a. String -> String -> a
noStringLift2 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right 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 (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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right 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 = 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])) 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 (forall a b. a -> b -> a
const (forall a b. a -> b -> a
const 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 = 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])) 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 (forall a b. a -> b -> a
const 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  -> forall a. Maybe a
Nothing
                Kind
KDouble -> forall a. Maybe a
Nothing
                KFP{}   -> forall a. Maybe a
Nothing
                Kind
_       -> if SV
x forall a. Eq a => a -> a -> Bool
== SV
y then forall a. a -> Maybe a
Just SV
w else 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           = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.Core.Operations: Impossible happened while trying to lift " forall a. [a] -> [a] -> [a]
++ String
w forall a. [a] -> [a] -> [a]
++ String
" over " forall a. [a] -> [a] -> [a]
++ 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 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 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 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 forall a. Eq a => a -> a -> Bool
== if Bool
b then -Integer
1 else forall a. Bits a => Int -> a
bit Int
w forall a. Num a => a -> a -> a
- Integer
1
isConcreteOnes (SVal Kind
_ (Left (CV Kind
KUnbounded     (CInteger Integer
n)))) = Integer
n forall a. Eq a => a -> a -> Bool
== -Integer
1  -- see comment above
isConcreteOnes (SVal Kind
_ (Left (CV Kind
KBool          (CInteger Integer
n)))) = Integer
n 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 forall a. Eq a => a -> a -> Bool
== forall a. Bits a => Int -> a
bit Int
w forall a. Num a => a -> a -> a
- Integer
1
isConcreteMax (SVal Kind
_ (Left (CV (KBounded Bool
True  Int
w) (CInteger Integer
n)))) = Integer
n forall a. Eq a => a -> a -> Bool
== forall a. Bits a => Int -> a
bit (Int
w forall a. Num a => a -> a -> a
- Int
1) forall a. Num a => a -> a -> a
- Integer
1
isConcreteMax (SVal Kind
_ (Left (CV Kind
KBool              (CInteger Integer
n)))) = Integer
n 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 forall a. Eq a => a -> a -> Bool
== Integer
0
isConcreteMin (SVal Kind
_ (Left (CV (KBounded Bool
True  Int
w) (CInteger Integer
n)))) = Integer
n forall a. Eq a => a -> a -> Bool
== - forall a. Bits a => Int -> a
bit (Int
w forall a. Num a => a -> a -> a
- Int
1)
isConcreteMin (SVal Kind
_ (Left (CV Kind
KBool              (CInteger Integer
n)))) = Integer
n 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 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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.AlgReal." forall a. [a] -> [a] -> [a]
++ String
o forall a. [a] -> [a] -> [a]
++ String
": Unexpected arguments: " forall a. [a] -> [a] -> [a]
++ 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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.Float." forall a. [a] -> [a] -> [a]
++ String
o forall a. [a] -> [a] -> [a]
++ String
": Unexpected arguments: " forall a. [a] -> [a] -> [a]
++ 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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.Double." forall a. [a] -> [a] -> [a]
++ String
o forall a. [a] -> [a] -> [a]
++ String
": Unexpected arguments: " forall a. [a] -> [a] -> [a]
++ 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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.FPR." forall a. [a] -> [a] -> [a]
++ String
o forall a. [a] -> [a] -> [a]
++ String
": Unexpected arguments: " forall a. [a] -> [a] -> [a]
++ 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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.Rational." forall a. [a] -> [a] -> [a]
++ String
o forall a. [a] -> [a] -> [a]
++ String
": Unexpected arguments: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Rational
a, Rational
b)

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

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

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

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

noRatUnary :: String -> Rational -> Rational
noRatUnary :: String -> Rational -> Rational
noRatUnary String
o Rational
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.Rational." forall a. [a] -> [a] -> [a]
++ String
o forall a. [a] -> [a] -> [a]
++ String
": Unexpected argument: " forall a. [a] -> [a] -> [a]
++ 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 = 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
  where ks :: [Kind]
ks = case forall a. HasKind a => a -> Kind
kindOf SVal
x of
               KTuple [Kind]
xs -> [Kind]
xs
               Kind
k         -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible happened, tupleLT called with: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind
k, SVal
x, SVal
y)

        n :: Int
n = 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache forall a b. (a -> b) -> a -> b
$ \State
_ -> State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
ek 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache forall a b. (a -> b) -> a -> b
$ \State
_ -> State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
ek 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 forall a b. (a -> b) -> a -> b
$ [(SVal, SVal)] -> SVal
walk forall a b. (a -> b) -> a -> b
$ 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 (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 forall a. HasKind a => a -> Kind
kindOf SVal
x of
               KMaybe Kind
k' -> Kind
k'
               Kind
k         -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible happened, maybeLT called with: " forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache forall a b. (a -> b) -> a -> b
$ \State
_ -> State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
ka 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 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 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`) (forall a b. a -> b -> a
const SVal
svTrue)              SVal
y)
                           (\SVal
rx -> (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
sEitherCase (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 forall a. HasKind a => a -> Kind
kindOf SVal
x of
                     KEither Kind
k1 Kind
k2 -> (Kind
k1, Kind
k2)
                     Kind
k             -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible happened, eitherLT called with: " forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache forall a b. (a -> b) -> a -> b
$ \State
_ -> State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
ka 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 forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache forall a b. (a -> b) -> a -> b
$ \State
_ -> State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kb 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 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 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 (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 forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
w32 forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger (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 (forall a b. b -> Either a b
Right (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 [] forall a b. (a -> b) -> a -> b
$ SVal
fVal SVal -> SVal -> SVal
`svStrongEqual` Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KFloat (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache (\State
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return SV
ysw)))
                             forall (m :: * -> *) a. Monad m => a -> m a
return SV
n
svFloatAsSWord32 (SVal Kind
k Either CV (Cached SV)
_) = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"svFloatAsSWord32: non-float type: " forall a. [a] -> [a] -> [a]
++ 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 (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 forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
w64 forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger (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 (forall a b. b -> Either a b
Right (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 [] forall a b. (a -> b) -> a -> b
$ SVal
fVal SVal -> SVal -> SVal
`svStrongEqual` Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KDouble (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache (\State
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return SV
ysw)))
                             forall (m :: * -> *) a. Monad m => a -> m a
return SV
n
svDoubleAsSWord64 (SVal Kind
k Either CV (Cached SV)
_) = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"svDoubleAsSWord64: non-float type: " forall a. [a] -> [a] -> [a]
++ 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 (forall a. RealFloat a => a -> Bool
isNaN FP
f)
  = let wN :: Kind
wN = Bool -> Int -> Kind
KBounded Bool
False (Int
eb forall a. Num a => a -> a -> a
+ Int
sb)
    in Kind -> Either CV (Cached SV) -> SVal
SVal Kind
wN forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
wN forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger forall a b. (a -> b) -> a -> b
$ BFOpts -> BigFloat -> Integer
bfToBits (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 (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y))
  where kTo :: Kind
kTo   = Bool -> Int -> Kind
KBounded Bool
False (Int
eb 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 [] forall a b. (a -> b) -> a -> b
$ SVal
fVal SVal -> SVal -> SVal
`svStrongEqual` Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kFrom (forall a b. b -> Either a b
Right (forall a. (State -> IO a) -> Cached a
cache (\State
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return SV
ysw)))
                             forall (m :: * -> *) a. Monad m => a -> m a
return SV
n
svFloatingPointAsSWord (SVal Kind
k Either CV (Cached SV)
_) = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"svFloatingPointAsSWord: non-float type: " forall a. [a] -> [a] -> [a]
++ 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) #-}