module Data.SBV.BitVectors.Model (
Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..)
, bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE
, lsb, msb, SBVUF, sbvUFName, genFree, genFree_
)
where
import Data.Array (Array, Ix, listArray, elems, bounds, rangeSize)
import Data.Bits (Bits(..))
import Data.Int (Int8, Int16, Int32, Int64)
import Data.List (genericLength, genericIndex, genericSplitAt, unzip4, unzip5, unzip6, unzip7)
import Data.Word (Word8, Word16, Word32, Word64)
import Test.QuickCheck (Arbitrary(..))
import Data.SBV.BitVectors.Data
import Data.SBV.Utils.Boolean
liftSym1 :: (State -> (Bool, Size) -> SW -> IO SW) ->
(Integer -> Integer) -> SBV b -> SBV b
liftSym1 _ opC (SBV sgnsz (Left a)) = SBV sgnsz $ Left $ mapCW opC a
liftSym1 opS _ a@(SBV sgnsz _) = SBV sgnsz $ Right $ cache c
where c st = do swa <- sbvToSW st a
opS st sgnsz swa
liftSym2 :: (State -> (Bool, Size) -> SW -> SW -> IO SW) ->
(Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b
liftSym2 _ opC (SBV sgnsz (Left a)) (SBV _ (Left b)) = SBV sgnsz $ Left $ mapCW2 opC a b
liftSym2 opS _ a@(SBV sgnsz _) b = SBV sgnsz $ Right $ cache c
where c st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
opS st sgnsz sw1 sw2
liftSym2B :: (State -> (Bool, Size) -> SW -> SW -> IO SW)
-> (Integer -> Integer -> Bool)
-> SBV b -> SBV b -> SBool
liftSym2B _ opC (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opC a b)
liftSym2B opS _ a b = SBV (False, 1) $ Right $ cache c
where c st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
opS st (False, 1) sw1 sw2
liftSym1Bool :: (State -> (Bool, Size) -> SW -> IO SW)
-> (Bool -> Bool)
-> SBool -> SBool
liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a
liftSym1Bool opS _ a = SBV (False, 1) $ Right $ cache c
where c st = do sw <- sbvToSW st a
opS st (False, 1) sw
liftSym2Bool :: (State -> (Bool, Size) -> SW -> SW -> IO SW)
-> (Bool -> Bool -> Bool)
-> SBool -> SBool -> SBool
liftSym2Bool _ opC (SBV _ (Left a)) (SBV _ (Left b)) = literal (cwToBool a `opC` cwToBool b)
liftSym2Bool opS _ a b = SBV (False, 1) $ Right $ cache c
where c st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
opS st (False, 1) sw1 sw2
mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> (Bool, Size) -> SW -> SW -> IO SW
mkSymOpSC shortCut op st sgnsz a b = maybe (newExpr st sgnsz (SBVApp op [a, b])) return (shortCut a b)
mkSymOp :: Op -> State -> (Bool, Size) -> SW -> SW -> IO SW
mkSymOp = mkSymOpSC (const (const Nothing))
mkSymOp1SC :: (SW -> Maybe SW) -> Op -> State -> (Bool, Size) -> SW -> IO SW
mkSymOp1SC shortCut op st sgnsz a = maybe (newExpr st sgnsz (SBVApp op [a])) return (shortCut a)
mkSymOp1 :: Op -> State -> (Bool, Size) -> SW -> IO SW
mkSymOp1 = mkSymOp1SC (const Nothing)
genFree :: (Bool, Size) -> String -> Symbolic (SBV a)
genFree s = mkSymSBV s . Just
genFree_ :: (Bool, Size) -> Symbolic (SBV a)
genFree_ s = mkSymSBV s Nothing
genLiteral :: Integral a => (Bool,Size) -> a -> SBV b
genLiteral s = SBV s . Left . mkConstCW s
genFromCW :: Integral a => CW -> a
genFromCW x = fromInteger (cwVal x)
instance SymWord Bool where
free = genFree (False, 1)
free_ = genFree_ (False, 1)
literal x = genLiteral (False, 1) (if x then (1::Integer) else 0)
fromCW = cwToBool
instance SymWord Word8 where
free = genFree (False, 8)
free_ = genFree_ (False, 8)
literal = genLiteral (False, 8)
fromCW = genFromCW
instance SymWord Int8 where
free = genFree (True, 8)
free_ = genFree_ (True, 8)
literal = genLiteral (True, 8)
fromCW = genFromCW
instance SymWord Word16 where
free = genFree (False, 16)
free_ = genFree_ (False, 16)
literal = genLiteral (False, 16)
fromCW = genFromCW
instance SymWord Int16 where
free = genFree (True, 16)
free_ = genFree_ (True, 16)
literal = genLiteral (True, 16)
fromCW = genFromCW
instance SymWord Word32 where
free = genFree (False, 32)
free_ = genFree_ (False, 32)
literal = genLiteral (False, 32)
fromCW = genFromCW
instance SymWord Int32 where
free = genFree (True, 32)
free_ = genFree_ (True, 32)
literal = genLiteral (True, 32)
fromCW = genFromCW
instance SymWord Word64 where
free = genFree (False, 64)
free_ = genFree_ (False, 64)
literal = genLiteral (False, 64)
fromCW = genFromCW
instance SymWord Int64 where
free = genFree (True, 64)
free_ = genFree_ (True, 64)
literal = genLiteral (True, 64)
fromCW = genFromCW
infix 4 .==, ./=
class EqSymbolic a where
(.==), (./=) :: a -> a -> SBool
x ./= y = bnot (x .== y)
infix 4 .<, .<=, .>, .>=
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
(.<), (.<=), (.>), (.>=) :: a -> a -> SBool
smin, smax :: a -> a -> a
a .<= b = a .< b ||| a .== b
a .> b = b .< a
a .>= b = b .<= a
a `smin` b = ite (a .<= b) a b
a `smax` b = ite (a .<= b) b a
instance EqSymbolic (SBV a) where
(.==) = liftSym2B (mkSymOpSC opt Equal) (==)
where opt x y = if x == y then Just trueSW else Nothing
(./=) = liftSym2B (mkSymOpSC opt NotEqual) (/=)
where opt x y = if x == y then Just falseSW else Nothing
instance SymWord a => OrdSymbolic (SBV a) where
(.<) = liftSym2B (mkSymOp LessThan) (<)
(.<=) = liftSym2B (mkSymOp LessEq) (<=)
(.>) = liftSym2B (mkSymOp GreaterThan) (>)
(.>=) = liftSym2B (mkSymOp GreaterEq) (>=)
instance EqSymbolic Bool where
x .== y = if x == y then true else false
instance EqSymbolic a => EqSymbolic [a] where
[] .== [] = true
(x:xs) .== (y:ys) = x .== y &&& xs .== ys
_ .== _ = false
instance OrdSymbolic a => OrdSymbolic [a] where
[] .< [] = false
[] .< _ = true
_ .< [] = false
(x:xs) .< (y:ys) = x .< y ||| (x .== y &&& xs .< ys)
instance EqSymbolic a => EqSymbolic (Maybe a) where
Nothing .== Nothing = true
Just a .== Just b = a .== b
_ .== _ = false
instance (OrdSymbolic a) => OrdSymbolic (Maybe a) where
Nothing .< Nothing = false
Nothing .< _ = true
Just _ .< Nothing = false
Just a .< Just b = a .< b
instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) where
Left a .== Left b = a .== b
Right a .== Right b = a .== b
_ .== _ = false
instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) where
Left a .< Left b = a .< b
Left _ .< Right _ = true
Right _ .< Left _ = false
Right a .< Right b = a .< b
instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) where
(a0, b0) .== (a1, b1) = a0 .== a1 &&& b0 .== b1
instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) where
(a0, b0) .< (a1, b1) = a0 .< a1 ||| (a0 .== a1 &&& b0 .< b1)
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) where
(a0, b0, c0) .== (a1, b1, c1) = (a0, b0) .== (a1, b1) &&& c0 .== c1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) where
(a0, b0, c0) .< (a1, b1, c1) = (a0, b0) .< (a1, b1) ||| ((a0, b0) .== (a1, b1) &&& c0 .< c1)
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) where
(a0, b0, c0, d0) .== (a1, b1, c1, d1) = (a0, b0, c0) .== (a1, b1, c1) &&& d0 .== d1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) where
(a0, b0, c0, d0) .< (a1, b1, c1, d1) = (a0, b0, c0) .< (a1, b1, c1) ||| ((a0, b0, c0) .== (a1, b1, c1) &&& d0 .< d1)
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) where
(a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .== (a1, b1, c1, d1) &&& e0 .== e1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) where
(a0, b0, c0, d0, e0) .< (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .< (a1, b1, c1, d1) ||| ((a0, b0, c0, d0) .== (a1, b1, c1, d1) &&& e0 .< e1)
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) where
(a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) &&& f0 .== f1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) where
(a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .< (a1, b1, c1, d1, e1)
||| ((a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) &&& f0 .< f1)
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) where
(a0, b0, c0, d0, e0, f0, g0) .== (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) &&& g0 .== g1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) where
(a0, b0, c0, d0, e0, f0, g0) .< (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1)
||| ((a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) &&& g0 .< g1)
instance Boolean SBool where
true = literal True
false = literal False
bnot = liftSym1Bool (mkSymOp1 Not) not
(&&&) = liftSym2Bool (mkSymOpSC opt And) (&&)
where opt x y
| x == falseSW || y == falseSW = Just falseSW
| x == trueSW = Just y
| y == trueSW = Just x
| True = Nothing
(|||) = liftSym2Bool (mkSymOpSC opt Or) (||)
where opt x y
| x == trueSW || y == trueSW = Just trueSW
| x == falseSW = Just y
| y == falseSW = Just x
| True = Nothing
(<+>) = liftSym2Bool (mkSymOpSC opt XOr) (<+>)
where opt x y
| x == y = Just falseSW
| True = Nothing
allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBool
allDifferent (x:xs@(_:_)) = bAll ((./=) x) xs &&& allDifferent xs
allDifferent _ = true
allEqual :: (Eq a, SymWord a) => [SBV a] -> SBool
allEqual (x:xs@(_:_)) = bAll ((.==) x) xs
allEqual _ = true
oneIf :: (Num a, SymWord a) => SBool -> SBV a
oneIf t = ite t 1 0
instance (Ord a, Num a, SymWord a) => Num (SBV a) where
fromInteger = literal . fromIntegral
x + y
| x `isConcretely` (== 0) = y
| y `isConcretely` (== 0) = x
| True = liftSym2 (mkSymOp Plus) (+) x y
x * y
| x `isConcretely` (== 0) = 0
| y `isConcretely` (== 0) = 0
| x `isConcretely` (== 1) = y
| y `isConcretely` (== 1) = x
| True = liftSym2 (mkSymOp Times) (*) x y
x y
| y `isConcretely` (== 0) = x
| True = liftSym2 (mkSymOp Minus) () x y
abs a
| hasSign a = ite (a .< 0) (a) a
| True = a
signum a
| hasSign a = ite (a .< 0) (1) (ite (a .== 0) 0 1)
| True = oneIf (a ./= 0)
instance (Bits a, SymWord a) => Bits (SBV a) where
(.&.) = liftSym2 (mkSymOp And) (.&.)
(.|.) = liftSym2 (mkSymOp Or) (.|.)
xor = liftSym2 (mkSymOp XOr) xor
complement = liftSym1 (mkSymOp1 Not) complement
bitSize (SBV (_ ,s) _) = s
isSigned (SBV (b, _) _) = b
shiftL x y
| y < 0 = shiftR x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Shl y)) (`shiftL` y) x
shiftR x y
| y < 0 = shiftL x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Shr y)) (`shiftR` y) x
rotateL x y
| y < 0 = rotateR x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Rol y)) (`rotateL` y) x
rotateR x y
| y < 0 = rotateL x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Ror y)) (`rotateR` y) x
bitValue :: (Bits a, SymWord a) => SBV a -> Int -> SBool
bitValue x i = (x .&. bit i) ./= 0
setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a
setBitTo x i b = ite b (setBit x i) (clearBit x i)
blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]
blastLE x = map (bitValue x) [0 .. (sizeOf x)1]
blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]
blastBE = reverse . blastLE
lsb :: (Bits a, SymWord a) => SBV a -> SBool
lsb x = bitValue x 0
msb :: (Bits a, SymWord a) => SBV a -> SBool
msb x = bitValue x ((sizeOf x) 1)
class BVDivisible a where
bvQuotRem :: a -> a -> (a, a)
instance BVDivisible Word64 where
bvQuotRem x 0 = (0, x)
bvQuotRem x y = x `quotRem` y
instance BVDivisible Word32 where
bvQuotRem x 0 = (0, x)
bvQuotRem x y = x `quotRem` y
instance BVDivisible Word16 where
bvQuotRem x 0 = (0, x)
bvQuotRem x y = x `quotRem` y
instance BVDivisible Word8 where
bvQuotRem x 0 = (0, x)
bvQuotRem x y = x `quotRem` y
instance BVDivisible Integer where
bvQuotRem x 0 = (0, x)
bvQuotRem x y = x `quotRem` y
instance BVDivisible CW where
bvQuotRem x y
| cwSameType x y = let (r1, r2) = bvQuotRem (cwVal x) (cwVal y)
in (x { cwVal = r1 }, y { cwVal = r2 })
bvQuotRem x y = error $ "SBV.liftQRem: impossible, unexpected args received: " ++ show (x, y)
instance BVDivisible SWord64 where
bvQuotRem = liftQRem
instance BVDivisible SWord32 where
bvQuotRem = liftQRem
instance BVDivisible SWord16 where
bvQuotRem = liftQRem
instance BVDivisible SWord8 where
bvQuotRem = liftQRem
liftQRem :: (SymWord a, Num a, BVDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)
liftQRem x y = ite (y .== 0) (0, x) (qr x y)
where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = bvQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r))
qr a@(SBV sgnsz _) b = (SBV sgnsz (Right (cache (mk Quot))), SBV sgnsz (Right (cache (mk Rem))))
where mk o st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
mkSymOp o st sgnsz sw1 sw2
instance (SymWord b, Arbitrary b) => Arbitrary (SFunArray a b) where
arbitrary = arbitrary >>= \r -> return $ SFunArray (const r)
instance (SymWord a, Arbitrary a) => Arbitrary (SBV a) where
arbitrary = arbitrary >>= return . literal
class Mergeable a where
symbolicMerge :: SBool -> a -> a -> a
ite :: SBool -> a -> a -> a
select :: (Bits b, SymWord b, Integral b) => [a] -> a -> SBV b -> a
ite s a b
| Just t <- unliteral s = if t then a else b
| True = symbolicMerge s a b
select [] err _ = err
select xs err ind
| hasSign ind = ite (ind .< 0) err $ result
| True = result
where result = go xs $ reverse (zip [(0::Integer)..] bits)
bits = map (ind `bitValue`) [0 .. bitSize ind 1]
go [] _ = err
go (x:_) [] = x
go elts ((n, b):nbs) = let (ys, zs) = genericSplitAt ((2::Integer) ^ n) elts
in ite b (go zs nbs) (go ys nbs)
instance SymWord a => Mergeable (SBV a) where
symbolicMerge t a b
| Just c1 <- unliteral a, Just c2 <- unliteral b, c1 == c2
= a
| True
= SBV sgnsz $ Right $ cache c
where sgnsz = (hasSign a, sizeOf a)
c st = do swt <- sbvToSW st t
case () of
() | swt == trueSW -> sbvToSW st a
() | swt == falseSW -> sbvToSW st b
() -> do swa <- sbvToSW st a
swb <- sbvToSW st b
if swa == swb
then return swa
else newExpr st sgnsz (SBVApp Ite [swt, swa, swb])
select xs err ind
| Just i <- unliteral ind
= let i' :: Integer
i' = fromIntegral i
in if i' < 0 || i' >= genericLength xs then err else genericIndex xs i'
select [] err _ = err
select xs err ind = SBV sgnszElt $ Right $ cache r
where sgnszInd = (hasSign ind, sizeOf ind)
sgnszElt = (hasSign err, sizeOf err)
r st = do sws <- mapM (sbvToSW st) xs
swe <- sbvToSW st err
if all (== swe) sws
then return swe
else do idx <- getTableIndex st sgnszInd sgnszElt sws
swi <- sbvToSW st ind
let len = length xs
newExpr st sgnszElt (SBVApp (LkUp (idx, sgnszInd, sgnszElt, len) swi swe) [])
instance Mergeable () where
symbolicMerge _ _ _ = ()
select _ _ _ = ()
instance Mergeable a => Mergeable [a] where
symbolicMerge t xs ys
| lxs == lys = zipWith (symbolicMerge t) xs ys
| True = error $ "SBV.Mergeable.List: No least-upper-bound for lists of differing size " ++ show (lxs, lys)
where (lxs, lys) = (length xs, length ys)
instance Mergeable a => Mergeable (Maybe a) where
symbolicMerge _ Nothing Nothing = Nothing
symbolicMerge t (Just a) (Just b) = Just $ symbolicMerge t a b
symbolicMerge _ a b = error $ "SBV.Mergeable.Maybe: No least-upper-bound for " ++ show (k a, k b)
where k Nothing = "Nothing"
k _ = "Just"
instance (Mergeable a, Mergeable b) => Mergeable (Either a b) where
symbolicMerge t (Left a) (Left b) = Left $ symbolicMerge t a b
symbolicMerge t (Right a) (Right b) = Right $ symbolicMerge t a b
symbolicMerge _ a b = error $ "SBV.Mergeable.Either: No least-upper-bound for " ++ show (k a, k b)
where k (Left _) = "Left"
k (Right _) = "Right"
instance (Ix a, Mergeable b) => Mergeable (Array a b) where
symbolicMerge t a b
| ba == bb = listArray ba (zipWith (symbolicMerge t) (elems a) (elems b))
| True = error $ "SBV.Mergeable.Array: No least-upper-bound for rangeSizes" ++ show (k ba, k bb)
where [ba, bb] = map bounds [a, b]
k = rangeSize
instance Mergeable b => Mergeable (a -> b) where
symbolicMerge t f g = \x -> symbolicMerge t (f x) (g x)
select xs err ind = \x -> select (map ($ x) xs) (err x) ind
instance (Mergeable a, Mergeable b) => Mergeable (a, b) where
symbolicMerge t (i0, i1) (j0, j1) = (i i0 j0, i i1 j1)
where i a b = symbolicMerge t a b
select xs (err1, err2) ind = (select as err1 ind, select bs err2 ind)
where (as, bs) = unzip xs
instance (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) where
symbolicMerge t (i0, i1, i2) (j0, j1, j2) = (i i0 j0, i i1 j1, i i2 j2)
where i a b = symbolicMerge t a b
select xs (err1, err2, err3) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind)
where (as, bs, cs) = unzip3 xs
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) where
symbolicMerge t (i0, i1, i2, i3) (j0, j1, j2, j3) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3)
where i a b = symbolicMerge t a b
select xs (err1, err2, err3, err4) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind)
where (as, bs, cs, ds) = unzip4 xs
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) where
symbolicMerge t (i0, i1, i2, i3, i4) (j0, j1, j2, j3, j4) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4)
where i a b = symbolicMerge t a b
select xs (err1, err2, err3, err4, err5) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind)
where (as, bs, cs, ds, es) = unzip5 xs
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) where
symbolicMerge t (i0, i1, i2, i3, i4, i5) (j0, j1, j2, j3, j4, j5) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4, i i5 j5)
where i a b = symbolicMerge t a b
select xs (err1, err2, err3, err4, err5, err6) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind, select fs err6 ind)
where (as, bs, cs, ds, es, fs) = unzip6 xs
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) where
symbolicMerge t (i0, i1, i2, i3, i4, i5, i6) (j0, j1, j2, j3, j4, j5, j6) = (i i0 j0, i i1 j1, i i2 j2, i i3 j3, i i4 j4, i i5 j5, i i6 j6)
where i a b = symbolicMerge t a b
select xs (err1, err2, err3, err4, err5, err6, err7) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind, select fs err6 ind, select gs err7 ind)
where (as, bs, cs, ds, es, fs, gs) = unzip7 xs
instance (SymWord a, Bounded a) => Bounded (SBV a) where
minBound = literal minBound
maxBound = literal maxBound
instance EqSymbolic (SArray a b) where
(SArray _ a) .== (SArray _ b) = SBV (False, 1) $ Right $ cache c
where c st = do ai <- uncache a st
bi <- uncache b st
newExpr st (False, 1) (SBVApp (ArrEq ai bi) [])
instance SymWord b => Mergeable (SArray a b) where
symbolicMerge = mergeArrays
instance SymArray SFunArray where
newArray _ = newArray_
newArray_ mbiVal = return $ SFunArray $ const $ maybe (error "Reading from an uninitialized array entry") id mbiVal
readArray (SFunArray f) a = f a
resetArray (SFunArray _) a = SFunArray $ const a
writeArray (SFunArray f) a b = SFunArray (\a' -> ite (a .== a') b (f a'))
mergeArrays t (SFunArray f) (SFunArray g) = SFunArray (\x -> ite t (f x) (g x))
instance SymWord b => Mergeable (SFunArray a b) where
symbolicMerge = mergeArrays
newtype SBVUF = SBVUF String
sbvUFName :: SBVUF -> String
sbvUFName (SBVUF s) = s
mkUFName :: String -> SBVUF
mkUFName nm = SBVUF $ "uninterpreted_" ++ nm
class Uninterpreted a where
uninterpret :: String -> a
uninterpretWithHandle :: String -> (SBVUF, a)
uninterpret = snd . uninterpretWithHandle
instance HasSignAndSize a => Uninterpreted (SBV a) where
uninterpretWithHandle nm = (mkUFName nm, SBV sgnsza $ Right $ cache result)
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
result st = do newUninterpreted st nm (SBVType [sgnsza])
newExpr st sgnsza $ SBVApp (Uninterpreted nm) []
forceArg :: SW -> IO ()
forceArg (SW (b, s) n) = b `seq` s `seq` n `seq` return ()
instance (HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) where
uninterpretWithHandle nm = (mkUFName nm, f)
where f arg0 = SBV sgnsza $ Right $ cache result
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
result st = do newUninterpreted st nm (SBVType [sgnszb, sgnsza])
sw0 <- sbvToSW st arg0
mapM_ forceArg [sw0]
newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]
instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) where
uninterpretWithHandle nm = (mkUFName nm, f)
where f arg0 arg1 = SBV sgnsza $ Right $ cache result
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
result st = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza])
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
mapM_ forceArg [sw0, sw1]
newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]
instance (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where
uninterpretWithHandle nm = (mkUFName nm, f)
where f arg0 arg1 arg2 = SBV sgnsza $ Right $ cache result
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
result st = do newUninterpreted st nm (SBVType [sgnszd, sgnszc, sgnszb, sgnsza])
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
mapM_ forceArg [sw0, sw1, sw2]
newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]
instance (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
uninterpretWithHandle nm = (mkUFName nm, f)
where f arg0 arg1 arg2 arg3 = SBV sgnsza $ Right $ cache result
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
result st = do newUninterpreted st nm (SBVType [sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
sw3 <- sbvToSW st arg3
mapM_ forceArg [sw0, sw1, sw2, sw3]
newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]
instance (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
uninterpretWithHandle nm = (mkUFName nm, f)
where f arg0 arg1 arg2 arg3 arg4 = SBV sgnsza $ Right $ cache result
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
result st = do newUninterpreted st nm (SBVType [sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
sw3 <- sbvToSW st arg3
sw4 <- sbvToSW st arg4
mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]
newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]
instance (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
uninterpretWithHandle nm = (mkUFName nm, f)
where f arg0 arg1 arg2 arg3 arg4 arg5 = SBV sgnsza $ Right $ cache result
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))
result st = do newUninterpreted st nm (SBVType [sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
sw3 <- sbvToSW st arg3
sw4 <- sbvToSW st arg4
sw5 <- sbvToSW st arg5
mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]
newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]
instance (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
uninterpretWithHandle nm = (mkUFName nm, f)
where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 = SBV sgnsza $ Right $ cache result
where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))
sgnszh = (hasSign (undefined :: h), sizeOf (undefined :: h))
result st = do newUninterpreted st nm (SBVType [sgnszh, sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
sw3 <- sbvToSW st arg3
sw4 <- sbvToSW st arg4
sw5 <- sbvToSW st arg5
sw6 <- sbvToSW st arg6
mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where
uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1) -> f arg0 arg1)
instance (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where
uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2) -> f arg0 arg1 arg2)
instance (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where
uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3)
instance (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4)
instance (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5)
instance (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
=> Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6)