module Data.SBV.BitVectors.Symbolic
( NodeId(..)
, SW(..), swKind, trueSW, falseSW
, Op(..), FPOp(..)
, Quantifier(..), needsExistentials
, RoundingMode(..)
, SBVType(..), newUninterpreted, addAxiom
, SVal(..), svKind
, svBitSize, svSigned
, svMkSymVar
, ArrayContext(..), ArrayInfo
, svToSW, svToSymSW, forceSWArg
, SBVExpr(..), newExpr, isCodeGenMode
, Cached, cache, uncache
, ArrayIndex, uncacheAI
, NamedSymVar
, getSValPathCondition, extendSValPathCondition
, getTableIndex
, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State
, inProofMode, SBVRunMode(..), Result(..)
, Logic(..), SMTLibLogic(..)
, addAssertion, addSValConstraint, internalConstraint, internalVariable
, SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension
, SolverCapabilities(..)
, extractSymbolicSimulationState
, SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine, getSBranchRunConfig
, outputSVal
, mkSValUserSort
, SArr(..), readSArr, resetSArr, writeSArr, mergeSArr, newSArr, eqSArr
) where
import Control.DeepSeq (NFData(..))
import Control.Monad (when, unless)
import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)
import Control.Monad.Trans (MonadIO, liftIO)
import Data.Char (isAlpha, isAlphaNum)
import Data.IORef (IORef, newIORef, modifyIORef, readIORef, writeIORef)
import Data.List (intercalate, sortBy)
import Data.Maybe (isJust, fromJust, fromMaybe)
import GHC.Stack.Compat
import qualified Data.Generics as G (Data(..))
import qualified Data.Typeable as T (Typeable)
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.Mem.StableName
import System.Random
import Data.SBV.BitVectors.Kind
import Data.SBV.BitVectors.Concrete
import Prelude ()
import Prelude.Compat
newtype NodeId = NodeId Int deriving (Eq, Ord)
data SW = SW Kind NodeId deriving (Eq, Ord)
instance Show SW where
show (SW _ (NodeId n))
| n < 0 = "s_" ++ show (abs n)
| True = 's' : show n
swKind :: SW -> Kind
swKind (SW k _) = k
forceSWArg :: SW -> IO ()
forceSWArg (SW k n) = k `seq` n `seq` return ()
falseSW :: SW
falseSW = SW KBool $ NodeId (2)
trueSW :: SW
trueSW = SW KBool $ NodeId (1)
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
| IntCast Kind Kind
| Uninterpreted String
| Label String
| IEEEFP FPOp
deriving (Eq, Ord)
data FPOp = FP_Cast Kind Kind SW
| FP_Reinterpret Kind Kind
| FP_Abs
| FP_Neg
| FP_Add
| FP_Sub
| FP_Mul
| FP_Div
| FP_FMA
| FP_Sqrt
| FP_Rem
| FP_RoundToIntegral
| FP_Min
| FP_Max
| FP_ObjEqual
| FP_IsNormal
| FP_IsSubnormal
| FP_IsZero
| FP_IsInfinite
| FP_IsNaN
| FP_IsNegative
| FP_IsPositive
deriving (Eq, Ord)
instance Show FPOp where
show (FP_Cast f t r) = "(FP_Cast: " ++ show f ++ " -> " ++ show t ++ "using RM [" ++ show r ++ "])"
show (FP_Reinterpret f t) = case (f, t) of
(KBounded False 32, KFloat) -> "(_ to_fp 8 24)"
(KBounded False 64, KDouble) -> "(_ to_fp 11 53)"
_ -> error $ "SBV.FP_Reinterpret: Unexpected conversion: " ++ show f ++ " to " ++ show t
show FP_Abs = "fp.abs"
show FP_Neg = "fp.neg"
show FP_Add = "fp.add"
show FP_Sub = "fp.sub"
show FP_Mul = "fp.mul"
show FP_Div = "fp.div"
show FP_FMA = "fp.fma"
show FP_Sqrt = "fp.sqrt"
show FP_Rem = "fp.rem"
show FP_RoundToIntegral = "fp.roundToIntegral"
show FP_Min = "fp.min"
show FP_Max = "fp.max"
show FP_ObjEqual = "="
show FP_IsNormal = "fp.isNormal"
show FP_IsSubnormal = "fp.isSubnormal"
show FP_IsZero = "fp.isZero"
show FP_IsInfinite = "fp.isInfinite"
show FP_IsNaN = "fp.isNaN"
show FP_IsNegative = "fp.isNegative"
show FP_IsPositive = "fp.isPositive"
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 (IntCast fr to) = "cast_" ++ show fr ++ "_" ++ show to
show (Uninterpreted i) = "[uninterpreted] " ++ i
show (Label s) = "[label] " ++ s
show (IEEEFP w) = show w
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, "#")
]
data Quantifier = ALL | EX deriving Eq
needsExistentials :: [Quantifier] -> Bool
needsExistentials = (EX `elem`)
newtype SBVType = SBVType [Kind]
deriving (Eq, Ord)
instance Show SBVType where
show (SBVType []) = error "SBV: internal error, empty SBVType"
show (SBVType xs) = intercalate " -> " $ map show xs
data SBVExpr = SBVApp !Op ![SW]
deriving (Eq, Ord)
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 Result = Result { reskinds :: Set.Set Kind
, resTraces :: [(String, CW)]
, resUISegs :: [(String, [String])]
, resInputs :: [(Quantifier, NamedSymVar)]
, resConsts :: [(SW, CW)]
, resTables :: [((Int, Kind, Kind), [SW])]
, resArrays :: [(Int, ArrayInfo)]
, resUOConsts :: [(String, SBVType)]
, resAxioms :: [(String, [String])]
, resAsgns :: SBVPgm
, resConstraints :: [SW]
, resAssertions :: [(String, Maybe CallStack, SW)]
, resOutputs :: [SW]
}
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 asserts 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
++ ["ASSERTIONS"]
++ map ((" "++) . shAssert) asserts
++ ["OUTPUTS"]
++ map ((" " ++) . show) os
where usorts = [sh s t | KUserSort s t <- Set.toList kinds]
where sh s (Left _, _) = s
sh s (Right es, _) = s ++ " (" ++ intercalate ", " es ++ ")"
shs sw = show sw ++ " :: " ++ show (swKind 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 ++ " :: " ++ show (swKind 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
shAssert (nm, stk, p) = " -- assertion: " ++ nm ++ " " ++ maybe "[No location]" showCallStack stk ++ ": " ++ show p
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 ++ " :: " ++ show (swKind s)
show (ArrayReset i s) = " reset array_" ++ show i ++ " with " ++ show s ++ " :: " ++ show (swKind s)
show (ArrayMutate i a b) = " cloned from array_" ++ show i ++ " with " ++ show a ++ " :: " ++ show (swKind a) ++ " |-> " ++ show b ++ " :: " ++ show (swKind 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 (Bool, 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)]
data SBVRunMode = Proof (Bool, SMTConfig)
| CodeGen
| Concrete StdGen
isConcreteMode :: State -> Bool
isConcreteMode State{runMode} = case runMode of
Concrete{} -> True
Proof{} -> False
CodeGen -> False
isCodeGenMode :: State -> Bool
isCodeGenMode State{runMode} = case runMode of
Concrete{} -> False
Proof{} -> False
CodeGen -> True
data State = State { runMode :: SBVRunMode
, pathCond :: SVal
, 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])]
, rAsserts :: IORef [(String, Maybe CallStack, SW)]
, rSWCache :: IORef (Cache SW)
, rAICache :: IORef (Cache Int)
}
getSValPathCondition :: State -> SVal
getSValPathCondition = pathCond
extendSValPathCondition :: State -> (SVal -> SVal) -> State
extendSValPathCondition 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) -> Just s
_ -> Nothing
data SVal = SVal !Kind !(Either CW (Cached SW))
svKind :: SVal -> Kind
svKind (SVal k _) = k
svBitSize :: SVal -> Int
svBitSize x =
case svKind x of
KBounded _ s -> s
_ -> error $ "svBitSize: invalid kind " ++ show (svKind x)
svSigned :: SVal -> Bool
svSigned x = kindHasSign (svKind x)
instance Show SVal where
show (SVal KBool (Left c)) = showCW False c
show (SVal k (Left c)) = showCW False c ++ " :: " ++ show k
show (SVal k (Right _)) = "<symbolic> :: " ++ show k
instance Eq SVal where
SVal _ (Left a) == SVal _ (Left b) = a == b
a == b = error $ "Comparing symbolic bit-vectors; Use (.==) instead. Received: " ++ show (a, b)
SVal _ (Left a) /= SVal _ (Left b) = a /= b
a /= b = error $ "Comparing symbolic bit-vectors; Use (./=) instead. Received: " ++ show (a, b)
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' -> when (t /= t') $ error $ "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n"
++ " Current type : " ++ show t ++ "\n"
++ " Previously used at: " ++ show t'
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` "_"
addAssertion :: State -> Maybe CallStack -> String -> SW -> IO ()
addAssertion st cs msg cond = modifyIORef (rAsserts st) ((msg, cs, cond):)
internalVariable :: State -> Kind -> IO SW
internalVariable st k = do (sw, nm) <- newSW st k
let q = case runMode st of
Proof (True, _) -> EX
_ -> ALL
modifyIORef (rinps st) ((q, (sw, "__internal_sbv_" ++ nm)):)
return sw
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", "fp"]
newConst :: State -> CW -> IO SW
newConst st c = do
constMap <- readIORef (rconstMap st)
let key = (isNeg0 (cwVal c), c)
case key `Map.lookup` constMap of
Just sw -> return sw
Nothing -> do let k = cwKind c
(sw, _) <- newSW st k
modifyIORef (rconstMap st) (Map.insert key sw)
return sw
where isNeg0 (CWFloat f) = isNegativeZero f
isNeg0 (CWDouble d) = isNegativeZero d
isNeg0 _ = False
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
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
svToSW :: State -> SVal -> IO SW
svToSW st (SVal _ (Left c)) = newConst st c
svToSW st (SVal _ (Right f)) = uncache f st
svToSymSW :: SVal -> Symbolic SW
svToSymSW sbv = do st <- ask
liftIO $ svToSW st sbv
newtype Symbolic a = Symbolic (ReaderT State IO a)
deriving (Applicative, Functor, Monad, MonadIO, MonadReader State)
svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> Symbolic SVal
svMkSymVar 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: " ++ show k
Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ show k
Concrete _ -> do cw <- liftIO (randomCW k)
liftIO $ modifyIORef (rCInfo st) ((fromMaybe "_" mbNm, cw):)
return (SVal k (Left cw))
_ -> do (sw, internalName) <- liftIO $ newSW st k
let nm = fromMaybe internalName mbNm
liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)
return $ SVal k $ Right $ cache (const (return sw))
mkSValUserSort :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic SVal
mkSValUserSort k mbQ mbNm = do
st <- ask
let (KUserSort sortName _) = k
liftIO $ registerKind st k
let q = case (mbQ, runMode st) of
(Just x, _) -> x
(Nothing, Proof (True, _)) -> EX
(Nothing, Proof (False, _)) -> ALL
(Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode."
(Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."
ctr <- liftIO $ incCtr st
let sw = SW k (NodeId ctr)
nm = fromMaybe ('s':show ctr) mbNm
liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):)
return $ SVal k $ Right $ cache (const (return sw))
addAxiom :: String -> [String] -> Symbolic ()
addAxiom nm ax = do
st <- ask
liftIO $ modifyIORef (raxioms st) ((nm, ax) :)
runSymbolic :: (Bool, SMTConfig) -> Symbolic a -> IO Result
runSymbolic m c = snd `fmap` runSymbolic' (Proof m) 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 []
asserts <- newIORef []
rGen <- case currentRunMode of
Concrete g -> newIORef g
_ -> newStdGen >>= newIORef
let st = State { runMode = currentRunMode
, pathCond = SVal 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
, rAsserts = asserts
}
_ <- 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
, rAsserts=asserts, 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)
swapc ((_, a), b) = (b, a)
cmp (a, _) (b, _) = a `compare` b
cnsts <- (sortBy cmp . map swapc . 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
assertions <- reverse `fmap` readIORef asserts
return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO
imposeConstraint :: SVal -> Symbolic ()
imposeConstraint c = do st <- ask
case runMode st of
CodeGen -> error "SBV: constraints are not allowed in code-generation"
_ -> liftIO $ internalConstraint st c
internalConstraint :: State -> SVal -> IO ()
internalConstraint st b = do v <- svToSW st b
modifyIORef (rConstraints st) (v:)
addSValConstraint :: Maybe Double -> SVal -> SVal -> Symbolic ()
addSValConstraint Nothing c _ = imposeConstraint c
addSValConstraint (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
unless (isConcreteMode 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'
outputSVal :: SVal -> Symbolic ()
outputSVal (SVal _ (Left c)) = do
st <- ask
sw <- liftIO $ newConst st c
liftIO $ modifyIORef (routs st) (sw:)
outputSVal (SVal _ (Right f)) = do
st <- ask
sw <- liftIO $ uncache f st
liftIO $ modifyIORef (routs st) (sw:)
data SArr = SArr (Kind, Kind) (Cached ArrayIndex)
readSArr :: SArr -> SVal -> SVal
readSArr (SArr (_, bk) f) a = SVal bk $ Right $ cache r
where r st = do arr <- uncacheAI f st
i <- svToSW st a
newExpr st bk (SBVApp (ArrRead arr) [i])
resetSArr :: SArr -> SVal -> SArr
resetSArr (SArr ainfo f) b = SArr ainfo $ cache g
where g st = do amap <- readIORef (rArrayMap st)
val <- svToSW 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
writeSArr :: SArr -> SVal -> SVal -> SArr
writeSArr (SArr ainfo f) a b = SArr ainfo $ cache g
where g st = do arr <- uncacheAI f st
addr <- svToSW st a
val <- svToSW 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
mergeSArr :: SVal -> SArr -> SArr -> SArr
mergeSArr t (SArr ainfo a) (SArr _ b) = SArr ainfo $ cache h
where h st = do ai <- uncacheAI a st
bi <- uncacheAI b st
ts <- svToSW 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
newSArr :: (Kind, Kind) -> (Int -> String) -> Maybe SVal -> Symbolic SArr
newSArr ainfo mkNm mbInit = do
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 -> svToSW st ival >>= \sw -> return $ ArrayFree (Just sw)
liftIO $ modifyIORef (rArrayMap st) (IMap.insert i (nm, ainfo, actx))
return $ SArr ainfo $ cache $ const $ return i
eqSArr :: SArr -> SArr -> SVal
eqSArr (SArr _ a) (SArr _ b) = SVal KBool $ Right $ cache c
where c st = do ai <- uncacheAI a st
bi <- uncacheAI b st
newExpr st KBool (SBVApp (ArrEq ai bi) [])
newtype Cached a = Cached (State -> IO a)
cache :: (State -> IO a) -> Cached a
cache = Cached
uncache :: Cached SW -> State -> IO SW
uncache = uncacheGen rSWCache
type ArrayIndex = Int
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 = SMTLib2
deriving (Bounded, Enum, Eq, Show)
smtLibVersionExtension :: SMTLibVersion -> String
smtLibVersionExtension SMTLib2 = "smt2"
data SMTLibPgm = SMTLibPgm SMTLibVersion ( [(String, SW)]
, [String]
, [String])
instance NFData SMTLibVersion where rnf a = seq a ()
instance NFData SMTLibPgm where rnf a = seq a ()
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 CallStack where
rnf _ = ()
instance NFData Result where
rnf (Result kindInfo qcInfo cgs inps consts tbls arrs uis axs pgm cstr asserts 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 asserts `seq` rnf outs
instance NFData Kind where rnf a = seq a ()
instance NFData ArrayContext where rnf a = seq a ()
instance NFData SW where rnf a = seq a ()
instance NFData SBVExpr where rnf a = seq a ()
instance NFData Quantifier where rnf a = seq a ()
instance NFData SBVType where rnf a = seq a ()
instance NFData a => NFData (Cached a) where
rnf (Cached f) = f `seq` ()
instance NFData SVal where
rnf (SVal x y) = rnf x `seq` rnf y `seq` ()
instance NFData SBVPgm where rnf a = seq a ()
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) = rnf assocs `seq` ()
instance NFData SMTScript where
rnf (SMTScript b m) = rnf b `seq` rnf m `seq` ()
data SMTLibLogic
= AUFLIA
| AUFLIRA
| AUFNIRA
| LRA
| 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
| UFLRA
| UFNIA
| QF_FPBV
| QF_FP
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 RoundingMode = RoundNearestTiesToEven
| RoundNearestTiesToAway
| RoundTowardPositive
| RoundTowardNegative
| RoundTowardZero
deriving (Eq, Ord, Show, Read, T.Typeable, G.Data, Bounded, Enum)
data SMTConfig = SMTConfig {
verbose :: Bool
, timing :: Bool
, sBranchTimeOut :: Maybe Int
, timeOut :: Maybe Int
, printBase :: Int
, printRealPrec :: Int
, solverTweaks :: [String]
, satCmd :: String
, smtFile :: Maybe FilePath
, smtLibVersion :: SMTLibVersion
, solver :: SMTSolver
, roundingMode :: RoundingMode
, useLogic :: Maybe Logic
}
instance Show SMTConfig where
show = show . solver
data SMTModel = SMTModel {
modelAssocs :: [(String, CW)]
}
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)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult
data Solver = Z3
| Yices
| Boolector
| CVC4
| MathSAT
| ABC
deriving (Show, Enum, Bounded)
data SMTSolver = SMTSolver {
name :: Solver
, executable :: String
, options :: [String]
, engine :: SMTEngine
, capabilities :: SolverCapabilities
}
instance Show SMTSolver where
show = show . name