-----------------------------------------------------------------------------
-- |
-- 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        #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}

{-# 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, svSignum
  , svDivide, svQuot, svRem, svQuotRem, svDivides
  , svEqual, svNotEqual, svStrongEqual, svImplies
  , 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
  , svMkOverflow1, svMkOverflow2
  -- ** Derived operations
  , svToWord1, svFromWord1, svTestBit
  , svShiftLeft, svShiftRight
  , svRotateLeft, svRotateRight
  , svBarrelRotateLeft, svBarrelRotateRight
  , svBlastLE, svBlastBE
  , svAddConstant, svIncrement, svDecrement
  , svFloatAsSWord32, svDoubleAsSWord64, svFloatingPointAsSWord
  -- Utils
  , mkSymOp
  )
  where

import Prelude hiding (Foldable(..))
import Data.Bits (Bits(..))
import Data.List (genericIndex, genericLength, genericTake, foldr, length, foldl', elem, nub, sort)

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

import Data.Ratio

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

import LibBF

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

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

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

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

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

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

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

-- | Convert from a generalized floating point
svFloatingPoint :: FP -> SVal
svFloatingPoint :: FP -> SVal
svFloatingPoint f :: FP
f@(FP Int
eb Int
sb BigFloat
_) = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$! Kind -> CVal -> CV
CV Kind
k (FP -> CVal
CFP FP
f))
  where k :: Kind
k  = Int -> Int -> Kind
KFP Int
eb Int
sb

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Unary minus. We handle arbitrary-FP's specially here, just for the negated literals.
svUNeg :: SVal -> SVal
svUNeg :: SVal -> SVal
svUNeg = (State -> Kind -> SV -> IO SV)
-> (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (FP -> FP)
-> (Rational -> Rational)
-> SVal
-> SVal
liftSym1 (Op -> State -> Kind -> SV -> IO SV
mkSymOp1 Op
UNeg) AlgReal -> AlgReal
forall a. Num a => a -> a
negate Integer -> Integer
forall a. Num a => a -> a
negate Float -> Float
forall a. Num a => a -> a
negate Double -> Double
forall a. Num a => a -> a
negate FP -> FP
forall a. Num a => a -> a
negate Rational -> Rational
forall a. Num a => a -> a
negate

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

-- | Signum.
--
-- NB. The following "carefully" tests the number for == 0, as Float/Double's NaN and +/-0
-- cases would cause trouble with explicit equality tests.
svSignum :: SVal -> SVal
svSignum :: SVal -> SVal
svSignum SVal
a
  | SVal -> Bool
forall a. HasKind a => a -> Bool
hasSign SVal
a = SVal -> SVal -> SVal -> SVal
svIte (SVal
a SVal -> SVal -> SVal
`svGreaterThan` SVal
z) SVal
i
              (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal -> SVal
svIte (SVal
a SVal -> SVal -> SVal
`svLessThan`    SVal
z) (SVal -> SVal
svUNeg SVal
i) SVal
a
  | Bool
True      = SVal -> SVal -> SVal -> SVal
svIte (SVal
a SVal -> SVal -> SVal
`svGreaterThan` SVal
z) SVal
i SVal
a
  where k :: Kind
k = SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
a
        z :: SVal
z = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (Integer
0 :: Integer)
        i :: SVal
i = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (Integer
1 :: Integer)

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

-- | Divides predicate
svDivides :: Integer -> SVal -> SVal
svDivides :: Integer -> SVal -> SVal
svDivides Integer
n SVal
v
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"svDivides: The first argument must be a strictly positive number, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
  | Bool
True   = case SVal
v of
              SVal Kind
KUnbounded (Left (CV Kind
KUnbounded (CInteger Integer
val))) -> Bool -> SVal
svBool (Integer
val Integer -> Integer -> Integer
forall {p}. Integral p => p -> p -> p
`mod` Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
              SVal
_                                                     -> Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
c
  where c :: State -> IO SV
c State
st = do sva <- State -> SVal -> IO SV
svToSV State
st SVal
v
                  newExpr st KBool (SBVApp (Divides n) [sva])

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

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

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

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

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

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

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

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

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

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

-- | Implication. Only for booleans.
svImplies :: SVal -> SVal -> SVal
svImplies :: SVal -> SVal -> SVal
svImplies SVal
a SVal
b
  | (SVal -> Bool) -> [SVal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\SVal
x -> SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KBool) [SVal
a, SVal
b] = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.svImplies: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SVal, Kind, SVal, Kind) -> String
forall a. Show a => a -> String
show (SVal
a, SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
a, SVal
b, SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
b)
  | SVal -> Bool
isConcreteZero SVal
a                     = SVal
svTrue  -- F -> _ = T
  |                     SVal -> Bool
isConcreteOne  SVal
b = SVal
svTrue  -- _ -> T = T
  | SVal -> Bool
isConcreteOne  SVal
a Bool -> Bool -> Bool
&& SVal -> Bool
isConcreteZero SVal
b = SVal
svFalse -- T -> F = F
  | SVal -> Bool
isConcreteOne  SVal
a Bool -> Bool -> Bool
&& SVal -> Bool
isConcreteOne  SVal
b = SVal
svTrue  -- T -> T = T
  | Bool
True                                 = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
c
  where c :: State -> IO SV
c State
st = do sva <- State -> SVal -> IO SV
svToSV State
st SVal
a
                  svb <- svToSV st b
                  -- One final optimization, equal args is just True!
                  if sva == svb
                     then pure trueSV
                     else newExpr st KBool (SBVApp Implies [sva, svb])

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

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

        getFP :: SVal -> Maybe FP
getFP (SVal Kind
_ (Left (CV Kind
_ (CFP FP
f))))    = FP -> Maybe FP
forall a. a -> Maybe a
Just FP
f
        getFP SVal
_                                 = Maybe FP
forall a. Maybe a
Nothing

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

-- Comparisons have to be careful in making sure we don't rely on CVal ord/eq instance.
compareSV :: Op -> SVal -> SVal -> SVal
compareSV :: Op -> SVal -> SVal -> SVal
compareSV Op
op SVal
x SVal
y
  -- Make sure we don't get anything we can't handle or expect
  | Op
op Op -> [Op] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Op
Equal, Op
NotEqual, Op
LessThan, Op
GreaterThan, Op
LessEq, Op
GreaterEq] = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to compareSV: "              String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, SVal, SVal) -> String
forall a. Show a => a -> String
show (Op
op, SVal
x, SVal
y)
  | Kind
kx Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
ky                                                                 = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"Mismatched kinds in call to compareSV:"      String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, SVal, Kind, Kind) -> String
forall a. Show a => a -> String
show (Op
op, SVal
x, SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
x, SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
y)
  | (Kind -> Bool
forall a. HasKind a => a -> Bool
isSet Kind
kx Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isArray Kind
ky) Bool -> Bool -> Bool
&& Op
op Op -> [Op] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Op
Equal, Op
NotEqual]               = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"Unexpected Set/Array not-equal comparison: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, SVal, Kind) -> String
forall a. Show a => a -> String
show (Op
op, SVal
x, Kind
k)

  -- Boolean equality optimizations
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
Equal,    SVal Kind
_ (Left CV
xv) <- SVal
x, CV
xv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
trueCV  = SVal
y         -- true  .== y     --> y
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
Equal,    SVal Kind
_ (Left CV
yv) <- SVal
y, CV
yv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
trueCV  = SVal
x         -- x     .== true  --> x
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
Equal,    SVal Kind
_ (Left CV
xv) <- SVal
x, CV
xv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
falseCV = SVal -> SVal
svNot SVal
y   -- false .== y     --> svNot y
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
Equal,    SVal Kind
_ (Left CV
yv) <- SVal
y, CV
yv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
falseCV = SVal -> SVal
svNot SVal
x   -- x     .== false --> svNot x

  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
