module Data.SBV.BitVectors.Model (
Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..), SNum
, sbvTestBit, sbvPopCount, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE
, lsb, msb, SBVUF, sbvUFName, 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
)
where
import Control.Monad (when)
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
liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> SBV b -> SBV b
liftSym1 _ opCR opCI (SBV k (Left a)) = SBV k $ Left $ mapCW opCR opCI a
liftSym1 opS _ _ a@(SBV k _) = SBV k $ Right $ cache c
where c st = do swa <- sbvToSW st a
opS st k swa
liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b
liftSym2 _ opCR opCI (SBV k (Left a)) (SBV _ (Left b)) = SBV k $ Left $ mapCW2 opCR opCI a b
liftSym2 opS _ _ a@(SBV k _) b = SBV k $ Right $ cache c
where c st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
opS st k sw1 sw2
liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool
liftSym2B _ opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opCR opCI a b)
liftSym2B 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
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 _ (Right x)) = fromInteger x
genFromCW c = error $ "genFromCW: Unsupported AlgReal value: " ++ show c
instance SymWord Bool where
forall = genVar (Just ALL) (KBounded False 1)
forall_ = genVar_ (Just ALL) (KBounded False 1)
exists = genVar (Just EX) (KBounded False 1)
exists_ = genVar_ (Just EX) (KBounded False 1)
free = genVar Nothing (KBounded False 1)
free_ = genVar_ Nothing (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
forall = genVar (Just ALL) (KBounded False 8)
forall_ = genVar_ (Just ALL) (KBounded False 8)
exists = genVar (Just EX) (KBounded False 8)
exists_ = genVar_ (Just EX) (KBounded False 8)
free = genVar Nothing (KBounded False 8)
free_ = genVar_ Nothing (KBounded False 8)
literal = genLiteral (KBounded False 8)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int8 where
forall = genVar (Just ALL) (KBounded True 8)
forall_ = genVar_ (Just ALL) (KBounded True 8)
exists = genVar (Just EX) (KBounded True 8)
exists_ = genVar_ (Just EX) (KBounded True 8)
free = genVar Nothing (KBounded True 8)
free_ = genVar_ Nothing (KBounded True 8)
literal = genLiteral (KBounded True 8)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Word16 where
forall = genVar (Just ALL) (KBounded False 16)
forall_ = genVar_ (Just ALL) (KBounded False 16)
exists = genVar (Just EX) (KBounded False 16)
exists_ = genVar_ (Just EX) (KBounded False 16)
free = genVar Nothing (KBounded False 16)
free_ = genVar_ Nothing (KBounded False 16)
literal = genLiteral (KBounded False 16)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int16 where
forall = genVar (Just ALL) (KBounded True 16)
forall_ = genVar_ (Just ALL) (KBounded True 16)
exists = genVar (Just EX) (KBounded True 16)
exists_ = genVar_ (Just EX) (KBounded True 16)
free = genVar Nothing (KBounded True 16)
free_ = genVar_ Nothing (KBounded True 16)
literal = genLiteral (KBounded True 16)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Word32 where
forall = genVar (Just ALL) (KBounded False 32)
forall_ = genVar_ (Just ALL) (KBounded False 32)
exists = genVar (Just EX) (KBounded False 32)
exists_ = genVar_ (Just EX) (KBounded False 32)
free = genVar Nothing (KBounded False 32)
free_ = genVar_ Nothing (KBounded False 32)
literal = genLiteral (KBounded False 32)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int32 where
forall = genVar (Just ALL) (KBounded True 32)
forall_ = genVar_ (Just ALL) (KBounded True 32)
exists = genVar (Just EX) (KBounded True 32)
exists_ = genVar_ (Just EX) (KBounded True 32)
free = genVar Nothing (KBounded True 32)
free_ = genVar_ Nothing (KBounded True 32)
literal = genLiteral (KBounded True 32)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Word64 where
forall = genVar (Just ALL) (KBounded False 64)
forall_ = genVar_ (Just ALL) (KBounded False 64)
exists = genVar (Just EX) (KBounded False 64)
exists_ = genVar_ (Just EX) (KBounded False 64)
free = genVar Nothing (KBounded False 64)
free_ = genVar_ Nothing (KBounded False 64)
literal = genLiteral (KBounded False 64)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Int64 where
forall = genVar (Just ALL) (KBounded True 64)
forall_ = genVar_ (Just ALL) (KBounded True 64)
exists = genVar (Just EX) (KBounded True 64)
exists_ = genVar_ (Just EX) (KBounded True 64)
free = genVar Nothing (KBounded True 64)
free_ = genVar_ Nothing (KBounded True 64)
literal = genLiteral (KBounded True 64)
fromCW = genFromCW
mbMaxBound = Just maxBound
mbMinBound = Just minBound
instance SymWord Integer where
forall = mkSymSBV (Just ALL) KUnbounded . Just
forall_ = mkSymSBV (Just ALL) KUnbounded Nothing
exists = mkSymSBV (Just EX) KUnbounded . Just
exists_ = mkSymSBV (Just EX) KUnbounded Nothing
free = mkSymSBV Nothing KUnbounded . Just
free_ = mkSymSBV Nothing KUnbounded Nothing
literal = SBV KUnbounded . Left . mkConstCW KUnbounded
fromCW = genFromCW
mbMaxBound = Nothing
mbMinBound = Nothing
instance SymWord AlgReal where
forall = mkSymSBV (Just ALL) KReal . Just
forall_ = mkSymSBV (Just ALL) KReal Nothing
exists = mkSymSBV (Just EX) KReal . Just
exists_ = mkSymSBV (Just EX) KReal Nothing
free = mkSymSBV Nothing KReal . Just
free_ = mkSymSBV Nothing KReal Nothing
literal = SBV KReal . Left . CW KReal . Left
fromCW (CW _ (Left a)) = a
fromCW c = error $ "SymWord.AlgReal: Unexpected non-real value: " ++ show c
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
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) (==) (==)
(./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) (/=) (/=)
eqOpt :: SW -> SW -> SW -> Maybe SW
eqOpt w x y = 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) (<) (<) x y
x .<= y
| Just mb <- mbMinBound, x `isConcretely` (== mb) = true
| Just mb <- mbMaxBound, y `isConcretely` (== mb) = true
| True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) (<=) (<=) x y
x .> y
| Just mb <- mbMinBound, x `isConcretely` (== mb) = false
| Just mb <- mbMaxBound, y `isConcretely` (== mb) = false
| True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) (>) (>) x y
x .>= y
| Just mb <- mbMaxBound, x `isConcretely` (== mb) = true
| Just mb <- mbMinBound, y `isConcretely` (== mb) = true
| True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) (>=) (>=) 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 (OrdSymbolic a, Num a) => SNum a
instance SNum SWord8
instance SNum SWord16
instance SNum SWord32
instance SNum SWord64
instance SNum SInt8
instance SNum SInt16
instance SNum SInt32
instance SNum SInt64
instance SNum SInteger
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 :: (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 Fractional SReal where
fromRational = literal . fromRational
x / y = liftSym2 (mkSymOp Quot) (/) die x y
where
die = error $ "impossible: non-real value found in Fractional.SReal " ++ show (x, y)
noReal :: String -> AlgReal -> AlgReal -> AlgReal
noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b)
noRealUnary :: String -> AlgReal -> AlgReal
noRealUnary o a = error $ "SBV.AlgReal." ++ o ++ ": Unexpected argument: " ++ show a
instance (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) (noReal ".&.") (.&.) x y
x .|. y
| x `isConcretely` (== 0) = y
| x `isConcretely` (== 1) = 1
| y `isConcretely` (== 0) = x
| y `isConcretely` (== 1) = 1
| True = liftSym2 (mkSymOp Or) (noReal ".|.") (.|.) x y
x `xor` y
| x `isConcretely` (== 0) = y
| y `isConcretely` (== 0) = x
| True = liftSym2 (mkSymOp XOr) (noReal "xor") xor x y
complement = liftSym1 (mkSymOp1 Not) (noRealUnary "Not") complement
bitSize _ = intSizeOf (undefined :: a)
isSigned _ = hasSign (undefined :: a)
shiftL x y
| y < 0 = shiftR x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Shl y)) (noRealUnary "shiftL") (`shiftL` y) x
shiftR x y
| y < 0 = shiftL x (y)
| y == 0 = x
| True = liftSym1 (mkSymOp1 (Shr y)) (noRealUnary "shiftR") (`shiftR` y) 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) 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) 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."
#if __GLASGOW_HASKELL__ >= 704
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."
#endif
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 :: (Bits a, SymWord a) => SBV a -> Int -> SBool
sbvTestBit x i = (x .&. bit i) ./= 0
sbvPopCount :: (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 :: (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
| 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 :: (Bits a, SymWord a) => SBV a -> [SBool]
blastBE = reverse . blastLE
lsb :: (Bits a, SymWord a) => SBV a -> SBool
lsb x = sbvTestBit x 0
msb :: (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 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 Int64 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 Int32 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 Int16 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 Int8 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 a b
| Right x <- cwVal a, Right y <- cwVal b
= let (r1, r2) = bvQuotRem x y in (a { cwVal = Right r1 }, b { cwVal = Right r2 })
bvQuotRem a b = error $ "SBV.liftQRem: impossible, unexpected args received: " ++ show (a, b)
instance BVDivisible SWord64 where
bvQuotRem = liftQRem
instance BVDivisible SInt64 where
bvQuotRem = liftQRem
instance BVDivisible SWord32 where
bvQuotRem = liftQRem
instance BVDivisible SInt32 where
bvQuotRem = liftQRem
instance BVDivisible SWord16 where
bvQuotRem = liftQRem
instance BVDivisible SInt16 where
bvQuotRem = liftQRem
instance BVDivisible SWord8 where
bvQuotRem = liftQRem
instance BVDivisible SInt8 where
bvQuotRem = liftQRem
instance BVDivisible SInteger 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 xs err ind
| isReal ind = error "SBV.select: unsupported real valued select/index expression"
| Just i <- unliteral ind = if i < 0 || i >= genericLength xs
then err
else xs `genericIndex` i
| 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, 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
| 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 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 $ 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)
cgUninterpret :: String -> [String] -> a -> a
sbvUninterpret :: Maybe ([String], a) -> String -> (SBVUF, a)
uninterpret = snd . uninterpretWithHandle
uninterpretWithHandle = sbvUninterpret Nothing
cgUninterpret nm code v = snd $ sbvUninterpret (Just (code, v)) nm
instance HasKind a => Uninterpreted (SBV a) where
sbvUninterpret mbCgData nm
| Just (_, v) <- mbCgData = (mkUFName nm, v)
| True = (mkUFName nm, 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 = (mkUFName 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 = (mkUFName 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 = (mkUFName 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 = (mkUFName 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 = (mkUFName 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 = (mkUFName 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 = (mkUFName 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 (h, f) = sbvUninterpret (uc2 `fmap` mbCgData) nm in (h, \(arg0, arg1) -> f arg0 arg1)
where uc2 (cs, fn) = (cs, \a b -> fn (a, b))
instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where
sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc3 `fmap` mbCgData) nm in (h, \(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 (h, f) = sbvUninterpret (uc4 `fmap` mbCgData) nm in (h, \(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 (h, f) = sbvUninterpret (uc5 `fmap` mbCgData) nm in (h, \(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 (h, f) = sbvUninterpret (uc6 `fmap` mbCgData) nm in (h, \(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 (h, f) = sbvUninterpret (uc7 `fmap` mbCgData) nm in (h, \(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