module Data.SBV.BitVectors.Data
( SBool, SWord8, SWord16, SWord32, SWord64
, SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble
, nan, infinity, sNaN, sInfinity, RoundingMode(..), smtLibSquareRoot, smtLibFusedMA
, SymWord(..)
, CW(..), CWVal(..), AlgReal(..), cwSameType, cwIsBit, cwToBool
, mkConstCW ,liftCW2, mapCW, mapCW2
, SW(..), trueSW, falseSW, trueCW, falseCW, normCW
, SBV(..), NodeId(..), mkSymSBV, mkSymSBVWithRandom
, ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind
, sbvToSW, sbvToSymSW, forceSWArg
, SBVExpr(..), newExpr
, cache, Cached, uncache, uncacheAI, HasKind(..)
, Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, SExecutable(..), runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition
, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)
, Logic(..), SMTLibLogic(..)
, getTraceInfo, getConstraints, addConstraint
, SBVType(..), newUninterpreted, unintFnUIKind, addAxiom
, Quantifier(..), needsExistentials
, SMTLibPgm(..), SMTLibVersion(..)
, SolverCapabilities(..)
, extractSymbolicSimulationState
, SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), getSBranchRunConfig
) where
import Control.DeepSeq (NFData(..))
import Control.Applicative (Applicative)
import Control.Monad (when)
import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)
import Control.Monad.Trans (MonadIO, liftIO)
import Data.Char (isAlpha, isAlphaNum)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Word (Word8, Word16, Word32, Word64)
import Data.IORef (IORef, newIORef, modifyIORef, readIORef, writeIORef)
import Data.List (intercalate, sortBy)
import Data.Maybe (isJust, fromJust)
import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields)
import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith)
import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup)
import qualified Data.Set as Set (Set, empty, toList, insert)
import qualified Data.Foldable as F (toList)
import qualified Data.Sequence as S (Seq, empty, (|>))
import System.Exit (ExitCode(..))
import System.Mem.StableName
import System.Random
import Data.SBV.BitVectors.AlgReals
import Data.SBV.Utils.Lib
data CWVal = CWAlgReal AlgReal
| CWInteger Integer
| CWFloat Float
| CWDouble Double
| CWUserSort (Maybe Int, String)
instance Eq CWVal where
CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b
CWInteger a == CWInteger b = a == b
CWUserSort a == CWUserSort b = a == b
CWFloat a == CWFloat b = a == b
CWDouble a == CWDouble b = a == b
_ == _ = False
instance Ord CWVal where
CWAlgReal a `compare` CWAlgReal b = a `algRealStructuralCompare` b
CWAlgReal _ `compare` CWInteger _ = LT
CWAlgReal _ `compare` CWFloat _ = LT
CWAlgReal _ `compare` CWDouble _ = LT
CWAlgReal _ `compare` CWUserSort _ = LT
CWInteger _ `compare` CWAlgReal _ = GT
CWInteger a `compare` CWInteger b = a `compare` b
CWInteger _ `compare` CWFloat _ = LT
CWInteger _ `compare` CWDouble _ = LT
CWInteger _ `compare` CWUserSort _ = LT
CWFloat _ `compare` CWAlgReal _ = GT
CWFloat _ `compare` CWInteger _ = GT
CWFloat a `compare` CWFloat b = a `compare` b
CWFloat _ `compare` CWDouble _ = LT
CWFloat _ `compare` CWUserSort _ = LT
CWDouble _ `compare` CWAlgReal _ = GT
CWDouble _ `compare` CWInteger _ = GT
CWDouble _ `compare` CWFloat _ = GT
CWDouble a `compare` CWDouble b = a `compare` b
CWDouble _ `compare` CWUserSort _ = LT
CWUserSort _ `compare` CWAlgReal _ = GT
CWUserSort _ `compare` CWInteger _ = GT
CWUserSort _ `compare` CWFloat _ = GT
CWUserSort _ `compare` CWDouble _ = GT
CWUserSort a `compare` CWUserSort b = a `compare` b
data CW = CW { cwKind :: !Kind
, cwVal :: !CWVal
}
deriving (Eq, Ord)
cwSameType :: CW -> CW -> Bool
cwSameType x y = cwKind x == cwKind y
cwIsBit :: CW -> Bool
cwIsBit x = case cwKind x of
KBool -> True
_ -> False
cwToBool :: CW -> Bool
cwToBool x = cwVal x /= CWInteger 0
normCW :: CW -> CW
normCW c@(CW (KBounded signed sz) (CWInteger v)) = c { cwVal = CWInteger norm }
where norm | sz == 0 = 0
| signed = let rg = 2 ^ (sz 1)
in case divMod v rg of
(a, b) | even a -> b
(_, b) -> b rg
| True = v `mod` (2 ^ sz)
normCW c = c
instance Eq G.DataType where
a == b = G.tyconUQname (G.dataTypeName a) == G.tyconUQname (G.dataTypeName b)
instance Ord G.DataType where
a `compare` b = G.tyconUQname (G.dataTypeName a) `compare` G.tyconUQname (G.dataTypeName b)
data Kind = KBool
| KBounded Bool Int
| KUnbounded
| KReal
| KUserSort String (Either String [String], G.DataType)
| KFloat
| KDouble
deriving (Eq, Ord)
instance Show Kind where
show KBool = "SBool"
show (KBounded False n) = "SWord" ++ show n
show (KBounded True n) = "SInt" ++ show n
show KUnbounded = "SInteger"
show KReal = "SReal"
show (KUserSort s _) = s
show KFloat = "SFloat"
show KDouble = "SDouble"
newtype NodeId = NodeId Int deriving (Eq, Ord)
data SW = SW Kind NodeId deriving (Eq, Ord)
forceSWArg :: SW -> IO ()
forceSWArg (SW k n) = k `seq` n `seq` return ()
data Quantifier = ALL | EX deriving Eq
needsExistentials :: [Quantifier] -> Bool
needsExistentials = (EX `elem`)
falseSW :: SW
falseSW = SW KBool $ NodeId (2)
trueSW :: SW
trueSW = SW KBool $ NodeId (1)
falseCW :: CW
falseCW = CW KBool (CWInteger 0)
trueCW :: CW
trueCW = CW KBool (CWInteger 1)
newtype SBVType = SBVType [Kind]
deriving (Eq, Ord)
typeArity :: SBVType -> Int
typeArity (SBVType xs) = length xs 1
instance Show SBVType where
show (SBVType []) = error "SBV: internal error, empty SBVType"
show (SBVType xs) = intercalate " -> " $ map show xs
data Op = Plus | Times | Minus | UNeg | Abs
| Quot | Rem
| Equal | NotEqual
| LessThan | GreaterThan | LessEq | GreaterEq
| Ite
| And | Or | XOr | Not
| Shl Int | Shr Int | Rol Int | Ror Int
| Extract Int Int
| Join
| LkUp (Int, Kind, Kind, Int) !SW !SW
| ArrEq Int Int
| ArrRead Int
| Uninterpreted String
deriving (Eq, Ord)
smtLibSquareRoot :: Op
smtLibSquareRoot = Uninterpreted "fp.sqrt"
smtLibFusedMA :: Op
smtLibFusedMA = Uninterpreted "fp.fma"
data SBVExpr = SBVApp !Op ![SW]
deriving (Eq, Ord)
class HasKind a where
kindOf :: a -> Kind
hasSign :: a -> Bool
intSizeOf :: a -> Int
isBoolean :: a -> Bool
isBounded :: a -> Bool
isReal :: a -> Bool
isFloat :: a -> Bool
isDouble :: a -> Bool
isInteger :: a -> Bool
isUninterpreted :: a -> Bool
showType :: a -> String
hasSign x = case kindOf x of
KBool -> False
KBounded b _ -> b
KUnbounded -> True
KReal -> True
KFloat -> True
KDouble -> True
KUserSort{} -> False
intSizeOf x = case kindOf x of
KBool -> error "SBV.HasKind.intSizeOf((S)Bool)"
KBounded _ s -> s
KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)"
KReal -> error "SBV.HasKind.intSizeOf((S)Real)"
KFloat -> error "SBV.HasKind.intSizeOf((S)Float)"
KDouble -> error "SBV.HasKind.intSizeOf((S)Double)"
KUserSort s _ -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s
isBoolean x | KBool{} <- kindOf x = True
| True = False
isBounded x | KBounded{} <- kindOf x = True
| True = False
isReal x | KReal{} <- kindOf x = True
| True = False
isFloat x | KFloat{} <- kindOf x = True
| True = False
isDouble x | KDouble{} <- kindOf x = True
| True = False
isInteger x | KUnbounded{} <- kindOf x = True
| True = False
isUninterpreted x | KUserSort{} <- kindOf x = True
| True = False
showType = show . kindOf
default kindOf :: (Read a, G.Data a) => a -> Kind
kindOf = constructUKind
instance HasKind Bool where kindOf _ = KBool
instance HasKind Int8 where kindOf _ = KBounded True 8
instance HasKind Word8 where kindOf _ = KBounded False 8
instance HasKind Int16 where kindOf _ = KBounded True 16
instance HasKind Word16 where kindOf _ = KBounded False 16
instance HasKind Int32 where kindOf _ = KBounded True 32
instance HasKind Word32 where kindOf _ = KBounded False 32
instance HasKind Int64 where kindOf _ = KBounded True 64
instance HasKind Word64 where kindOf _ = KBounded False 64
instance HasKind Integer where kindOf _ = KUnbounded
instance HasKind AlgReal where kindOf _ = KReal
instance HasKind Float where kindOf _ = KFloat
instance HasKind Double where kindOf _ = KDouble
liftCW :: (AlgReal -> b) -> (Integer -> b) -> (Float -> b) -> (Double -> b) -> ((Maybe Int, String) -> b) -> CW -> b
liftCW f _ _ _ _ (CW _ (CWAlgReal v)) = f v
liftCW _ f _ _ _ (CW _ (CWInteger v)) = f v
liftCW _ _ f _ _ (CW _ (CWFloat v)) = f v
liftCW _ _ _ f _ (CW _ (CWDouble v)) = f v
liftCW _ _ _ _ f (CW _ (CWUserSort v)) = f v
liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b
liftCW2 r i f d u x y = case (cwVal x, cwVal y) of
(CWAlgReal a, CWAlgReal b) -> r a b
(CWInteger a, CWInteger b) -> i a b
(CWFloat a, CWFloat b) -> f a b
(CWDouble a, CWDouble b) -> d a b
(CWUserSort a, CWUserSort b) -> u a b
_ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y)
mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW
mapCW r i f d u x = normCW $ CW (cwKind x) $ case cwVal x of
CWAlgReal a -> CWAlgReal (r a)
CWInteger a -> CWInteger (i a)
CWFloat a -> CWFloat (f a)
CWDouble a -> CWDouble (d a)
CWUserSort a -> CWUserSort (u a)
mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW
mapCW2 r i f d u x y = case (cwSameType x y, cwVal x, cwVal y) of
(True, CWAlgReal a, CWAlgReal b) -> normCW $ CW (cwKind x) (CWAlgReal (r a b))
(True, CWInteger a, CWInteger b) -> normCW $ CW (cwKind x) (CWInteger (i a b))
(True, CWFloat a, CWFloat b) -> normCW $ CW (cwKind x) (CWFloat (f a b))
(True, CWDouble a, CWDouble b) -> normCW $ CW (cwKind x) (CWDouble (d a b))
(True, CWUserSort a, CWUserSort b) -> normCW $ CW (cwKind x) (CWUserSort (u a b))
_ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y)
instance HasKind CW where
kindOf = cwKind
instance HasKind SW where
kindOf (SW k _) = k
instance Show CW where
show w | cwIsBit w = show (cwToBool w)
show w = liftCW show show show show snd w ++ " :: " ++ showType w
instance Show SW where
show (SW _ (NodeId n))
| n < 0 = "s_" ++ show (abs n)
| True = 's' : show n
instance Show Op where
show (Shl i) = "<<" ++ show i
show (Shr i) = ">>" ++ show i
show (Rol i) = "<<<" ++ show i
show (Ror i) = ">>>" ++ show i
show (Extract i j) = "choose [" ++ show i ++ ":" ++ show j ++ "]"
show (LkUp (ti, at, rt, l) i e)
= "lookup(" ++ tinfo ++ ", " ++ show i ++ ", " ++ show e ++ ")"
where tinfo = "table" ++ show ti ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")"
show (ArrEq i j) = "array_" ++ show i ++ " == array_" ++ show j
show (ArrRead i) = "select array_" ++ show i
show (Uninterpreted i) = "[uninterpreted] " ++ i
show op
| Just s <- op `lookup` syms = s
| True = error "impossible happened; can't find op!"
where syms = [ (Plus, "+"), (Times, "*"), (Minus, "-"), (UNeg, "-"), (Abs, "abs")
, (Quot, "quot")
, (Rem, "rem")
, (Equal, "=="), (NotEqual, "/=")
, (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<"), (GreaterEq, ">")
, (Ite, "if_then_else")
, (And, "&"), (Or, "|"), (XOr, "^"), (Not, "~")
, (Join, "#")
]
reorder :: SBVExpr -> SBVExpr
reorder s = case s of
SBVApp op [a, b] | isCommutative op && a > b -> SBVApp op [b, a]
_ -> s
where isCommutative :: Op -> Bool
isCommutative o = o `elem` [Plus, Times, Equal, NotEqual, And, Or, XOr]
instance Show SBVExpr where
show (SBVApp Ite [t, a, b]) = unwords ["if", show t, "then", show a, "else", show b]
show (SBVApp (Shl i) [a]) = unwords [show a, "<<", show i]
show (SBVApp (Shr i) [a]) = unwords [show a, ">>", show i]
show (SBVApp (Rol i) [a]) = unwords [show a, "<<<", show i]
show (SBVApp (Ror i) [a]) = unwords [show a, ">>>", show i]
show (SBVApp op [a, b]) = unwords [show a, show op, show b]
show (SBVApp op args) = unwords (show op : map show args)
newtype SBVPgm = SBVPgm {pgmAssignments :: (S.Seq (SW, SBVExpr))}
type NamedSymVar = (SW, String)
data UnintKind = UFun Int String | UArr Int String
deriving Show
data Result = Result (Set.Set Kind)
[(String, CW)]
[(String, [String])]
[(Quantifier, NamedSymVar)]
[(SW, CW)]
[((Int, Kind, Kind), [SW])]
[(Int, ArrayInfo)]
[(String, SBVType)]
[(String, [String])]
SBVPgm
[SW]
[SW]
getConstraints :: Result -> [SW]
getConstraints (Result _ _ _ _ _ _ _ _ _ _ cstrs _) = cstrs
getTraceInfo :: Result -> [(String, CW)]
getTraceInfo (Result _ tvals _ _ _ _ _ _ _ _ _ _) = tvals
instance Show Result where
show (Result _ _ _ _ cs _ _ [] [] _ [] [r])
| Just c <- r `lookup` cs
= show c
show (Result kinds _ cgs is cs ts as uis axs xs cstrs os) = intercalate "\n" $
(if null usorts then [] else "SORTS" : map (" " ++) usorts)
++ ["INPUTS"]
++ map shn is
++ ["CONSTANTS"]
++ map shc cs
++ ["TABLES"]
++ map sht ts
++ ["ARRAYS"]
++ map sha as
++ ["UNINTERPRETED CONSTANTS"]
++ map shui uis
++ ["USER GIVEN CODE SEGMENTS"]
++ concatMap shcg cgs
++ ["AXIOMS"]
++ map shax axs
++ ["DEFINE"]
++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList (pgmAssignments xs))
++ ["CONSTRAINTS"]
++ map ((" " ++) . show) cstrs
++ ["OUTPUTS"]
++ map ((" " ++) . show) os
where usorts = [s | KUserSort s _ <- Set.toList kinds]
shs sw = show sw ++ " :: " ++ showType sw
sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es
shc (sw, cw) = " " ++ show sw ++ " = " ++ show cw
shcg (s, ss) = ("Variable: " ++ s) : map (" " ++) ss
shn (q, (sw, nm)) = " " ++ ni ++ " :: " ++ showType sw ++ ex ++ alias
where ni = show sw
ex | q == ALL = ""
| True = ", existential"
alias | ni == nm = ""
| True = ", aliasing " ++ show nm
sha (i, (nm, (ai, bi), ctx)) = " " ++ ni ++ " :: " ++ show ai ++ " -> " ++ show bi ++ alias
++ "\n Context: " ++ show ctx
where ni = "array_" ++ show i
alias | ni == nm = ""
| True = ", aliasing " ++ show nm
shui (nm, t) = " [uninterpreted] " ++ nm ++ " :: " ++ show t
shax (nm, ss) = " -- user defined axiom: " ++ nm ++ "\n " ++ intercalate "\n " ss
data ArrayContext = ArrayFree (Maybe SW)
| ArrayReset Int SW
| ArrayMutate Int SW SW
| ArrayMerge SW Int Int
instance Show ArrayContext where
show (ArrayFree Nothing) = " initialized with random elements"
show (ArrayFree (Just s)) = " initialized with " ++ show s ++ " :: " ++ showType s
show (ArrayReset i s) = " reset array_" ++ show i ++ " with " ++ show s ++ " :: " ++ showType s
show (ArrayMutate i a b) = " cloned from array_" ++ show i ++ " with " ++ show a ++ " :: " ++ showType a ++ " |-> " ++ show b ++ " :: " ++ showType b
show (ArrayMerge s i j) = " merged arrays " ++ show i ++ " and " ++ show j ++ " on condition " ++ show s
type ExprMap = Map.Map SBVExpr SW
type CnstMap = Map.Map CW SW
type KindSet = Set.Set Kind
type TableMap = Map.Map [SW] (Int, Kind, Kind)
type ArrayInfo = (String, (Kind, Kind), ArrayContext)
type ArrayMap = IMap.IntMap ArrayInfo
type UIMap = Map.Map String SBVType
type CgMap = Map.Map String [String]
type Cache a = IMap.IntMap [(StableName (State -> IO a), a)]
unintFnUIKind :: (String, SBVType) -> (String, UnintKind)
unintFnUIKind (s, t) = (s, UFun (typeArity t) s)
arrayUIKind :: (Int, ArrayInfo) -> Maybe (String, UnintKind)
arrayUIKind (i, (nm, _, ctx))
| external ctx = Just ("array_" ++ show i, UArr 1 nm)
| True = Nothing
where external (ArrayFree{}) = True
external (ArrayReset{}) = False
external (ArrayMutate{}) = False
external (ArrayMerge{}) = False
data SBVRunMode = Proof (Bool, Maybe SMTConfig)
| CodeGen
| Concrete StdGen
isConcreteMode :: SBVRunMode -> Bool
isConcreteMode (Concrete _) = True
isConcreteMode (Proof{}) = False
isConcreteMode CodeGen = False
data State = State { runMode :: SBVRunMode
, pathCond :: SBool
, rStdGen :: IORef StdGen
, rCInfo :: IORef [(String, CW)]
, rctr :: IORef Int
, rUsedKinds :: IORef KindSet
, rinps :: IORef [(Quantifier, NamedSymVar)]
, rConstraints :: IORef [SW]
, routs :: IORef [SW]
, rtblMap :: IORef TableMap
, spgm :: IORef SBVPgm
, rconstMap :: IORef CnstMap
, rexprMap :: IORef ExprMap
, rArrayMap :: IORef ArrayMap
, rUIMap :: IORef UIMap
, rCgMap :: IORef CgMap
, raxioms :: IORef [(String, [String])]
, rSWCache :: IORef (Cache SW)
, rAICache :: IORef (Cache Int)
}
getPathCondition :: State -> SBool
getPathCondition = pathCond
extendPathCondition :: State -> (SBool -> SBool) -> State
extendPathCondition st f = st{pathCond = f (pathCond st)}
inProofMode :: State -> Bool
inProofMode s = case runMode s of
Proof{} -> True
CodeGen -> False
Concrete{} -> False
getSBranchRunConfig :: State -> Maybe SMTConfig
getSBranchRunConfig st = case runMode st of
Proof (_, s) -> s
_ -> Nothing
data SBV a = SBV !Kind !(Either CW (Cached SW))
type SBool = SBV Bool
type SWord8 = SBV Word8
type SWord16 = SBV Word16
type SWord32 = SBV Word32
type SWord64 = SBV Word64
type SInt8 = SBV Int8
type SInt16 = SBV Int16
type SInt32 = SBV Int32
type SInt64 = SBV Int64
type SInteger = SBV Integer
type SReal = SBV AlgReal
type SFloat = SBV Float
type SDouble = SBV Double
nan :: Floating a => a
nan = 0/0
infinity :: Floating a => a
infinity = 1/0
sNaN :: (Floating a, SymWord a) => SBV a
sNaN = literal nan
sInfinity :: (Floating a, SymWord a) => SBV a
sInfinity = literal infinity
data RoundingMode = RoundNearestTiesToEven
| RoundNearestTiesToAway
| RoundTowardPositive
| RoundTowardNegative
| RoundTowardZero
instance Show (SBV a) where
show (SBV _ (Left c)) = show c
show (SBV k (Right _)) = "<symbolic> :: " ++ show k
instance Eq (SBV a) where
SBV _ (Left a) == SBV _ (Left b) = a == b
a == b = error $ "Comparing symbolic bit-vectors; Use (.==) instead. Received: " ++ show (a, b)
SBV _ (Left a) /= SBV _ (Left b) = a /= b
a /= b = error $ "Comparing symbolic bit-vectors; Use (./=) instead. Received: " ++ show (a, b)
instance HasKind a => HasKind (SBV a) where
kindOf (SBV k _) = k
incCtr :: State -> IO Int
incCtr s = do ctr <- readIORef (rctr s)
let i = ctr + 1
i `seq` writeIORef (rctr s) i
return ctr
throwDice :: State -> IO Double
throwDice st = do g <- readIORef (rStdGen st)
let (r, g') = randomR (0, 1) g
writeIORef (rStdGen st) g'
return r
newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted st nm t mbCode
| null nm || not (isAlpha (head nm)) || not (all validChar (tail nm))
= error $ "Bad uninterpreted constant name: " ++ show nm ++ ". Must be a valid identifier."
| True = do
uiMap <- readIORef (rUIMap st)
case nm `Map.lookup` uiMap of
Just t' -> if t /= t'
then error $ "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n"
++ " Current type : " ++ show t ++ "\n"
++ " Previously used at: " ++ show t'
else return ()
Nothing -> do modifyIORef (rUIMap st) (Map.insert nm t)
when (isJust mbCode) $ modifyIORef (rCgMap st) (Map.insert nm (fromJust mbCode))
where validChar x = isAlphaNum x || x `elem` "_"
newSW :: State -> Kind -> IO (SW, String)
newSW st k = do ctr <- incCtr st
let sw = SW k (NodeId ctr)
registerKind st k
return (sw, 's' : show ctr)
registerKind :: State -> Kind -> IO ()
registerKind st k
| KUserSort sortName _ <- k, sortName `elem` reserved
= error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name."
| True
= modifyIORef (rUsedKinds st) (Set.insert k)
where reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP", "FloatingPoint"]
newConst :: State -> CW -> IO SW
newConst st c = do
constMap <- readIORef (rconstMap st)
case c `Map.lookup` constMap of
Just sw -> return sw
Nothing -> do let k = kindOf c
(sw, _) <- newSW st k
modifyIORef (rconstMap st) (Map.insert c sw)
return sw
getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int
getTableIndex st at rt elts = do
tblMap <- readIORef (rtblMap st)
case elts `Map.lookup` tblMap of
Just (i, _, _) -> return i
Nothing -> do let i = Map.size tblMap
modifyIORef (rtblMap st) (Map.insert elts (i, at, rt))
return i
mkConstCW :: Integral a => Kind -> a -> CW
mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a))
mkConstCW k@(KBounded{}) a = normCW $ CW k (CWInteger (toInteger a))
mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a))
mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a)))
mkConstCW KFloat a = normCW $ CW KFloat (CWFloat (fromInteger (toInteger a)))
mkConstCW KDouble a = normCW $ CW KDouble (CWDouble (fromInteger (toInteger a)))
mkConstCW (KUserSort s _) a = error $ "Unexpected call to mkConstCW with uninterpreted kind: " ++ s ++ " with value: " ++ show (toInteger a)
newExpr :: State -> Kind -> SBVExpr -> IO SW
newExpr st k app = do
let e = reorder app
exprMap <- readIORef (rexprMap st)
case e `Map.lookup` exprMap of
Just sw -> return sw
Nothing -> do (sw, _) <- newSW st k
modifyIORef (spgm st) (\(SBVPgm xs) -> SBVPgm (xs S.|> (sw, e)))
modifyIORef (rexprMap st) (Map.insert e sw)
return sw
sbvToSW :: State -> SBV a -> IO SW
sbvToSW st (SBV _ (Left c)) = newConst st c
sbvToSW st (SBV _ (Right f)) = uncache f st
newtype Symbolic a = Symbolic (ReaderT State IO a)
deriving (Applicative, Functor, Monad, MonadIO, MonadReader State)
mkSymSBV :: forall a. (Random a, SymWord a) => Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBV = mkSymSBVWithRandom randomIO
mkSymSBVWithRandom :: forall a. SymWord a => IO (SBV a) -> Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBVWithRandom rand mbQ k mbNm = do
st <- ask
let q = case (mbQ, runMode st) of
(Just x, _) -> x
(Nothing, Concrete{}) -> ALL
(Nothing, Proof (True, _)) -> EX
(Nothing, Proof (False, _)) -> ALL
(Nothing, CodeGen) -> ALL
case runMode st of
Concrete _ | q == EX -> case mbNm of
Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: a)
Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: a)
Concrete _ -> do v@(SBV _ (Left cw)) <- liftIO rand
liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):)
return v
_ -> do (sw, internalName) <- liftIO $ newSW st k
let nm = maybe internalName id mbNm
liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)
return $ SBV k $ Right $ cache (const (return sw))
sbvToSymSW :: SBV a -> Symbolic SW
sbvToSymSW sbv = do
st <- ask
liftIO $ sbvToSW st sbv
class Outputtable a where
output :: a -> Symbolic a
instance Outputtable (SBV a) where
output i@(SBV _ (Left c)) = do
st <- ask
sw <- liftIO $ newConst st c
liftIO $ modifyIORef (routs st) (sw:)
return i
output i@(SBV _ (Right f)) = do
st <- ask
sw <- liftIO $ uncache f st
liftIO $ modifyIORef (routs st) (sw:)
return i
instance Outputtable a => Outputtable [a] where
output = mapM output
instance Outputtable () where
output = return
instance (Outputtable a, Outputtable b) => Outputtable (a, b) where
output = mlift2 (,) output output
instance (Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) where
output = mlift3 (,,) output output output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) where
output = mlift4 (,,,) output output output output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) where
output = mlift5 (,,,,) output output output output output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) where
output = mlift6 (,,,,,) output output output output output output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) where
output = mlift7 (,,,,,,) output output output output output output output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) where
output = mlift8 (,,,,,,,) output output output output output output output output
addAxiom :: String -> [String] -> Symbolic ()
addAxiom nm ax = do
st <- ask
liftIO $ modifyIORef (raxioms st) ((nm, ax) :)
runSymbolic :: (Bool, Maybe SMTConfig) -> Symbolic a -> IO Result
runSymbolic b c = snd `fmap` runSymbolic' (Proof b) c
runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)
runSymbolic' currentRunMode (Symbolic c) = do
ctr <- newIORef (2)
cInfo <- newIORef []
pgm <- newIORef (SBVPgm S.empty)
emap <- newIORef Map.empty
cmap <- newIORef Map.empty
inps <- newIORef []
outs <- newIORef []
tables <- newIORef Map.empty
arrays <- newIORef IMap.empty
uis <- newIORef Map.empty
cgs <- newIORef Map.empty
axioms <- newIORef []
swCache <- newIORef IMap.empty
aiCache <- newIORef IMap.empty
usedKinds <- newIORef Set.empty
cstrs <- newIORef []
rGen <- case currentRunMode of
Concrete g -> newIORef g
_ -> newStdGen >>= newIORef
let st = State { runMode = currentRunMode
, pathCond = SBV KBool (Left trueCW)
, rStdGen = rGen
, rCInfo = cInfo
, rctr = ctr
, rUsedKinds = usedKinds
, rinps = inps
, routs = outs
, rtblMap = tables
, spgm = pgm
, rconstMap = cmap
, rArrayMap = arrays
, rexprMap = emap
, rUIMap = uis
, rCgMap = cgs
, raxioms = axioms
, rSWCache = swCache
, rAICache = aiCache
, rConstraints = cstrs
}
_ <- newConst st falseCW
_ <- newConst st trueCW
r <- runReaderT c st
res <- extractSymbolicSimulationState st
return (r, res)
extractSymbolicSimulationState :: State -> IO Result
extractSymbolicSimulationState st@State{ spgm=pgm, rinps=inps, routs=outs, rtblMap=tables, rArrayMap=arrays, rUIMap=uis, raxioms=axioms
, rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints = cstrs} = do
SBVPgm rpgm <- readIORef pgm
inpsO <- reverse `fmap` readIORef inps
outsO <- reverse `fmap` readIORef outs
let swap (a, b) = (b, a)
cmp (a, _) (b, _) = a `compare` b
cnsts <- (sortBy cmp . map swap . Map.toList) `fmap` readIORef (rconstMap st)
tbls <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef tables
arrs <- IMap.toAscList `fmap` readIORef arrays
unint <- Map.toList `fmap` readIORef uis
axs <- reverse `fmap` readIORef axioms
knds <- readIORef usedKinds
cgMap <- Map.toList `fmap` readIORef cgs
traceVals <- reverse `fmap` readIORef cInfo
extraCstrs <- reverse `fmap` readIORef cstrs
return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO
constructUKind :: forall a. (Read a, G.Data a) => a -> Kind
constructUKind a = KUserSort sortName (mbEnumFields, dataType)
where dataType = G.dataTypeOf a
sortName = G.tyconUQname . G.dataTypeName $ dataType
constrs = G.dataTypeConstrs dataType
isEnumeration = not (null constrs) && all (null . G.constrFields) constrs
mbEnumFields
| isEnumeration = check constrs []
| True = Left $ sortName ++ "is not a finite non-empty enumeration"
check [] sofar = Right $ reverse sofar
check (c:cs) sofar = case checkConstr c of
Nothing -> check cs (show c : sofar)
Just s -> Left $ sortName ++ "." ++ show c ++ ": " ++ s
checkConstr c = case (reads (show c) :: [(a, String)]) of
((_, "") : _) -> Nothing
_ -> Just $ "not a nullary constructor"
class (HasKind a, Ord a) => SymWord a where
forall :: String -> Symbolic (SBV a)
forall_ :: Symbolic (SBV a)
mkForallVars :: Int -> Symbolic [SBV a]
exists :: String -> Symbolic (SBV a)
exists_ :: Symbolic (SBV a)
mkExistVars :: Int -> Symbolic [SBV a]
free :: String -> Symbolic (SBV a)
free_ :: Symbolic (SBV a)
mkFreeVars :: Int -> Symbolic [SBV a]
symbolic :: String -> Symbolic (SBV a)
symbolics :: [String] -> Symbolic [SBV a]
literal :: a -> SBV a
unliteral :: SBV a -> Maybe a
fromCW :: CW -> a
isConcrete :: SBV a -> Bool
isSymbolic :: SBV a -> Bool
isConcretely :: SBV a -> (a -> Bool) -> Bool
mbMaxBound, mbMinBound :: Maybe a
mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
forall = mkSymWord (Just ALL) . Just
forall_ = mkSymWord (Just ALL) Nothing
exists = mkSymWord (Just EX) . Just
exists_ = mkSymWord (Just EX) Nothing
free = mkSymWord Nothing . Just
free_ = mkSymWord Nothing Nothing
mkForallVars n = mapM (const forall_) [1 .. n]
mkExistVars n = mapM (const exists_) [1 .. n]
mkFreeVars n = mapM (const free_) [1 .. n]
symbolic = free
symbolics = mapM symbolic
unliteral (SBV _ (Left c)) = Just $ fromCW c
unliteral _ = Nothing
isConcrete (SBV _ (Left _)) = True
isConcrete _ = False
isSymbolic = not . isConcrete
isConcretely s p
| Just i <- unliteral s = p i
| True = False
mbMaxBound = Nothing
mbMinBound = Nothing
default literal :: Show a => a -> SBV a
literal x = let k@(KUserSort _ (conts, _)) = kindOf x
sx = show x
mbIdx = case conts of
Right xs -> sx `lookup` zip xs [0..]
_ -> Nothing
in SBV k (Left (CW k (CWUserSort (mbIdx, sx))))
default fromCW :: Read a => CW -> a
fromCW (CW _ (CWUserSort (_, s))) = read s
fromCW cw = error $ "Cannot convert CW " ++ show cw ++ " to kind " ++ show (kindOf (undefined :: a))
default mkSymWord :: (Read a, G.Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
mkSymWord mbQ mbNm = do
st <- ask
let k@(KUserSort sortName _) = constructUKind (undefined :: a)
liftIO $ registerKind st k
let q = case (mbQ, runMode st) of
(Just x, _) -> x
(Nothing, Proof (True, _)) -> EX
(Nothing, Proof (False, _)) -> ALL
(Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."
(Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode."
ctr <- liftIO $ incCtr st
let sw = SW k (NodeId ctr)
nm = maybe ('s':show ctr) id mbNm
liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)
return $ SBV k $ Right $ cache (const (return sw))
instance (Random a, SymWord a) => Random (SBV a) where
randomR (l, h) g = case (unliteral l, unliteral h) of
(Just lb, Just hb) -> let (v, g') = randomR (lb, hb) g in (literal (v :: a), g')
_ -> error $ "SBV.Random: Cannot generate random values with symbolic bounds"
random g = let (v, g') = random g in (literal (v :: a) , g')
class SymArray array where
newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)
newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)
readArray :: array a b -> SBV a -> SBV b
resetArray :: SymWord b => array a b -> SBV b -> array a b
writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b
mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b
data SArray a b = SArray (Kind, Kind) (Cached ArrayIndex)
type ArrayIndex = Int
instance (HasKind a, HasKind b) => Show (SArray a b) where
show (SArray{}) = "SArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">"
instance SymArray SArray where
newArray_ = declNewSArray (\t -> "array_" ++ show t)
newArray n = declNewSArray (const n)
readArray (SArray (_, bk) f) a = SBV bk $ Right $ cache r
where r st = do arr <- uncacheAI f st
i <- sbvToSW st a
newExpr st bk (SBVApp (ArrRead arr) [i])
resetArray (SArray ainfo f) b = SArray ainfo $ cache g
where g st = do amap <- readIORef (rArrayMap st)
val <- sbvToSW st b
i <- uncacheAI f st
let j = IMap.size amap
j `seq` modifyIORef (rArrayMap st) (IMap.insert j ("array_" ++ show j, ainfo, ArrayReset i val))
return j
writeArray (SArray ainfo f) a b = SArray ainfo $ cache g
where g st = do arr <- uncacheAI f st
addr <- sbvToSW st a
val <- sbvToSW st b
amap <- readIORef (rArrayMap st)
let j = IMap.size amap
j `seq` modifyIORef (rArrayMap st) (IMap.insert j ("array_" ++ show j, ainfo, ArrayMutate arr addr val))
return j
mergeArrays t (SArray ainfo a) (SArray _ b) = SArray ainfo $ cache h
where h st = do ai <- uncacheAI a st
bi <- uncacheAI b st
ts <- sbvToSW st t
amap <- readIORef (rArrayMap st)
let k = IMap.size amap
k `seq` modifyIORef (rArrayMap st) (IMap.insert k ("array_" ++ show k, ainfo, ArrayMerge ts ai bi))
return k
declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b)
declNewSArray mkNm mbInit = do
let aknd = kindOf (undefined :: a)
bknd = kindOf (undefined :: b)
st <- ask
amap <- liftIO $ readIORef $ rArrayMap st
let i = IMap.size amap
nm = mkNm i
actx <- liftIO $ case mbInit of
Nothing -> return $ ArrayFree Nothing
Just ival -> sbvToSW st ival >>= \sw -> return $ ArrayFree (Just sw)
liftIO $ modifyIORef (rArrayMap st) (IMap.insert i (nm, (aknd, bknd), actx))
return $ SArray (aknd, bknd) $ cache $ const $ return i
data SFunArray a b = SFunArray (SBV a -> SBV b)
instance (HasKind a, HasKind b) => Show (SFunArray a b) where
show (SFunArray _) = "SFunArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">"
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
mkSFunArray = SFunArray
imposeConstraint :: SBool -> Symbolic ()
imposeConstraint c = do st <- ask
case runMode st of
CodeGen -> error "SBV: constraints are not allowed in code-generation"
_ -> do liftIO $ do v <- sbvToSW st c
modifyIORef (rConstraints st) (v:)
addConstraint :: Maybe Double -> SBool -> SBool -> Symbolic ()
addConstraint Nothing c _ = imposeConstraint c
addConstraint (Just t) c c'
| t < 0 || t > 1
= error $ "SBV: pConstrain: Invalid probability threshold: " ++ show t ++ ", must be in [0, 1]."
| True
= do st <- ask
when (not (isConcreteMode (runMode st))) $ error "SBV: pConstrain only allowed in 'genTest' or 'quickCheck' contexts."
case () of
() | t > 0 && t < 1 -> liftIO (throwDice st) >>= \d -> imposeConstraint (if d <= t then c else c')
| t > 0 -> imposeConstraint c
| True -> imposeConstraint c'
newtype Cached a = Cached (State -> IO a)
cache :: (State -> IO a) -> Cached a
cache = Cached
uncache :: Cached SW -> State -> IO SW
uncache = uncacheGen rSWCache
uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
uncacheAI = uncacheGen rAICache
uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen getCache (Cached f) st = do
let rCache = getCache st
stored <- readIORef rCache
sn <- f `seq` makeStableName f
let h = hashStableName sn
case maybe Nothing (sn `lookup`) (h `IMap.lookup` stored) of
Just r -> return r
Nothing -> do r <- f st
r `seq` modifyIORef rCache (IMap.insertWith (++) h [(sn, r)])
return r
data SMTLibVersion = SMTLib1
| SMTLib2
deriving Eq
data SMTLibPgm = SMTLibPgm SMTLibVersion ( [(String, SW)]
, [String]
, [String])
instance NFData SMTLibVersion
instance NFData SMTLibPgm
instance Show SMTLibPgm where
show (SMTLibPgm _ (_, pre, post)) = intercalate "\n" $ pre ++ post
instance NFData CW where
rnf (CW x y) = x `seq` y `seq` ()
instance NFData Result where
rnf (Result kindInfo qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs)
= rnf kindInfo `seq` rnf qcInfo `seq` rnf cgs `seq` rnf inps
`seq` rnf consts `seq` rnf tbls `seq` rnf arrs
`seq` rnf uis `seq` rnf axs `seq` rnf pgm
`seq` rnf cstr `seq` rnf outs
instance NFData Kind
instance NFData ArrayContext
instance NFData SW
instance NFData SBVExpr
instance NFData Quantifier
instance NFData SBVType
instance NFData UnintKind
instance NFData a => NFData (Cached a) where
rnf (Cached f) = f `seq` ()
instance NFData a => NFData (SBV a) where
rnf (SBV x y) = rnf x `seq` rnf y `seq` ()
instance NFData SBVPgm
instance NFData SMTResult where
rnf (Unsatisfiable _) = ()
rnf (Satisfiable _ xs) = rnf xs `seq` ()
rnf (Unknown _ xs) = rnf xs `seq` ()
rnf (ProofError _ xs) = rnf xs `seq` ()
rnf (TimeOut _) = ()
instance NFData SMTModel where
rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` ()
instance NFData SMTScript where
rnf (SMTScript b m) = rnf b `seq` rnf m `seq` ()
data SMTLibLogic
= AUFLIA
| AUFLIRA
| AUFNIRA
| LRA
| UFLRA
| UFNIA
| QF_ABV
| QF_AUFBV
| QF_AUFLIA
| QF_AX
| QF_BV
| QF_IDL
| QF_LIA
| QF_LRA
| QF_NIA
| QF_NRA
| QF_RDL
| QF_UF
| QF_UFBV
| QF_UFIDL
| QF_UFLIA
| QF_UFLRA
| QF_UFNRA
| QF_FPABV
| QF_FPA
deriving Show
data Logic = PredefinedLogic SMTLibLogic
| CustomLogic String
instance Show Logic where
show (PredefinedLogic l) = show l
show (CustomLogic s) = s
data SolverCapabilities = SolverCapabilities {
capSolverName :: String
, mbDefaultLogic :: Maybe String
, supportsMacros :: Bool
, supportsProduceModels :: Bool
, supportsQuantifiers :: Bool
, supportsUninterpretedSorts :: Bool
, supportsUnboundedInts :: Bool
, supportsReals :: Bool
, supportsFloats :: Bool
, supportsDoubles :: Bool
}
data SMTConfig = SMTConfig {
verbose :: Bool
, timing :: Bool
, sBranchTimeOut :: Maybe Int
, timeOut :: Maybe Int
, printBase :: Int
, printRealPrec :: Int
, solverTweaks :: [String]
, satCmd :: String
, smtFile :: Maybe FilePath
, useSMTLib2 :: Bool
, solver :: SMTSolver
, roundingMode :: RoundingMode
, useLogic :: Maybe Logic
}
instance Show SMTConfig where
show = show . solver
data SMTModel = SMTModel {
modelAssocs :: [(String, CW)]
, modelArrays :: [(String, [String])]
, modelUninterps :: [(String, [String])]
}
deriving Show
data SMTResult = Unsatisfiable SMTConfig
| Satisfiable SMTConfig SMTModel
| Unknown SMTConfig SMTModel
| ProofError SMTConfig [String]
| TimeOut SMTConfig
data SMTScript = SMTScript {
scriptBody :: String
, scriptModel :: Maybe String
}
type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult
data Solver = Z3
| Yices
| Boolector
| CVC4
| MathSAT
deriving (Show, Enum, Bounded)
data SMTSolver = SMTSolver {
name :: Solver
, executable :: String
, options :: [String]
, engine :: SMTEngine
, xformExitCode :: ExitCode -> ExitCode
, capabilities :: SolverCapabilities
}
instance Show SMTSolver where
show = show . name
class SExecutable a where
sName_ :: a -> Symbolic ()
sName :: [String] -> a -> Symbolic ()
instance NFData a => SExecutable (Symbolic a) where
sName_ a = a >>= \r -> rnf r `seq` return ()
sName [] = sName_
sName xs = error $ "SBV.SExecutable.sName: Extra unmapped name(s): " ++ intercalate ", " xs
instance NFData a => SExecutable (SBV a) where
sName_ v = sName_ (output v)
sName xs v = sName xs (output v)
instance SExecutable () where
sName_ () = sName_ (output ())
sName xs () = sName xs (output ())
instance (NFData a, SymWord a) => SExecutable [SBV a] where
sName_ vs = sName_ (output vs)
sName xs vs = sName xs (output vs)
instance (NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) where
sName_ (a, b) = sName_ (output a >> output b)
sName _ = sName_
instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) where
sName_ (a, b, c) = sName_ (output a >> output b >> output c)
sName _ = sName_
instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) where
sName_ (a, b, c, d) = sName_ (output a >> output b >> output c >> output c >> output d)
sName _ = sName_
instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) where
sName_ (a, b, c, d, e) = sName_ (output a >> output b >> output c >> output d >> output e)
sName _ = sName_
instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where
sName_ (a, b, c, d, e, f) = sName_ (output a >> output b >> output c >> output d >> output e >> output f)
sName _ = sName_
instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where
sName_ (a, b, c, d, e, f, g) = sName_ (output a >> output b >> output c >> output d >> output e >> output f >> output g)
sName _ = sName_
instance (SymWord a, SExecutable p) => SExecutable (SBV a -> p) where
sName_ k = forall_ >>= \a -> sName_ $ k a
sName (s:ss) k = forall s >>= \a -> sName ss $ k a
sName [] k = sName_ k
instance (SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) where
sName_ k = forall_ >>= \a -> sName_ $ \b -> k (a, b)
sName (s:ss) k = forall s >>= \a -> sName ss $ \b -> k (a, b)
sName [] k = sName_ k
instance (SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) where
sName_ k = forall_ >>= \a -> sName_ $ \b c -> k (a, b, c)
sName (s:ss) k = forall s >>= \a -> sName ss $ \b c -> k (a, b, c)
sName [] k = sName_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) where
sName_ k = forall_ >>= \a -> sName_ $ \b c d -> k (a, b, c, d)
sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d -> k (a, b, c, d)
sName [] k = sName_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
sName_ k = forall_ >>= \a -> sName_ $ \b c d e -> k (a, b, c, d, e)
sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d e -> k (a, b, c, d, e)
sName [] k = sName_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
sName_ k = forall_ >>= \a -> sName_ $ \b c d e f -> k (a, b, c, d, e, f)
sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d e f -> k (a, b, c, d, e, f)
sName [] k = sName_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
sName_ k = forall_ >>= \a -> sName_ $ \b c d e f g -> k (a, b, c, d, e, f, g)
sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d e f g -> k (a, b, c, d, e, f, g)
sName [] k = sName_ k