NotEqual, SVal Kind
_ (Left CV
xv) <- SVal
x, CV
xv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
trueCV  = SVal -> SVal
svNot SVal
y   -- true  ./= y     --> svNot y
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
NotEqual, SVal Kind
_ (Left CV
yv) <- SVal
y, CV
yv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
trueCV  = SVal -> SVal
svNot SVal
x   -- x     ./= true  --> svNot x
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
NotEqual, SVal Kind
_ (Left CV
xv) <- SVal
x, CV
xv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
falseCV = SVal
y         -- false ./= y     --> y
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool, Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
NotEqual, SVal Kind
_ (Left CV
yv) <- SVal
y, CV
yv CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
== CV
falseCV = SVal
x         -- x     ./= false --> x

  -- Comparison optimizations if one operand is min/max bit-vector
  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
LessThan,    SVal -> Bool
isConcreteMax SVal
x = SVal
svFalse   -- MAX <  _
  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
LessThan,    SVal -> Bool
isConcreteMin SVal
y = SVal
svFalse   -- _   <  MIN

  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
GreaterThan, SVal -> Bool
isConcreteMin SVal
x = SVal
svFalse   -- MIN >  _
  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
GreaterThan, SVal -> Bool
isConcreteMax SVal
y = SVal
svFalse   -- _   > MAX

  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
LessEq,      SVal -> Bool
isConcreteMin SVal
x = SVal
svTrue    -- MIN <= _
  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
LessEq,      SVal -> Bool
isConcreteMax SVal
y = SVal
svTrue    -- _   <= MAX

  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
GreaterEq,   SVal -> Bool
isConcreteMax SVal
x = SVal
svTrue    -- MAX >= _
  | Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
GreaterEq,   SVal -> Bool
isConcreteMin SVal
y = SVal
svTrue    -- _   >= MIN

  -- General constant folding, but be careful not to be too smart here.
  | SVal Kind
_ (Left CV
xv) <- SVal
x, SVal Kind
_ (Left CV
yv) <- SVal
y
  = case Kind -> Op -> CVal -> CVal -> Maybe Ordering
cCompare Kind
k Op
op (CV -> CVal
cvVal CV
xv) (CV -> CVal
cvVal CV
yv) of
      Maybe Ordering
Nothing -> -- cCompare is conservative on floats. Give those one more chance, only at the top-level.
                 -- (i.e., if stored under a Maybe/Either/List etc., we'll resort to a symbolic result.)
                 case (Kind
k, CV -> CVal
cvVal CV
xv, CV -> CVal
cvVal CV
yv) of
                    (Kind
KFloat,   CFloat  Float
a, CFloat  Float
b) -> Bool -> SVal
svBool (Float
a Float -> Float -> Bool
forall a. Ord a => a -> a -> Bool
`cOp` Float
b)
                    (Kind
KDouble,  CDouble Double
a, CDouble Double
b) -> Bool -> SVal
svBool (Double
a Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
`cOp` Double
b)
                    (KFP{}  ,  CFP     FP
a, CFP     FP
b) -> Bool -> SVal
svBool (FP
a FP -> FP -> Bool
forall a. Ord a => a -> a -> Bool
`cOp` FP
b)
                    (Kind, CVal, CVal)
_                                  -> SVal
symResult
      Just Ordering
r  -> Bool -> SVal
svBool (Bool -> SVal) -> Bool -> SVal
forall a b. (a -> b) -> a -> b
$ case Op
op of
                            Op
Equal       -> Ordering
r Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
                            Op
NotEqual    -> Ordering
r Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
EQ
                            Op
LessThan    -> Ordering
r Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT
                            Op
GreaterThan -> Ordering
r Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT
                            Op
LessEq      -> Ordering
r Ordering -> [Ordering] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ordering
EQ, Ordering
LT]
                            Op
GreaterEq   -> Ordering
r Ordering -> [Ordering] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ordering
EQ, Ordering
GT]
                            Op
_           -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to compareSV: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, SVal, SVal) -> String
forall a. Show a => a -> String
show (Op
op, SVal
x, SVal
y)

   -- No constant folding opportunities, turn symbolic
   | Bool
True
   = SVal
symResult
   where kx :: Kind
