module Data.SBV.BitVectors.Model (
Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral
, sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight
, allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier
, lsb, msb, genVar, genVar_, forall, forall_, exists, exists_
, constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32
, sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64
, sInt64s, sInteger, sIntegers, sReal, sReals, toSReal, sFloat, sFloats, sDouble, sDoubles, slet
, fusedMA
)
where
import Control.Monad (when, liftM)
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, unzip4, unzip5, unzip6, unzip7, intercalate)
import Data.Maybe (fromMaybe)
import Data.Word (Word8, Word16, Word32, Word64)
import Test.QuickCheck (Testable(..), Arbitrary(..))
import qualified Test.QuickCheck as QC (whenFail)
import qualified Test.QuickCheck.Monadic as QC (monadicIO, run)
import System.Random
import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.Data
import Data.SBV.Utils.Boolean
noUnint :: String -> a
noUnint x = error $ "Unexpected operation called on uninterpreted value: " ++ show x
noUnint2 :: String -> String -> a
noUnint2 x y = error $ "Unexpected binary operation called on uninterpreted values: " ++ show (x, y)
liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> SBV b -> SBV b
liftSym1 _ opCR opCI opCF opCD (SBV k (Left a)) = SBV k $ Left $ mapCW opCR opCI opCF opCD noUnint a
liftSym1 opS _ _ _ _ a@(SBV k _) = SBV k $ Right $ cache c
where c st = do swa <- sbvToSW st a
opS st k swa
liftSW2 :: (State -> Kind -> SW -> SW -> IO SW) -> Kind -> SBV a -> SBV b -> Cached SW
liftSW2 opS k a b = cache c
where c st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
opS st k sw1 sw2
liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> SBV b -> SBV b -> SBV b
liftSym2 _ okCW opCR opCI opCF opCD (SBV k (Left a)) (SBV _ (Left b)) | okCW a b = SBV k $ Left $ mapCW2 opCR opCI opCF opCD noUnint2 a b
liftSym2 opS _ _ _ _ _ a@(SBV k _) b = SBV k $ Right $ liftSW2 opS k a b
liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> SBV b -> SBV b -> SBool
liftSym2B _ okCW opCR opCI opCF opCD (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI opCF opCD noUnint2 a b)
liftSym2B opS _ _ _ _ _ a b = SBV (KBounded False 1) $ Right $ liftSW2 opS (KBounded False 1) a b
liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool
liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a
liftSym1Bool opS _ a = SBV (KBounded False 1) $ Right $ cache c
where c st = do sw <- sbvToSW st a
opS st (KBounded False 1) sw
liftSym2Bool :: (State -> Kind -> 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 (KBounded False 1) $ Right $ cache c
where c st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
opS st (KBounded False 1) sw1 sw2
mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW
mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b)
mkSymOp :: Op -> State -> Kind -> SW -> SW -> IO SW
mkSymOp = mkSymOpSC (const (const Nothing))
mkSymOp1SC :: (SW -> Maybe SW) -> Op -> State -> Kind -> SW -> IO SW
mkSymOp1SC shortCut op st k a = maybe (newExpr st k (SBVApp op [a])) return (shortCut a)
mkSymOp1 :: Op -> State -> Kind -> SW -> IO SW
mkSymOp1 = mkSymOp1SC (const Nothing)
genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)
genVar q k = mkSymSBV q k . Just
genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a)
genVar_ q k = mkSymSBV q k Nothing
genLiteral :: Integral a => Kind -> a -> SBV b
genLiteral k = SBV k . Left . mkConstCW k
genFromCW :: Integral a => CW -> a
genFromCW (CW _ (CWInteger x)) = fromInteger x
genFromCW c = error $ "genFromCW: Unsupported non-integral value: " ++ show c
genMkSymVar :: (Random a, SymWord a) => Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
genMkSymVar k mbq Nothing = genVar_ mbq k
genMkSymVar k mbq (Just s) = genVar mbq k s
instance SymWord Bool where
mkSymWord = genMkSymVar (KBounded False 1)
literal x = genLiteral (KBounded False 1) (if x then (1::Integer) else 0)
fromCW = cwToBool
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Word8 where
mkSymWord = genMkSymVar (KBounded False 8)
literal = genLiteral (KBounded False 8)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int8 where
mkSymWord = genMkSymVar (KBounded True 8)
literal = genLiteral (KBounded True 8)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Word16 where
mkSymWord = genMkSymVar (KBounded False 16)
literal = genLiteral (KBounded False 16)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int16 where
mkSymWord = genMkSymVar (KBounded True 16)
literal = genLiteral (KBounded True 16)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Word32 where
mkSymWord = genMkSymVar (KBounded False 32)
literal = genLiteral (KBounded False 32)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int32 where
mkSymWord = genMkSymVar (KBounded True 32)
literal = genLiteral (KBounded True 32)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Word64 where
mkSymWord = genMkSymVar (KBounded False 64)
literal = genLiteral (KBounded False 64)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int64 where
mkSymWord = genMkSymVar (KBounded True 64)
literal = genLiteral (KBounded True 64)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Integer where
mkSymWord = genMkSymVar KUnbounded
literal = SBV KUnbounded . Left . mkConstCW KUnbounded
fromCW = genFromCW
mbMaxBound = Nothing
mbMinBound = Nothing
instance SymWord AlgReal where
mkSymWord = genMkSymVar KReal
literal = SBV KReal . Left . CW KReal . CWAlgReal
fromCW (CW _ (CWAlgReal a)) = a
fromCW c = error $ "SymWord.AlgReal: Unexpected non-real value: " ++ show c
isConcretely (SBV KReal (Left (CW KReal (CWAlgReal v)))) p
| isExactRational v = p v
isConcretely _ _ = False
mbMaxBound = Nothing
mbMinBound = Nothing
instance SymWord Float where
mkSymWord = genMkSymVar KFloat
literal = SBV KFloat . Left . CW KFloat . CWFloat
fromCW (CW _ (CWFloat a)) = a
fromCW c = error $ "SymWord.Float: Unexpected non-float value: " ++ show c
isConcretely _ _ = False
mbMaxBound = Nothing
mbMinBound = Nothing
instance SymWord Double where
mkSymWord = genMkSymVar KDouble
literal = SBV KDouble . Left . CW KDouble . CWDouble
fromCW (CW _ (CWDouble a)) = a
fromCW c = error $ "SymWord.Double: Unexpected non-double value: " ++ show c
isConcretely _ _ = False
mbMaxBound = Nothing
mbMinBound = Nothing
sBool :: String -> Symbolic SBool
sBool = symbolic
sBools :: [String] -> Symbolic [SBool]
sBools = symbolics
sWord8 :: String -> Symbolic SWord8
sWord8 = symbolic
sWord8s :: [String] -> Symbolic [SWord8]
sWord8s = symbolics
sWord16 :: String -> Symbolic SWord16
sWord16 = symbolic
sWord16s :: [String] -> Symbolic [SWord16]
sWord16s = symbolics
sWord32 :: String -> Symbolic SWord32
sWord32 = symbolic
sWord32s :: [String] -> Symbolic [SWord32]
sWord32s = symbolics
sWord64 :: String -> Symbolic SWord64
sWord64 = symbolic
sWord64s :: [String] -> Symbolic [SWord64]
sWord64s = symbolics
sInt8 :: String -> Symbolic SInt8
sInt8 = symbolic
sInt8s :: [String] -> Symbolic [SInt8]
sInt8s = symbolics
sInt16 :: String -> Symbolic SInt16
sInt16 = symbolic
sInt16s :: [String] -> Symbolic [SInt16]
sInt16s = symbolics
sInt32 :: String -> Symbolic SInt32
sInt32 = symbolic
sInt32s :: [String] -> Symbolic [SInt32]
sInt32s = symbolics
sInt64 :: String -> Symbolic SInt64
sInt64 = symbolic
sInt64s :: [String] -> Symbolic [SInt64]
sInt64s = symbolics
sInteger:: String -> Symbolic SInteger
sInteger = symbolic
sIntegers :: [String] -> Symbolic [SInteger]
sIntegers = symbolics
sReal:: String -> Symbolic SReal
sReal = symbolic
sReals :: [String] -> Symbolic [SReal]
sReals = symbolics
sFloat :: String -> Symbolic SFloat
sFloat = symbolic
sFloats :: [String] -> Symbolic [SFloat]
sFloats = symbolics
sDouble :: String -> Symbolic SDouble
sDouble = symbolic
sDoubles :: [String] -> Symbolic [SDouble]
sDoubles = symbolics
toSReal :: SInteger -> SReal
toSReal x
| Just i <- unliteral x = literal $ fromInteger i
| True = SBV KReal (Right (cache y))
where y st = do xsw <- sbvToSW st x
newExpr st KReal (SBVApp (Extract 0 0) [xsw])
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 (eqOpt trueSW) Equal) rationalCheck (==) (==) (==) (==)
(./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) rationalCheck (/=) (/=) (/=) (/=)
eqOpt :: SW -> SW -> SW -> Maybe SW
eqOpt w x y = case kindOf x of
KFloat -> Nothing
KDouble -> Nothing
_ -> if x == y then Just w else Nothing
instance SymWord a => OrdSymbolic (SBV a) where
x .< y
| Just mb <- mbMaxBound, x `isConcretely` (== mb) = false
| Just mb <- mbMinBound, y `isConcretely` (== mb) = false
| True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) (<) (<) x y
x .<= y
| Just mb <- mbMinBound, x `isConcretely` (== mb) = true
| Just mb <- mbMaxBound, y `isConcretely` (== mb) = true
| True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) (<=) (<=) x y
x .> y
| Just mb <- mbMinBound, x `isConcretely` (== mb) = false
| Just mb <- mbMaxBound, y `isConcretely` (== mb) = false
| True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) (>) (>) x y
x .>= y
| Just mb <- mbMaxBound, x `isConcretely` (== mb) = true
| Just mb <- mbMinBound, y `isConcretely` (== mb) = true
| True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) x y
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)
class (SymWord a, Num a, Bits a) => SIntegral a
instance SIntegral Word8
instance SIntegral Word16
instance SIntegral Word32
instance SIntegral Word64
instance SIntegral Int8
instance SIntegral Int16
instance SIntegral Int32
instance SIntegral Int64
instance SIntegral Integer
instance Boolean SBool where
true = literal True
false = literal False
bnot b | b `isConcretely` (== False) = true
| b `isConcretely` (== True) = false
| True = liftSym1Bool (mkSymOp1SC opt Not) not b
where opt x
| x == falseSW = Just trueSW
| x == trueSW = Just falseSW
| True = Nothing
a &&& b | a `isConcretely` (== False) || b `isConcretely` (== False) = false
| a `isConcretely` (== True) = b
| b `isConcretely` (== True) = a
| True = liftSym2Bool (mkSymOpSC opt And) (&&) a b
where opt x y
| x == falseSW || y == falseSW = Just falseSW
| x == trueSW = Just y
| y == trueSW = Just x
| True = Nothing
a ||| b | a `isConcretely` (== True) || b `isConcretely` (== True) = true
| a `isConcretely` (== False) = b
| b `isConcretely` (== False) = a
| True = liftSym2Bool (mkSymOpSC opt Or) (||) a b
where opt x y
| x == trueSW || y == trueSW = Just trueSW
| x == falseSW = Just y
| y == falseSW = Just x
| True = Nothing
a <+> b | a `isConcretely` (== False) = b
| b `isConcretely` (== False) = a
| a `isConcretely` (== True) = bnot b
| b `isConcretely` (== True) = bnot a
| True = liftSym2Bool (mkSymOpSC opt XOr) (<+>) a b
where opt x y
| x == y = Just falseSW
| x == falseSW = Just y
| y == falseSW = Just x
| True = Nothing
allDifferent :: EqSymbolic a => [a] -> SBool
allDifferent (x:xs@(_:_)) = bAll (x ./=) xs &&& allDifferent xs
allDifferent _ = true
allEqual :: EqSymbolic a => [a] -> SBool
allEqual (x:xs@(_:_)) = bAll (x .==) xs
allEqual _ = true
inRange :: OrdSymbolic a => a -> (a, a) -> SBool
inRange x (y, z) = x .>= y &&& x .<= z
sElem :: EqSymbolic a => a -> [a] -> SBool
sElem x xs = bAny (.== x) xs
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) rationalCheck (+) (+) (+) (+) x y
x * y
| x `isConcretely` (== 0) = 0
| y `isConcretely` (== 0) = 0
| x `isConcretely` (== 1) = y
| y `isConcretely` (== 1) = x
| True = liftSym2 (mkSymOp Times) rationalCheck (*) (*) (*) (*) x y
x y
| y `isConcretely` (== 0) = x
| True = liftSym2 (mkSymOp Minus) rationalCheck () () () () 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 (SymWord a, Fractional a) => Fractional (SBV a) where
fromRational = literal . fromRational
x / y = liftSym2 (mkSymOp Quot) rationalCheck (/) die (/) (/) x y
where
die = error "impossible: integer valued data found in Fractional instance"
instance (SymWord a, Fractional a, Floating a) => Floating (SBV a) where
pi = literal pi
exp = lift1FNS "exp" exp
log = lift1FNS "log" log
sqrt = lift1F sqrt smtLibSquareRoot
sin = lift1FNS "sin" sin
cos = lift1FNS "cos" cos
tan = lift1FNS "tan" tan
asin = lift1FNS "asin" asin
acos = lift1FNS "acos" acos
atan = lift1FNS "atan" atan
sinh = lift1FNS "sinh" sinh
cosh = lift1FNS "cosh" cosh
tanh = lift1FNS "tanh" tanh
asinh = lift1FNS "asinh" asinh
acosh = lift1FNS "acosh" acosh
atanh = lift1FNS "atanh" atanh
(**) = lift2FNS "**" (**)
logBase = lift2FNS "logBase" logBase
fusedMA :: (SymWord a, Floating a) => SBV a -> SBV a -> SBV a -> SBV a
fusedMA a b c = SBV k $ Right $ cache r
where k = kindOf a
r st = do swa <- sbvToSW st a
swb <- sbvToSW st b
swc <- sbvToSW st c
newExpr st k (SBVApp smtLibFusedMA [swa, swb, swc])
lift1F :: (SymWord a, Floating a) => (a -> a) -> Op -> SBV a -> SBV a
lift1F f smtOp sv
| Just v <- unliteral sv = literal $ f v
| True = SBV k $ Right $ cache c
where k = kindOf sv
c st = do swa <- sbvToSW st sv
newExpr st k (SBVApp smtOp [swa])
lift1FNS :: (SymWord a, Floating a) => String -> (a -> a) -> SBV a -> SBV a
lift1FNS nm f sv
| Just v <- unliteral sv = literal $ f v
| True = error $ "SBV." ++ nm ++ ": not supported for symbolic values of type " ++ show (kindOf sv)
lift2FNS :: (SymWord a, Floating a) => String -> (a -> a -> a) -> SBV a -> SBV a -> SBV a
lift2FNS nm f sv1 sv2
| Just v1 <- unliteral sv1
, Just v2 <- unliteral sv2 = literal $ f v1 v2
| True = error $ "SBV." ++ nm ++ ": not supported for symbolic values of type " ++ show (kindOf sv1)
rationalCheck :: CW -> CW -> Bool
rationalCheck a b = case (cwVal a, cwVal b) of
(CWAlgReal x, CWAlgReal y) -> isExactRational x && isExactRational y
_ -> True
rationalSBVCheck :: SBV a -> SBV a -> Bool
rationalSBVCheck (SBV KReal (Left a)) (SBV KReal (Left b)) = rationalCheck a b
rationalSBVCheck _ _ = True
noReal :: String -> AlgReal -> AlgReal -> AlgReal
noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b)
noFloat :: String -> Float -> Float -> Float
noFloat o a b = error $ "SBV.Float." ++ o ++ ": Unexpected arguments: " ++ show (a, b)
noDouble :: String -> Double -> Double -> Double
noDouble o a b = error $ "SBV.Double." ++ o ++ ": Unexpected arguments: " ++ show (a, b)
noRealUnary :: String -> AlgReal -> AlgReal
noRealUnary o a = error $ "SBV.AlgReal." ++ o ++ ": Unexpected argument: " ++ show a
noFloatUnary :: String -> Float -> Float
noFloatUnary o a = error $ "SBV.Float." ++ o ++ ": Unexpected argument: " ++ show a
noDoubleUnary :: String -> Double -> Double
noDoubleUnary o a = error $ "SBV.Double." ++ o ++ ": Unexpected argument: " ++ show a
instance (Num a, Bits a, SymWord a) => Bits (SBV a) where
x .&. y
| x `isConcretely` (== 0) = 0
| x `isConcretely` (== 1) = y
| y `isConcretely` (== 0) = 0
| y `isConcretely` (== 1) = x
| True = liftSym2 (mkSymOp And) (const (const True)) (noReal ".&.") (.&.) (noFloat ".&.") (noDouble ".&.") x y
x .|. y
| x `isConcretely` (== 0) = y
| x `isConcretely` (== 1) = 1
| y `isConcretely` (== 0) = x
| y `isConcretely` (== 1) = 1
| True = liftSym2 (mkSymOp Or) (const (const True)) (noReal ".|.") (.|.) (noFloat ".|.") (noDouble ".|.") x y
x `xor` y
| x `isConcretely` (== 0) = y
| y `isConcretely` (== 0) = x
| True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y
complement = liftSym1 (mkSymOp1 Not) (noRealUnary "complement") complement (noFloatUnary "complement") (noDoubleUnary "complement")
bitSize _ = intSizeOf (undefined :: a)
isSigned _ = hasSign (undefined :: a)
bit i = 1 `shiftL` i
shiftL x y
| y < 0 = shiftR x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Shl y)) (noRealUnary "shiftL") (`shiftL` y) (noFloatUnary "shiftL") (noDoubleUnary "shiftL") x
shiftR x y
| y < 0 = shiftL x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Shr y)) (noRealUnary "shiftR") (`shiftR` y) (noFloatUnary "shiftR") (noDoubleUnary "shiftR") x
rotateL x y
| y < 0 = rotateR x (y)
| y == 0 = x
| isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x
| True = shiftL x y
rotateR x y
| y < 0 = rotateL x (y)
| y == 0 = x
| isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x
| True = shiftR x y
x `testBit` i
| isConcrete x = (x .&. bit i) /= 0
| True = error $ "SBV.testBit: Called on symbolic value: " ++ show x ++ ". Use sbvTestBit instead."
popCount x
| isConcrete x = let go !c 0 = c
go !c w = go (c+1) (w .&. (w1))
in go 0 x
| True = error $ "SBV.popCount: Called on symbolic value: " ++ show x ++ ". Use sbvPopCount instead."
rot :: Bool -> Int -> Int -> Integer -> Integer
rot toLeft sz amt x
| sz < 2 = x
| True = norm x y' `shiftL` y .|. norm (x `shiftR` y') y
where (y, y') | toLeft = (amt `mod` sz, sz y)
| True = (sz y', amt `mod` sz)
norm v s = v .&. ((1 `shiftL` s) 1)
sbvTestBit :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool
sbvTestBit x i = (x .&. bit i) ./= 0
sbvPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8
sbvPopCount x
| isReal x = error "SBV.sbvPopCount: Called on a real value"
| isConcrete x = go 0 x
| not (isBounded x) = error "SBV.sbvPopCount: Called on an infinite precision symbolic value"
| True = sum [ite b 1 0 | b <- blastLE x]
where
go !c 0 = c
go !c w = go (c+1) (w .&. (w1))
setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a
setBitTo x i b = ite b (setBit x i) (clearBit x i)
sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sbvShiftLeft x i
| isSigned i = error "sbvShiftLeft: shift amount should be unsigned"
| True = select [x `shiftL` k | k <- [0 .. bitSize x 1]] 0 i
sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sbvShiftRight x i
| isSigned i = error "sbvShiftRight: shift amount should be unsigned"
| True = select [x `shiftR` k | k <- [0 .. bitSize x 1]] 0 i
sbvSignedShiftArithRight:: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sbvSignedShiftArithRight x i
| isSigned i = error "sbvSignedShiftArithRight: shift amount should be unsigned"
| isSigned x = sbvShiftRight x i
| True = ite (msb x)
(complement (sbvShiftRight (complement x) i))
(sbvShiftRight x i)
fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a)
fullAdder a b
| isSigned a = error "fullAdder: only works on unsigned numbers"
| True = (a .> s ||| b .> s, s)
where s = a + b
fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a)
fullMultiplier a b
| isSigned a = error "fullMultiplier: only works on unsigned numbers"
| True = (go (bitSize a) 0 a, a*b)
where go 0 p _ = p
go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (false, p)
(o, p'') = shiftIn c p'
(_, x') = shiftIn o x
in go (n1) p'' x'
shiftIn k v = (lsb v, mask .|. (v `shiftR` 1))
where mask = ite k (bit (bitSize v 1)) 0
blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
blastLE x
| isReal x = error "SBV.blastLE: Called on a real value"
| not (isBounded x) = error "SBV.blastLE: Called on an infinite precision value"
| True = map (sbvTestBit x) [0 .. intSizeOf x 1]
blastBE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
blastBE = reverse . blastLE
lsb :: (Num a, Bits a, SymWord a) => SBV a -> SBool
lsb x = sbvTestBit x 0
msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool
msb x
| isReal x = error "SBV.msb: Called on a real value"
| not (isBounded x) = error "SBV.msb: Called on an infinite precision value"
| True = sbvTestBit x (intSizeOf x 1)
instance (Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) where
succ x
| v == (maxBound :: a) = error $ "Enum.succ{" ++ showType x ++ "}: tried to take `succ' of maxBound"
| True = fromIntegral $ v + 1
where v = enumCvt "succ" x
pred x
| v == (minBound :: a) = error $ "Enum.pred{" ++ showType x ++ "}: tried to take `pred' of minBound"
| True = fromIntegral $ v 1
where v = enumCvt "pred" x
toEnum x
| xi < fromIntegral (minBound :: a) || xi > fromIntegral (maxBound :: a)
= error $ "Enum.toEnum{" ++ showType r ++ "}: " ++ show x ++ " is out-of-bounds " ++ show (minBound :: a, maxBound :: a)
| True
= r
where xi :: Integer
xi = fromIntegral x
r :: SBV a
r = fromIntegral x
fromEnum x
| r < fromIntegral (minBound :: Int) || r > fromIntegral (maxBound :: Int)
= error $ "Enum.fromEnum{" ++ showType x ++ "}: value " ++ show r ++ " is outside of Int's bounds " ++ show (minBound :: Int, maxBound :: Int)
| True
= fromIntegral r
where r :: Integer
r = enumCvt "fromEnum" x
enumFrom x = map fromIntegral [xi .. fromIntegral (maxBound :: a)]
where xi :: Integer
xi = enumCvt "enumFrom" x
enumFromThen x y
| yi >= xi = map fromIntegral [xi, yi .. fromIntegral (maxBound :: a)]
| True = map fromIntegral [xi, yi .. fromIntegral (minBound :: a)]
where xi, yi :: Integer
xi = enumCvt "enumFromThen.x" x
yi = enumCvt "enumFromThen.y" y
enumFromThenTo x y z = map fromIntegral [xi, yi .. zi]
where xi, yi, zi :: Integer
xi = enumCvt "enumFromThenTo.x" x
yi = enumCvt "enumFromThenTo.y" y
zi = enumCvt "enumFromThenTo.z" z
enumCvt :: (SymWord a, Integral a, Num b) => String -> SBV a -> b
enumCvt w x = case unliteral x of
Nothing -> error $ "Enum." ++ w ++ "{" ++ showType x ++ "}: Called on symbolic value " ++ show x
Just v -> fromIntegral v
class SDivisible a where
sQuotRem :: a -> a -> (a, a)
sDivMod :: a -> a -> (a, a)
sQuot :: a -> a -> a
sRem :: a -> a -> a
sDiv :: a -> a -> a
sMod :: a -> a -> a
x `sQuot` y = fst $ x `sQuotRem` y
x `sRem` y = snd $ x `sQuotRem` y
x `sDiv` y = fst $ x `sDivMod` y
x `sMod` y = snd $ x `sDivMod` y
instance SDivisible Word64 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int64 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Word32 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int32 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Word16 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int16 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Word8 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int8 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Integer where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible CW where
sQuotRem a b
| CWInteger x <- cwVal a, CWInteger y <- cwVal b
= let (r1, r2) = sQuotRem x y in (normCW a{ cwVal = CWInteger r1 }, normCW b{ cwVal = CWInteger r2 })
sQuotRem a b = error $ "SBV.sQuotRem: impossible, unexpected args received: " ++ show (a, b)
sDivMod a b
| CWInteger x <- cwVal a, CWInteger y <- cwVal b
= let (r1, r2) = sDivMod x y in (normCW a { cwVal = CWInteger r1 }, normCW b { cwVal = CWInteger r2 })
sDivMod a b = error $ "SBV.sDivMod: impossible, unexpected args received: " ++ show (a, b)
instance SDivisible SWord64 where
sQuotRem = liftQRem
sDivMod = liftDMod
instance SDivisible SInt64 where
sQuotRem = liftQRem
sDivMod = liftDMod
instance SDivisible SWord32 where
sQuotRem = liftQRem
sDivMod = liftDMod
instance SDivisible SInt32 where
sQuotRem = liftQRem
sDivMod = liftDMod
instance SDivisible SWord16 where
sQuotRem = liftQRem
sDivMod = liftDMod
instance SDivisible SInt16 where
sQuotRem = liftQRem
sDivMod = liftDMod
instance SDivisible SWord8 where
sQuotRem = liftQRem
sDivMod = liftDMod
instance SDivisible SInt8 where
sQuotRem = liftQRem
sDivMod = liftDMod
liftQRem :: (SymWord a, Num a, SDivisible 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) = sQuotRem 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
liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
liftDMod x y = ite (y .== 0) (0, x) $ ite (signum r .== negate (signum y)) (q1, r+y) qr
where qr@(q, r) = x `sQuotRem` y
instance SDivisible SInteger where
sDivMod = liftDMod
sQuotRem x y
| not (isSymbolic x || isSymbolic y)
= liftQRem x y
| True
= ite (y .== 0) (0, x) (qE+i, rEi*y)
where (qE, rE) = liftQRem x y
i = ite (x .>= 0 ||| rE .== 0) 0
$ ite (y .> 0) 1 (1)
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 = liftM literal arbitrary
class Mergeable a where
symbolicMerge :: SBool -> a -> a -> a
ite :: SBool -> a -> a -> a
select :: (SymWord b, Num 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 xs err ind
| isReal ind = error "SBV.select: unsupported real valued select/index expression"
| True = walk xs ind err
where walk [] _ acc = acc
walk (e:es) i acc = walk es (i1) (ite (i .== 0) e acc)
instance SymWord a => Mergeable (SBV a) where
symbolicMerge t a@(SBV{}) b@(SBV{})
| Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv
= a
| True
= SBV k $ Right $ cache c
where k = kindOf 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
case () of
() | swa == swb -> return swa
() | swa == trueSW && swb == falseSW -> return swt
() | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt])
() -> newExpr st k (SBVApp Ite [swt, swa, swb])
select xs err ind
| SBV _ (Left c) <- ind = case cwVal c of
CWInteger i -> if i < 0 || i >= genericLength xs
then err
else xs `genericIndex` i
_ -> error "SBV.select: unsupported real valued select/index expression"
select xs err ind = SBV kElt $ Right $ cache r
where kInd = kindOf ind
kElt = kindOf 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 kInd kElt sws
swi <- sbvToSW st ind
let len = length xs
newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, 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)
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 (KBounded False 1) $ Right $ cache c
where c st = do ai <- uncacheAI a st
bi <- uncacheAI b st
newExpr st (KBounded 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 $ fromMaybe (error "Reading from an uninitialized array entry") mbiVal
readArray (SFunArray f) = f
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
class Uninterpreted a where
uninterpret :: String -> a
cgUninterpret :: String -> [String] -> a -> a
sbvUninterpret :: Maybe ([String], a) -> String -> a
uninterpret = sbvUninterpret Nothing
cgUninterpret nm code v = sbvUninterpret (Just (code, v)) nm
instance HasKind a => Uninterpreted (SBV a) where
sbvUninterpret mbCgData nm
| Just (_, v) <- mbCgData = v
| True = SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st v
| True = do newUninterpreted st nm (SBVType [ka]) (fst `fmap` mbCgData)
newExpr st ka $ SBVApp (Uninterpreted nm) []
forceArg :: SW -> IO ()
forceArg (SW k n) = k `seq` n `seq` return ()
instance (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
where f arg0
| Just (_, v) <- mbCgData, isConcrete arg0
= v arg0
| True
= SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
kb = kindOf (undefined :: b)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0)
| True = do newUninterpreted st nm (SBVType [kb, ka]) (fst `fmap` mbCgData)
sw0 <- sbvToSW st arg0
mapM_ forceArg [sw0]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0]
instance (SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
where f arg0 arg1
| Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1
= v arg0 arg1
| True
= SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
kb = kindOf (undefined :: b)
kc = kindOf (undefined :: c)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1)
| True = do newUninterpreted st nm (SBVType [kc, kb, ka]) (fst `fmap` mbCgData)
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
mapM_ forceArg [sw0, sw1]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1]
instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
where f arg0 arg1 arg2
| Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2
= v arg0 arg1 arg2
| True
= SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
kb = kindOf (undefined :: b)
kc = kindOf (undefined :: c)
kd = kindOf (undefined :: d)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2)
| True = do newUninterpreted st nm (SBVType [kd, kc, kb, ka]) (fst `fmap` mbCgData)
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
mapM_ forceArg [sw0, sw1, sw2]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]
instance (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
where f arg0 arg1 arg2 arg3
| Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3
= v arg0 arg1 arg2 arg3
| True
= SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
kb = kindOf (undefined :: b)
kc = kindOf (undefined :: c)
kd = kindOf (undefined :: d)
ke = kindOf (undefined :: e)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3)
| True = do newUninterpreted st nm (SBVType [ke, kd, kc, kb, ka]) (fst `fmap` mbCgData)
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
sw3 <- sbvToSW st arg3
mapM_ forceArg [sw0, sw1, sw2, sw3]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]
instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
where f arg0 arg1 arg2 arg3 arg4
| Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4
= v arg0 arg1 arg2 arg3 arg4
| True
= SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
kb = kindOf (undefined :: b)
kc = kindOf (undefined :: c)
kd = kindOf (undefined :: d)
ke = kindOf (undefined :: e)
kf = kindOf (undefined :: f)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4)
| True = do newUninterpreted st nm (SBVType [kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData)
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 ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]
instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
where f arg0 arg1 arg2 arg3 arg4 arg5
| Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5
= v arg0 arg1 arg2 arg3 arg4 arg5
| True
= SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
kb = kindOf (undefined :: b)
kc = kindOf (undefined :: c)
kd = kindOf (undefined :: d)
ke = kindOf (undefined :: e)
kf = kindOf (undefined :: f)
kg = kindOf (undefined :: g)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4 arg5)
| True = do newUninterpreted st nm (SBVType [kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData)
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 ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]
instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)
=> Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
where f arg0 arg1 arg2 arg3 arg4 arg5 arg6
| Just (_, v) <- mbCgData, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6
= v arg0 arg1 arg2 arg3 arg4 arg5 arg6
| True
= SBV ka $ Right $ cache result
where ka = kindOf (undefined :: a)
kb = kindOf (undefined :: b)
kc = kindOf (undefined :: c)
kd = kindOf (undefined :: d)
ke = kindOf (undefined :: e)
kf = kindOf (undefined :: f)
kg = kindOf (undefined :: g)
kh = kindOf (undefined :: h)
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6)
| True = do newUninterpreted st nm (SBVType [kh, kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData)
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 ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
instance (SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where
sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc2 `fmap` mbCgData) nm in uncurry f
where uc2 (cs, fn) = (cs, curry fn)
instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where
sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc3 `fmap` mbCgData) nm in \(arg0, arg1, arg2) -> f arg0 arg1 arg2
where uc3 (cs, fn) = (cs, \a b c -> fn (a, b, c))
instance (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)
=> Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc4 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3
where uc4 (cs, fn) = (cs, \a b c d -> fn (a, b, c, d))
instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)
=> Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc5 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4
where uc5 (cs, fn) = (cs, \a b c d e -> fn (a, b, c, d, e))
instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)
=> Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc6 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5
where uc6 (cs, fn) = (cs, \a b c d e f -> fn (a, b, c, d, e, f))
instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a)
=> Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc7 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6
where uc7 (cs, fn) = (cs, \a b c d e f g -> fn (a, b, c, d, e, f, g))
constrain :: SBool -> Symbolic ()
constrain c = addConstraint Nothing c (bnot c)
pConstrain :: Double -> SBool -> Symbolic ()
pConstrain t c = addConstraint (Just t) c (bnot c)
instance Testable SBool where
property (SBV _ (Left b)) = property (cwToBool b)
property s = error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show s ++ ")"
instance Testable (Symbolic SBool) where
property m = QC.whenFail (putStrLn msg) $ QC.monadicIO test
where runOnce g = do (r, Result _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' (Concrete g) m
let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
cond = all (cwToBool . cval) cstrs
when (isSymbolic r) $ error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show r ++ ")"
if cond then if r `isConcretely` id
then return False
else do putStrLn $ complain tvals
return True
else runOnce g
test = do die <- QC.run $ newStdGen >>= runOnce
when die $ fail "Falsifiable"
msg = "*** SBV: See the custom counter example reported above."
complain [] = "*** SBV Counter Example: Predicate contains no universally quantified variables."
complain qcInfo = intercalate "\n" $ "*** SBV Counter Example:" : map ((" " ++) . info) qcInfo
where maxLen = maximum (0:[length s | (s, _) <- qcInfo])
shN s = s ++ replicate (maxLen length s) ' '
info (n, cw) = shN n ++ " = " ++ show cw
slet :: (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b
slet x f = SBV k $ Right $ cache r
where k = kindOf (undefined `asTypeOf` f x)
r st = do xsw <- sbvToSW st x
let xsbv = SBV (kindOf x) (Right (cache (const (return xsw))))
res = f xsbv
sbvToSW st res