kx = SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
x
         ky :: Kind
ky = SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
y
         k :: Kind
k  = Kind
kx       -- only used after we ensured kx == ky

         symResult :: SVal
symResult = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
          where res :: State -> IO SV
res State
st = do svx :: SV <- State -> SVal -> IO SV
svToSV State
st SVal
x
                            svy :: SV <- svToSV st y

                            -- We might be able to further optimize if we
                            -- know these are the same nodes, provided we
                            -- don't have a float case. (Recall that NaN doesn't
                            -- compare equal to itself, so avoid that.)
                            if svx == svy && not (isFloat k || isDouble k || isFP k)
                               then case op of
                                       Op
Equal       -> SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
trueSV
                                       Op
LessEq      -> SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
trueSV
                                       Op
GreaterEq   -> SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
trueSV
                                       Op
NotEqual    -> SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
falseSV
                                       Op
LessThan    -> SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
falseSV
                                       Op
GreaterThan -> SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
falseSV
                                       Op
_           -> String -> IO SV
forall a. HasCallStack => String -> a
error (String -> IO SV) -> String -> IO SV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to compareSV, equal SV case: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, SV) -> String
forall a. Show a => a -> String
show (Op
op, SV
svx)
                               else newExpr st KBool (SBVApp op [svx, svy])

         a
a cOp :: a -> a -> Bool
`cOp` a
b = case Op
op of
                      Op
Equal       -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
                      Op
NotEqual    -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
b
                      Op
LessThan    -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<  a
b
                      Op
GreaterThan -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>  a
b
                      Op
LessEq      -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b
                      Op
GreaterEq   -> a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
b
                      Op
_           -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to cOp: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op

-- Compare two CVals; if we can. We're being conservative here and deferring to a symbolic result if we get something complicated.
cCompare :: Kind -> Op -> CVal -> CVal -> Maybe Ordering
cCompare :: Kind -> Op -> CVal -> CVal -> Maybe Ordering
cCompare Kind
k Op
op CVal
x CVal
y =
    case (CVal
x, CVal
y) of

      -- The presence of NaN's throw this off. Why? Because @NaN `compare` x = GT@ in Haskell. But that's just the wrong thing to do here.
      -- So protect against NaN's. And a similar story for -0/0.
      (CFloat  Float
a, CFloat  Float
b) | (CVal -> Bool) -> [CVal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Kind -> CVal -> Bool
nanOrZero Kind
k) [CVal
x, CVal
y] -> Maybe Ordering
forall a. Maybe a
Nothing
                             | Bool
True                     -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Float
a Float -> Float -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Float
b

      (CDouble Double
a, CDouble Double
b) | (CVal -> Bool) -> [CVal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Kind -> CVal -> Bool
nanOrZero Kind
k) [CVal
x, CVal
y] -> Maybe Ordering
forall a. Maybe a
Nothing
                             | Bool
True                     -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Double
a Double -> Double -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Double
b

      (CFP     FP
a, CFP     FP
b) | (CVal -> Bool) -> [CVal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Kind -> CVal -> Bool
nanOrZero Kind
k) [CVal
x, CVal
y] -> Maybe Ordering
forall a. Maybe a
Nothing
                             | Bool
True                      -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ FP
a FP -> FP -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` FP
b

      -- Simple cases
      (CInteger  Integer
a, CInteger  Integer
b) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Integer
b
      (CRational Rational
a, CRational Rational
b) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Rational
a Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Rational
b
      (CChar     Char
a, CChar     Char
b) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Char
a Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Char
b
      (CString   String
a, CString   String
b) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
a String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` String
b

      -- We can handle algreal, so long as they are exact-rationals
      (CAlgReal     AlgReal
a, CAlgReal  AlgReal
b) | AlgReal -> Bool
isExactRational AlgReal
a Bool -> Bool -> Bool
&& AlgReal -> Bool
isExactRational AlgReal
b -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ AlgReal
a AlgReal -> AlgReal -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` AlgReal
b
                                    | Bool
True                                   -> Maybe Ordering
forall a. Maybe a
Nothing

      -- Structural cases
      (CMaybe       Maybe CVal
a, CMaybe    Maybe CVal
b) -> case (Maybe CVal
a, Maybe CVal
b) of
                                         (Maybe CVal
Nothing, Maybe CVal
Nothing) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ
                                         (Maybe CVal
Nothing, Just{})  -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT
                                         (Just{},  Maybe CVal
Nothing) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT
                                         (Just CVal
av, Just CVal
bv) -> case Kind
k of
                                                                 KMaybe Kind
ke -> Kind -> Op -> CVal -> CVal -> Maybe Ordering
cCompare Kind
ke Op
op CVal
av CVal
bv
                                                                 Kind
_         -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
"Unexpected kind in cCompare for maybe's: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

      (CEither      Either CVal CVal
a, CEither   Either CVal CVal
b) -> let (Kind
kl, Kind
kr) = case Kind
k of
                                                        KEither Kind
l Kind
r -> (Kind
l, Kind
r)
                                                        Kind
_           -> String -> (Kind, Kind)
forall a. HasCallStack => String -> a
error (String -> (Kind, Kind)) -> String -> (Kind, Kind)
forall a b. (a -> b) -> a -> b
$ String
"Unexpected kind in cCompare for either's: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                       in case (Either CVal CVal
a, Either CVal CVal
b) of
                                            (Left{},   Right{})  -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT
                                            (Right{},  Left{})   -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT
                                            (Left CVal
av,  Left  CVal
bv) -> Kind -> Op -> CVal -> CVal -> Maybe Ordering
cCompare Kind
kl Op
op CVal
av CVal
bv
                                            (Right CVal
av, Right CVal
bv) -> Kind -> Op -> CVal -> CVal -> Maybe Ordering
cCompare Kind
kr Op
op CVal
av CVal
bv

      -- Uninterpreted sorts use the index
      (CUserSort    (Maybe Int, String)
a, CUserSort (Maybe Int, String)
b) -> case ((Maybe Int, String)
a, (Maybe Int, String)
b) of
                                         ((Just Int
i, String
_), (Just Int
j, String
_)) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
j
                                         ((Maybe Int, String), (Maybe Int, String))
_                          -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
"cCompare: Impossible happened while trying to compare: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, (Maybe Int, String), (Maybe Int, String)) -> String
forall a. Show a => a -> String
show (Op
op, (Maybe Int, String)
a, (Maybe Int, String)
b)

      -- Lists and tuples use lexicographic ordering
      (CList        [CVal]
a, CList [CVal]
b) -> case Kind
k of
                                     KList Kind
ke -> [(Kind, CVal)] -> [(Kind, CVal)] -> Maybe Ordering
lexCmp ((CVal -> (Kind, CVal)) -> [CVal] -> [(Kind, CVal)]
forall a b. (a -> b) -> [a] -> [b]
map (Kind
ke,) [CVal]
a) ((CVal -> (Kind, CVal)) -> [CVal] -> [(Kind, CVal)]
forall a b. (a -> b) -> [a] -> [b]
map (Kind
ke,) [CVal]
b)
                                     Kind
_        -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
"cCompare: Unexpected kind in cCompare for List: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

      (CTuple       [CVal]
a, CTuple [CVal]
b) | [CVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
b -> case Kind
k of
                                                             KTuple [Kind]
ks | [Kind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
a -> [(Kind, CVal)] -> [(Kind, CVal)] -> Maybe Ordering
lexCmp ([Kind] -> [CVal] -> [(Kind, CVal)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Kind]
ks [CVal]
a) ([Kind] -> [CVal] -> [(Kind, CVal)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Kind]
ks [CVal]
b)
                                                             Kind
_                                 -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error String
"cCompare: Unexpected kind in cCompare for tuples"
                                 | Bool
True                 -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
"cCompare: Received tuples of differing size: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, Int, Int, Kind) -> String
forall a. Show a => a -> String
show (Op
op, [CVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
a, [CVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
b, Kind
k)

      -- Arrays and sets only support equality/inequality. And they have object-equality semantics. So
      -- if there are any floats or non-exact-rationals down in the index or element kinds, we bail
      (CSet RCSet CVal
a, CSet RCSet CVal
b)     | Op
op Op -> [Op] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Op
Equal, Op
NotEqual]
                           , KSet Kind
ke <- Kind
k
                           -> case Kind -> RCSet CVal -> RCSet CVal -> Maybe Bool
svSetEqual Kind
ke RCSet CVal
a RCSet CVal
b of
                                 Maybe Bool
Nothing    -> Maybe Ordering
forall a. Maybe a
Nothing  -- We don't know
                                 Just Bool
True  -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ  -- They're equal
                                 Just Bool
False -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ if Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
Equal
                                                         then Ordering
GT  -- Pick GT, So equality    test will fail
                                                         else Ordering
EQ  -- Pick EQ, So in-equality test will fail
                           | Bool
True
                           -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
"cCompare: Received unexpected set comparison: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, Kind) -> String
forall a. Show a => a -> String
show (Op
op, Kind
k)

      (CArray ArrayModel CVal CVal
a, CArray ArrayModel CVal CVal
b) | Op
op Op -> [Op] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Op
Equal, Op
NotEqual]
                           , KArray Kind
k1 Kind
k2 <- Kind
k
                           -> case Kind
-> Kind
-> ArrayModel CVal CVal
-> ArrayModel CVal CVal
-> Maybe Bool
svArrEqual Kind
k1 Kind
k2 ArrayModel CVal CVal
a ArrayModel CVal CVal
b of
                                Maybe Bool
Nothing    -> Maybe Ordering
forall a. Maybe a
Nothing  -- We don't know
                                Just Bool
True  -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ  -- They're equal
                                Just Bool
False -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ if Op
op Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
Equal
                                                        then Ordering
GT  -- Pick GT, So equality    test will fail
                                                        else Ordering
EQ  -- Pick EQ, So in-equality test will fail
                           | Bool
True
                           -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
"cCompare: Received unexpected array comparison: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, Kind) -> String
forall a. Show a => a -> String
show (Op
op, Kind
k)

      (CVal, CVal)
_ -> String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                           , String
"*** Data.SBV.cCompare: Bug in SBV: Unhandled rank in comparison fallthru"
                           , String
"***"
                           , String
"***   Ranks Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (CVal -> Int
cvRank CVal
x, CVal -> Int
cvRank CVal
y)
                           , String
"***"
                           , String
"*** Please report this as a bug!"
                           ]
  where -- lexicographic
        lexCmp :: [(Kind, CVal)] -> [(Kind, CVal)] -> Maybe Ordering
        lexCmp :: [(Kind, CVal)] -> [(Kind, CVal)] -> Maybe Ordering
lexCmp []     []     = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ
        lexCmp []     ((Kind, CVal)
_:[(Kind, CVal)]
_)  = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT
        lexCmp ((Kind, CVal)
_:[(Kind, CVal)]
_)  []     = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT
        lexCmp ((Kind
k1, CVal
a):[(Kind, CVal)]
as) ((Kind
k2, CVal
b):[(Kind, CVal)]
bs)
          | Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2
          = case Kind -> Op -> CVal -> CVal -> Maybe Ordering
cCompare Kind
k1 Op
op CVal
a CVal
b of
              Just Ordering
EQ -> [(Kind, CVal)]
as [(Kind, CVal)] -> [(Kind, CVal)] -> Maybe Ordering
`lexCmp` [(Kind, CVal)]
bs
              Maybe Ordering
other   -> Maybe Ordering
other
          | Bool
True
          = String -> Maybe Ordering
forall a. HasCallStack => String -> a
error (String -> Maybe Ordering) -> String -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ String
"Mismatching kinds in lexicographic comparison: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> String
forall a. Show a => a -> String
show (Kind
k1, Kind
k2)

        nanOrZero :: Kind -> CVal -> Bool
nanOrZero Kind
KFloat      (CFloat  Float
v) = Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
v Bool -> Bool -> Bool
|| Float
v Float -> Float -> Bool
forall a. Eq a => a -> a -> Bool
== Float
0
        nanOrZero Kind
KDouble     (CDouble Double
v) = Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
v Bool -> Bool -> Bool
|| Double
v Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
0
        nanOrZero (KFP Int
eb Int
sb) (CFP     FP
v) = FP -> Bool
forall a. RealFloat a => a -> Bool
isNaN FP
v Bool -> Bool -> Bool
|| FP
v FP -> FP -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Int -> Integer -> FP
fpFromInteger Int
eb Int
sb Integer
0
        nanOrZero Kind
knd         CVal
_           = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Unexpected arguments to nanOrZero: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
knd

        -- | Set equality. We return Nothing if the result is too complicated for us to concretely calculate.
        -- Why? Because the Eq instance of CVal is a bit iffy; it's designed to work as an index into maps, not as
        -- a means of checking this sort of equality
        svSetEqual :: Kind -> RCSet CVal -> RCSet CVal -> Maybe Bool
        svSetEqual :: Kind -> RCSet CVal -> RCSet CVal -> Maybe Bool
svSetEqual Kind
ek RCSet CVal
sa RCSet CVal
sb
          | Kind -> Bool
eqCheckIsObjectEq Kind
ek, RegularSet Set CVal
a    <- RCSet CVal
sa, RegularSet Set CVal
b    <- RCSet CVal
sb = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Set CVal
a Set CVal -> Set CVal -> Bool
forall a. Eq a => a -> a -> Bool
== Set CVal
b
          | Kind -> Bool
eqCheckIsObjectEq Kind
ek, ComplementSet Set CVal
a <- RCSet CVal
sa, ComplementSet Set CVal
b <- RCSet CVal
sb = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Set CVal
a Set CVal -> Set CVal -> Bool
forall a. Eq a => a -> a -> Bool
== Set CVal
b
          | Bool
True                                                               = Maybe Bool
forall a. Maybe a
Nothing

        -- | Array equality. See above comments.
        svArrEqual :: Kind -> Kind -> ArrayModel CVal CVal -> ArrayModel CVal CVal -> Maybe Bool
        svArrEqual :: Kind
-> Kind
-> ArrayModel CVal CVal
-> ArrayModel CVal CVal
-> Maybe Bool
svArrEqual Kind
k1 Kind
k2 (ArrayModel [(CVal, CVal)]
asc1 CVal
def1) (ArrayModel [(CVal, CVal)]
asc2 CVal
def2)
         | Bool -> Bool
not ((Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Kind -> Bool
eqCheckIsObjectEq [Kind
k1, Kind
k2])
         = Maybe Bool
forall a. Maybe a
Nothing
         | Bool
True
         = let -- Use of lookup is safe here, because we already made sure equality is *not* problematic above
               keysMatch :: Bool
keysMatch = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [CVal
key CVal -> [(CVal, CVal)] -> Maybe CVal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(CVal, CVal)]
asc1 Maybe CVal -> Maybe CVal -> Bool
forall a. Eq a => a -> a -> Bool
== CVal
key CVal -> [(CVal, CVal)] -> Maybe CVal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(CVal, CVal)]
asc2 | CVal
key <- [CVal] -> [CVal]
forall a. Eq a => [a] -> [a]
nub ([CVal] -> [CVal]
forall a. Ord a => [a] -> [a]
sort (((CVal, CVal) -> CVal) -> [(CVal, CVal)] -> [CVal]
forall a b. (a -> b) -> [a] -> [b]
map (CVal, CVal) -> CVal
forall a b. (a, b) -> a
fst ([(CVal, CVal)]
asc1 [(CVal, CVal)] -> [(CVal, CVal)] -> [(CVal, CVal)]
forall a. [a] -> [a] -> [a]
++ [(CVal, CVal)]
asc2)))]
               defsMatch :: Bool
defsMatch = CVal
def1 CVal -> CVal -> Bool
forall a. Eq a => a -> a -> Bool
== CVal
def2

               -- Check if keys cover everything. Clearly, we can't do this for all kinds; but only finite ones
               -- For the time being, we're retricting ourselves to bool only. Might want to extend this later.
               complete :: Bool
complete  = case Kind
k1 of
                             Kind
KBool -> let bools :: [CVal]
bools       = (CV -> CVal) -> [CV] -> [CVal]
forall a b. (a -> b) -> [a] -> [b]
map CV -> CVal
cvVal [CV
falseCV, CV
trueCV]
                                          covered :: [(CVal, b)] -> Bool
covered [(CVal, b)]
asc = (CVal -> Bool) -> [CVal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CVal -> [CVal] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((CVal, b) -> CVal) -> [(CVal, b)] -> [CVal]
forall a b. (a -> b) -> [a] -> [b]
map (CVal, b) -> CVal
forall a b. (a, b) -> a
fst [(CVal, b)]
asc) [CVal]
bools
                                      in [(CVal, CVal)] -> Bool
forall {b}. [(CVal, b)] -> Bool
covered [(CVal, CVal)]
asc1 Bool -> Bool -> Bool
&& [(CVal, CVal)] -> Bool
forall {b}. [(CVal, b)] -> Bool
covered [(CVal, CVal)]
asc2
                             Kind
_     -> Bool
False

           in case (Bool
keysMatch, Bool
defsMatch, Bool
complete) of
                (Bool
False, Bool
_   ,  Bool
_)    -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False -- keys mismatch. Nothing else matters.
                (Bool
True,  Bool
True,  Bool
_)    -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True  -- keys match, def matches; so all is good. Complete doesn't matter.
                (Bool
True,  Bool
False, Bool
True) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True  -- keys match, but defs don't. But we keys are complete, so def mismatch is OK
                (Bool, Bool, Bool)
_                    -> Maybe Bool
forall a. Maybe a
Nothing    -- otherwise, we don't really know. So, remain symbolic.

-- | Equality.
svEqual :: SVal -> SVal -> SVal
svEqual :: SVal -> SVal -> SVal
svEqual = Op -> SVal -> SVal -> SVal
compareSV Op
Equal

-- | Inequality.
svNotEqual :: SVal -> SVal -> SVal
svNotEqual :: SVal -> SVal -> SVal
svNotEqual = Op -> SVal -> SVal -> SVal
compareSV Op
NotEqual

-- | Less than.
svLessThan :: SVal -> SVal -> SVal
svLessThan :: SVal -> SVal -> SVal
svLessThan = Op -> SVal -> SVal -> SVal
compareSV Op
LessThan

-- | Greater than.
svGreaterThan :: SVal -> SVal -> SVal
svGreaterThan :: SVal -> SVal -> SVal
svGreaterThan = Op -> SVal -> SVal -> SVal
compareSV Op
GreaterThan

-- | Less than or equal to.
svLessEq :: SVal -> SVal -> SVal
svLessEq :: SVal -> SVal -> SVal
svLessEq = Op -> SVal -> SVal -> SVal
compareSV Op
LessEq

-- | Greater than or equal to.
svGreaterEq :: SVal -> SVal -> SVal
svGreaterEq :: SVal -> SVal -> SVal
svGreaterEq = Op -> SVal -> SVal -> SVal
compareSV Op
GreaterEq

-- | 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
forall a. String -> AlgReal -> AlgReal -> a
noReal String
".&.") Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.&.) (String -> Float -> Float -> Float
forall a. String -> Float -> Float -> a
noFloat String
".&.") (String -> Double -> Double -> Double
forall a. String -> Double -> Double -> a
noDouble String
".&.") (String -> FP -> FP -> FP
forall a. String -> FP -> FP -> a
noFP String
".&.") (String -> Rational -> Rational -> Rational
forall a. String -> Rational -> Rational -> a
noRat String
".&") SVal
x SVal
y
  where opt :: SV -> SV -> Maybe SV
opt SV
a SV
b
          | SV
a SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV Bool -> Bool -> Bool
|| SV
b SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV = SV -> Maybe SV
forall a. a -> Maybe a
Just SV
falseSV
          | SV
a SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV                  = SV -> Maybe SV
forall a. a -> Maybe a
Just SV
b
          | SV
b SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV                  = SV -> Maybe SV
forall a. a -> Maybe a
Just SV
a
          | SV
a SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
b                       = SV -> Maybe SV
forall a. a -> Maybe a
Just SV
a
          | Bool
True                         = Maybe SV
forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

-- | Join two words, by concatenating
svJoin :: SVal -> SVal -> SVal
svJoin :: SVal -> SVal -> SVal
svJoin x :: SVal
x@(SVal (KBounded Bool
s Int
i) Either CV (Cached SV)
a) y :: SVal
y@(SVal (KBounded Bool
s' Int
j) Either CV (Cached SV)
b)
  | Bool
s Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
s'
  = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"svJoin: received differently signed values: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SVal, SVal) -> String
forall a. Show a => a -> String
show (SVal
x, SVal
y)
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = SVal
y
  | Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = SVal
x
  | Left (CV Kind
_ (CInteger Integer
m)) <- Either CV (Cached SV)
a, Left (CV Kind
_ (CInteger Integer
n)) <- Either CV (Cached SV)
b
  = let val :: Integer
val
         | Bool
s -- signed, arithmetic doesn't work; blast and come back
         = let xbits :: [Bool]
xbits = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
xi | Int
xi <- [Int
0 .. Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
               ybits :: [Bool]
ybits = [Integer
n Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
yi | Int
yi <- [Int
0 .. Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
               rbits :: [(Int, Bool)]
rbits = [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([Bool]
ybits [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
xbits)
           in (Integer -> (Int, Bool) -> Integer)
-> Integer -> [(Int, Bool)] -> Integer
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Integer
acc (Int
idx, Bool
set) -> if Bool
set then Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
acc Int
idx else Integer
acc) Integer
0 [(Int, Bool)]
rbits
         | Bool
True -- unsigned, go fast
         = Integer
m Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
j Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
n
    in Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$! CV -> CV
normCV (Kind -> CVal -> CV
CV Kind
k (Integer -> CVal
CInteger Integer
val)))
  | Bool
True
  = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
z))
  where
    k :: Kind
k = Bool -> Int -> Kind
KBounded Bool
s (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)
    z :: State -> IO SV
z State
st = do xsw <- State -> SVal -> IO SV
svToSV State
st SVal
x
              ysw <- svToSV st y
              newExpr st k (SBVApp Join [xsw, ysw])
svJoin SVal
_ SVal
_ = String -> SVal
forall a. HasCallStack => String -> a
error String
"svJoin: non-bitvector type"

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

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

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

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

svExtend Bool
_ Int -> Op
_ Int
_ SVal
_ = String -> SVal
forall a. HasCallStack => String -> a
error String
"svExtend: non-bitvector type"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                adjustedShift <- if kx == ki
                                                 then return sw2
                                                 else newExpr st kx (SBVApp (KindCast ki kx) [sw2])

                                newExpr st kx (SBVApp op [sw1, adjustedShift])

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

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

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

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

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

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

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

-- | Generalization of '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 -> SVal -> SVal)
-> (SVal -> Int -> SVal)
-> (SVal -> Int -> SVal)
-> SVal
-> SVal
-> SVal
svRotate SVal -> SVal -> SVal
svShiftLeft SVal -> Int -> SVal
svRor SVal -> Int -> SVal
svRol

-- | 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 -> SVal -> SVal)
-> (SVal -> Int -> SVal)
-> (SVal -> Int -> SVal)
-> SVal
-> SVal
-> SVal
svRotate SVal -> SVal -> SVal
svShiftRight SVal -> Int -> SVal
svRol SVal -> Int -> SVal
svRor

-- | Common implementation for rotations. This is more complicated than it might first seem, since SMTLib does
-- not allow for non-constant rotation amounts, and only defines rotations for bit-vectors. In SBV, we support
-- both finite/infinite combos, and also non-constant (i.e., symbolic) rotations. Furthermore, if the rotation
-- amount is negative, then the direction of the rotation is reversed.
--
--   Case 1. Infinite x. In this case, we call unbounded-shifter, since you can't rotate an unbounded integer value.
--                       This is the Haskell semantics for rotates.
--   Case 2. Finite x.
--           Case 2.1. Infinite i, or finite i but i can contain a value > |x|. In this case, wrap-around can happen,
--                     so we reduce by the size of |x|.
--           Case 2.2. Finite i, and it can't contain a value > |x|. In this case, no reduction is needed.
svRotate :: (SVal -> SVal -> SVal) -> (SVal -> Int -> SVal) -> (SVal -> Int -> SVal) -> SVal -> SVal -> SVal
svRotate :: (SVal -> SVal -> SVal)
-> (SVal -> Int -> SVal)
-> (SVal -> Int -> SVal)
-> SVal
-> SVal
-> SVal
svRotate SVal -> SVal -> SVal
unboundedShifter SVal -> Int -> SVal
opRot SVal -> Int -> SVal
curRot SVal
x SVal
i
  | Bool -> Bool
not (SVal -> Bool
forall a. HasKind a => a -> Bool
isBounded SVal
x)
  = SVal -> SVal -> SVal
unboundedShifter SVal
x SVal
i
  | Bool
True
  = [SVal] -> SVal -> SVal -> SVal
svSelect [SVal]
table (Kind -> Integer -> SVal
svInteger (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
x) Integer
0) SVal
curRotate
 where sx :: Int
sx = SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
x
       si :: Int
si = SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
i

       -- Is it the case that this rotation can never "wrap-around?" This happens if
       -- i is bounded and the max rotation it can represent is less than the bit-size of the input
       noWrapAround :: Bool
       noWrapAround :: Bool
noWrapAround = SVal -> Bool
forall a. HasKind a => a -> Bool
isBounded SVal
i Bool -> Bool -> Bool
&& Integer
maxRotate Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
sx
         where maxRotate :: Integer
               maxRotate :: Integer
maxRotate
                 | SVal -> Bool
forall a. HasKind a => a -> Bool
hasSign SVal
i = Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
siInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                 | Bool
True      = Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
siInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1

       ifNegRotate :: SVal -> SVal -> SVal
ifNegRotate = SVal -> SVal -> SVal -> SVal
svIte (SVal -> SVal -> SVal
svLessThan SVal
i (Kind -> Integer -> SVal
svInteger (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
i) Integer
0))

       -- the lookup table has sx entries if index can wrap-around. Otherwise it is just as wide as it needs to be.
       table :: [SVal]
       table :: [SVal]
table = (Int -> SVal) -> [Int] -> [SVal]
forall a b. (a -> b) -> [a] -> [b]
map Int -> SVal
rotK [Int]
vals
         where rotK :: Int -> SVal
rotK Int
k = SVal -> SVal -> SVal
ifNegRotate (SVal
x SVal -> Int -> SVal
`opRot` Int
k) (SVal
x SVal -> Int -> SVal
`curRot` Int
k)
               vals :: [Int]
vals | Bool
noWrapAround = if SVal -> Bool
forall a. HasKind a => a -> Bool
hasSign SVal
i
                                        then -- If signed then bit (si-1) is the max abs value. (consider 3 bits, [-4..3] is the range)
                                             [Int
0 .. Int -> Int
forall a. Bits a => Int -> a
bit (Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
                                        else [Int
0 .. Int -> Int
forall a. Bits a => Int -> a
bit Int
si  Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
                    | Bool
True  -- If wrap-around can happen, then compute all rotations up to |x|
                    = [Int
0 .. Int
sx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

       -- What's the current rotation amount? Here we change the type of the
       -- index to make it one bit larger if the index is signed, since otherwise
       -- we run into (-(-1)) = -1 problem. See https://github.com/LeventErkok/sbv/issues/673#issuecomment-1782296700
       -- Note that curRotate is always non-negative.
       curRotate :: SVal
       curRotate :: SVal
curRotate
         | Bool
noWrapAround = SVal -> SVal -> SVal
ifNegRotate (SVal -> SVal
svUNeg SVal
i'          ) SVal
i'
         | Bool
True         = SVal -> SVal -> SVal
ifNegRotate (SVal -> SVal
svUNeg SVal
i' SVal -> SVal -> SVal
`svRem` SVal
n) (SVal
i' SVal -> SVal -> SVal
`svRem` SVal
n)

         where i' :: SVal
i' | SVal -> Bool
forall a. HasKind a => a -> Bool
hasSign SVal
i Bool -> Bool -> Bool
&& SVal -> Bool
forall a. HasKind a => a -> Bool
isBounded SVal
i = SVal -> SVal
toWord (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svAbs (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
enlarge SVal
i
                  | Bool
True                     = SVal
i

               -- Make sure sx can fit into this many bits
               si' :: Int
si' = (Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int -> Int
bitsNeeded Int
sx

               enlarge :: SVal -> SVal
enlarge
                 | SVal -> Bool
forall a. HasKind a => a -> Bool
isBounded SVal
i = Kind -> SVal -> SVal
svFromIntegral (Bool -> Int -> Kind
KBounded Bool
True  Int
si')  -- Increase bit size
                 | Bool
True        = SVal -> SVal
forall a. a -> a
id
               toWord :: SVal -> SVal
toWord
                 | SVal -> Bool
forall a. HasKind a => a -> Bool
isBounded SVal
i = Kind -> SVal -> SVal
svFromIntegral (Bool -> Int -> Kind
KBounded Bool
False Int
si')  -- Treat as word, after call to svAbs above
                 | Bool
True        = SVal -> SVal
forall a. a -> a
id

               n :: SVal
n = Kind -> Integer -> SVal
svInteger (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
i') (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
sx)

               bitsNeeded :: Int -> Int
               bitsNeeded :: Int -> Int
bitsNeeded = Int -> Int -> Int
forall {t} {t}. (Bits t, Num t, Num t) => t -> t -> t
go Int
0
                 where go :: t -> t -> t
go t
s t
0 = t
s
                       go t
s t
v = let s' :: t
s' = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ t
1 in t
s' t -> t -> t
forall a b. a -> b -> b
`seq` t -> t -> t
go t
s' (t
v t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)

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

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

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

liftSym1 :: (State -> Kind -> SV -> IO SV) -> (AlgReal  -> AlgReal)
                                           -> (Integer  -> Integer)
                                           -> (Float    -> Float)
                                           -> (Double   -> Double)
                                           -> (FP       -> FP)
                                           -> (Rational -> Rational)
                                           -> SVal      -> SVal
liftSym1 :: (State -> Kind -> SV -> IO SV)
-> (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (FP -> FP)
-> (Rational -> Rational)
-> SVal
-> SVal
liftSym1 State -> Kind -> SV -> IO SV
_   AlgReal -> AlgReal
opCR Integer -> Integer
opCI Float -> Float
opCF Double -> Double
opCD FP -> FP
opFP Rational -> Rational
opRA   (SVal Kind
k (Left CV
a)) = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (CV -> Either CV (Cached SV)) -> CV -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left  (CV -> SVal) -> CV -> SVal
forall a b. (a -> b) -> a -> b
$! (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (FP -> FP)
-> (Rational -> Rational)
-> CV
-> CV
mapCV AlgReal -> AlgReal
opCR Integer -> Integer
opCI Float -> Float
opCF Double -> Double
opCD FP -> FP
opFP Rational -> Rational
opRA CV
a
liftSym1 State -> Kind -> SV -> IO SV
opS AlgReal -> AlgReal
_    Integer -> Integer
_    Float -> Float
_    Double -> Double
_    FP -> FP
_    Rational -> Rational
_    a :: SVal
a@(SVal Kind
k Either CV (Cached SV)
_)        = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
c
   where c :: State -> IO SV
c State
st = do sva <- State -> SVal -> IO SV
svToSV State
st SVal
a
                   opS st k sva

{- A note on constant folding.

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

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

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

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

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

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


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

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

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

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

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

liftSym2 :: (State -> Kind -> SV -> SV -> IO SV)
         -> [CV       -> CV      -> Bool]
         -> (AlgReal  -> AlgReal -> AlgReal)
         -> (Integer  -> Integer -> Integer)
         -> (Float    -> Float   -> Float)
         -> (Double   -> Double  -> Double)
         -> (FP       -> FP      -> FP)
         -> (Rational -> Rational-> Rational)
         -> SVal      -> SVal    -> SVal
liftSym2 :: (State -> Kind -> SV -> SV -> IO SV)
-> [CV -> CV -> Bool]
-> (AlgReal -> AlgReal -> AlgReal)
-> (Integer -> Integer -> Integer)
-> (Float -> Float -> Float)
-> (Double -> Double -> Double)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> SVal
-> SVal
-> SVal
liftSym2 State -> Kind -> SV -> SV -> IO SV
_   [CV -> CV -> Bool]
okCV AlgReal -> AlgReal -> AlgReal
opCR Integer -> Integer -> Integer
opCI Float -> Float -> Float
opCF Double -> Double -> Double
opCD FP -> FP -> FP
opFP Rational -> Rational -> Rational
opRA (SVal Kind
k (Left CV
a)) (SVal Kind
_ (Left CV
b)) | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [CV -> CV -> Bool
f CV
a CV
b | CV -> CV -> Bool
f <- [CV -> CV -> Bool]
okCV] = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (CV -> Either CV (Cached SV)) -> CV -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left  (CV -> SVal) -> CV -> SVal
forall a b. (a -> b) -> a -> b
$! (AlgReal -> AlgReal -> AlgReal)
-> (Integer -> Integer -> Integer)
-> (Float -> Float -> Float)
-> (Double -> Double -> Double)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> 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 CV
a CV
b
liftSym2 State -> Kind -> SV -> SV -> IO SV
opS [CV -> CV -> Bool]
_    AlgReal -> AlgReal -> AlgReal
_    Integer -> Integer -> Integer
_    Float -> Float -> Float
_    Double -> Double -> Double
_    FP -> FP -> FP
_  Rational -> Rational -> Rational
_      a :: SVal
a@(SVal Kind
k Either CV (Cached SV)
_)      SVal
b                                           = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$  (State -> Kind -> SV -> SV -> IO SV)
-> Kind -> SVal -> SVal -> Cached SV
liftSV2 State -> Kind -> SV -> SV -> IO SV
opS Kind
k SVal
a SVal
b

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

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

mkSymOp1SC :: (SV -> Maybe SV) -> Op -> State -> Kind -> SV -> IO SV
mkSymOp1SC :: (SV -> Maybe SV) -> Op -> State -> Kind -> SV -> IO SV
mkSymOp1SC SV -> Maybe SV
shortCut Op
op State
st Kind
k SV
a = IO SV -> (SV -> IO SV) -> Maybe SV -> IO SV
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp Op
op [SV
a])) SV -> IO SV
forall a. a -> IO 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 (Maybe SV -> SV -> Maybe SV
forall a b. a -> b -> a
const Maybe SV
forall a. Maybe a
Nothing)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                        walk []                  = SVal
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)

                    svToSV st $ walk $ zipWith chkElt [1..] ks

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

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

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

                             br1 <- svToSV st brNothing
                             br2 <- svToSV st justRes

                             -- Do we have a value?
                             noVal <- newExpr st KBool $ SBVApp (MaybeIs ka False) [sv]
                             newExpr st KBool $ SBVApp Ite [noVal, br1, br2]

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

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

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

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

                            br1 <- svToSV st leftRes
                            br2 <- svToSV st rightRes

                            --  Which branch are we in? Return the appropriate value:
                            onLeft <- newExpr st KBool $ SBVApp (EitherIs ka kb False) [abv]
                            newExpr st KBool $ SBVApp Ite [onLeft, br1, br2]

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

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

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

{- HLint ignore svIte     "Eta reduce"         -}
{- HLint ignore svLazyIte "Eta reduce"         -}
{- HLint ignore module    "Reduce duplication" -}