{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE NamedFieldPuns #-}
module Data.SBV.SMT.SMT (
Modelable(..)
, SatModel(..), genParse
, extractModels, getModelValues
, getModelDictionaries, getModelUninterpretedValues
, displayModels, showModel
, standardEngine
, ThmResult(..)
, SatResult(..)
, AllSatResult(..)
, SafeResult(..)
, OptimizeResult(..)
)
where
import qualified Control.Exception as C
import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)
import Control.DeepSeq (NFData(..))
import Control.Monad (zipWithM)
import Data.Char (isSpace)
import Data.Maybe (fromMaybe)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.List (intercalate, isPrefixOf)
import Data.Word (Word8, Word16, Word32, Word64)
import Data.IORef (readIORef, writeIORef)
import Data.Time (getZonedTime, defaultTimeLocale, formatTime, diffUTCTime, getCurrentTime)
import System.Directory (findExecutable)
import System.Environment (getEnv)
import System.Exit (ExitCode(..))
import System.IO (hClose, hFlush, hPutStrLn, hGetContents, hGetLine)
import System.Process (runInteractiveProcess, waitForProcess, terminateProcess)
import qualified Data.Map as M
import Data.SBV.Core.AlgReals
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (SMTEngine, State(..))
import Data.SBV.SMT.Utils (showTimeoutValue, alignPlain, alignDiagnostic, debug, mergeSExpr, SMTException(..))
import Data.SBV.Utils.PrettyNum
import Data.SBV.Utils.Lib (joinArgs, splitArgs)
import Data.SBV.Utils.SExpr (parenDeficit)
import Data.SBV.Utils.TDiff (Timing(..), showTDiff)
import qualified System.Timeout as Timeout (timeout)
resultConfig :: SMTResult -> SMTConfig
resultConfig (Unsatisfiable c _) = c
resultConfig (Satisfiable c _) = c
resultConfig (SatExtField c _) = c
resultConfig (Unknown c _) = c
resultConfig (ProofError c _) = c
newtype ThmResult = ThmResult SMTResult
deriving NFData
newtype SatResult = SatResult SMTResult
deriving NFData
newtype AllSatResult = AllSatResult (Bool, Bool, [SMTResult])
newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
data OptimizeResult = LexicographicResult SMTResult
| ParetoResult (Bool, [SMTResult])
| IndependentResult [(String, SMTResult)]
instance Show ThmResult where
show (ThmResult r) = showSMTResult "Q.E.D."
"Unknown"
"Falsifiable" "Falsifiable. Counter-example:\n" "Falsifiable in an extension field:\n" r
instance Show SatResult where
show (SatResult r) = showSMTResult "Unsatisfiable"
"Unknown"
"Satisfiable" "Satisfiable. Model:\n" "Satisfiable in an extension field. Model:\n" r
instance Show SafeResult where
show (SafeResult (mbLoc, msg, r)) = showSMTResult (tag "No violations detected")
(tag "Unknown")
(tag "Violated") (tag "Violated. Model:\n") (tag "Violated in an extension field:\n") r
where loc = maybe "" (++ ": ") mbLoc
tag s = loc ++ msg ++ ": " ++ s
instance Show AllSatResult where
show (AllSatResult (l, e, xs)) = go (0::Int) xs
where uniqueWarn | e = " (Unique up to prefix existentials.)"
| True = ""
go c (s:ss) = let c' = c+1
(ok, o) = sh c' s
in c' `seq` if ok then o ++ "\n" ++ go c' ss else o
go c [] = case (l, c) of
(True, _) -> "Search stopped since model count request was reached." ++ uniqueWarn
(False, 0) -> "No solutions found."
(False, 1) -> "This is the only solution." ++ uniqueWarn
(False, _) -> "Found " ++ show c ++ " different solutions." ++ uniqueWarn
sh i c = (ok, showSMTResult "Unsatisfiable"
"Unknown"
("Solution #" ++ show i ++ ":\nSatisfiable") ("Solution #" ++ show i ++ ":\n")
("Solution $" ++ show i ++ " in an extension field:\n")
c)
where ok = case c of
Satisfiable{} -> True
_ -> False
instance Show OptimizeResult where
show res = case res of
LexicographicResult r -> sh id r
IndependentResult rs -> multi "objectives" (map (uncurry shI) rs)
ParetoResult (False, [r]) -> sh (\s -> "Unique pareto front: " ++ s) r
ParetoResult (False, rs) -> multi "pareto optimal values" (zipWith shP [(1::Int)..] rs)
ParetoResult (True, rs) -> multi "pareto optimal values" (zipWith shP [(1::Int)..] rs)
++ "\n*** Note: Pareto-front extraction was terminated before stream was ended as requested by the user."
++ "\n*** There might be other (potentially infinitely more) results."
where multi w [] = "There are no " ++ w ++ " to display models for."
multi _ xs = intercalate "\n" xs
shI n = sh (\s -> "Objective " ++ show n ++ ": " ++ s)
shP i = sh (\s -> "Pareto front #" ++ show i ++ ": " ++ s)
sh tag = showSMTResult (tag "Unsatisfiable.")
(tag "Unknown.")
(tag "Optimal with no assignments.")
(tag "Optimal model:" ++ "\n")
(tag "Optimal in an extension field:" ++ "\n")
class SatModel a where
parseCWs :: [CW] -> Maybe (a, [CW])
cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])
cvtModel f x = x >>= \(a, r) -> f a >>= \b -> return (b, r)
default parseCWs :: Read a => [CW] -> Maybe (a, [CW])
parseCWs (CW _ (CWUserSort (_, s)) : r) = Just (read s, r)
parseCWs _ = Nothing
genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
genParse k (x@(CW _ (CWInteger i)):r) | kindOf x == k = Just (fromIntegral i, r)
genParse _ _ = Nothing
instance SatModel () where
parseCWs xs = return ((), xs)
instance SatModel Bool where
parseCWs xs = do (x, r) <- genParse KBool xs
return ((x :: Integer) /= 0, r)
instance SatModel Word8 where
parseCWs = genParse (KBounded False 8)
instance SatModel Int8 where
parseCWs = genParse (KBounded True 8)
instance SatModel Word16 where
parseCWs = genParse (KBounded False 16)
instance SatModel Int16 where
parseCWs = genParse (KBounded True 16)
instance SatModel Word32 where
parseCWs = genParse (KBounded False 32)
instance SatModel Int32 where
parseCWs = genParse (KBounded True 32)
instance SatModel Word64 where
parseCWs = genParse (KBounded False 64)
instance SatModel Int64 where
parseCWs = genParse (KBounded True 64)
instance SatModel Integer where
parseCWs = genParse KUnbounded
instance SatModel AlgReal where
parseCWs (CW KReal (CWAlgReal i) : r) = Just (i, r)
parseCWs _ = Nothing
instance SatModel Float where
parseCWs (CW KFloat (CWFloat i) : r) = Just (i, r)
parseCWs _ = Nothing
instance SatModel Double where
parseCWs (CW KDouble (CWDouble i) : r) = Just (i, r)
parseCWs _ = Nothing
instance SatModel CW where
parseCWs (cw : r) = Just (cw, r)
parseCWs [] = Nothing
instance SatModel RoundingMode
instance SatModel a => SatModel [a] where
parseCWs [] = Just ([], [])
parseCWs xs = case parseCWs xs of
Just (a, ys) -> case parseCWs ys of
Just (as, zs) -> Just (a:as, zs)
Nothing -> Just ([], ys)
Nothing -> Just ([], xs)
instance (SatModel a, SatModel b) => SatModel (a, b) where
parseCWs as = do (a, bs) <- parseCWs as
(b, cs) <- parseCWs bs
return ((a, b), cs)
instance (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c), ds) <- parseCWs bs
return ((a, b, c), ds)
instance (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d), es) <- parseCWs bs
return ((a, b, c, d), es)
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d, e), fs) <- parseCWs bs
return ((a, b, c, d, e), fs)
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d, e, f), gs) <- parseCWs bs
return ((a, b, c, d, e, f), gs)
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d, e, f, g), hs) <- parseCWs bs
return ((a, b, c, d, e, f, g), hs)
class Modelable a where
modelExists :: a -> Bool
getModelAssignment :: SatModel b => a -> Either String (Bool, b)
getModelDictionary :: a -> M.Map String CW
getModelValue :: SymWord b => String -> a -> Maybe b
getModelValue v r = fromCW `fmap` (v `M.lookup` getModelDictionary r)
getModelUninterpretedValue :: String -> a -> Maybe String
getModelUninterpretedValue v r = case v `M.lookup` getModelDictionary r of
Just (CW _ (CWUserSort (_, s))) -> Just s
_ -> Nothing
extractModel :: SatModel b => a -> Maybe b
extractModel a = case getModelAssignment a of
Right (_, b) -> Just b
_ -> Nothing
getModelObjectives :: a -> M.Map String GeneralizedCW
getModelObjectiveValue :: String -> a -> Maybe GeneralizedCW
getModelObjectiveValue v r = v `M.lookup` getModelObjectives r
extractModels :: SatModel a => AllSatResult -> [a]
extractModels (AllSatResult (_, _, xs)) = [ms | Right (_, ms) <- map getModelAssignment xs]
getModelDictionaries :: AllSatResult -> [M.Map String CW]
getModelDictionaries (AllSatResult (_, _, xs)) = map getModelDictionary xs
getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]
getModelValues s (AllSatResult (_, _, xs)) = map (s `getModelValue`) xs
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
getModelUninterpretedValues s (AllSatResult (_, _, xs)) = map (s `getModelUninterpretedValue`) xs
instance Modelable ThmResult where
getModelAssignment (ThmResult r) = getModelAssignment r
modelExists (ThmResult r) = modelExists r
getModelDictionary (ThmResult r) = getModelDictionary r
getModelObjectives (ThmResult r) = getModelObjectives r
instance Modelable SatResult where
getModelAssignment (SatResult r) = getModelAssignment r
modelExists (SatResult r) = modelExists r
getModelDictionary (SatResult r) = getModelDictionary r
getModelObjectives (SatResult r) = getModelObjectives r
instance Modelable SMTResult where
getModelAssignment (Unsatisfiable _ _) = Left "SBV.getModelAssignment: Unsatisfiable result"
getModelAssignment (Satisfiable _ m) = Right (False, parseModelOut m)
getModelAssignment (SatExtField _ _) = Left "SBV.getModelAssignment: The model is in an extension field"
getModelAssignment (Unknown _ m) = Left $ "SBV.getModelAssignment: Solver state is unknown: " ++ m
getModelAssignment (ProofError _ s) = error $ unlines $ "Backend solver complains: " : s
modelExists Satisfiable{} = True
modelExists Unknown{} = False
modelExists _ = False
getModelDictionary Unsatisfiable{} = M.empty
getModelDictionary (Satisfiable _ m) = M.fromList (modelAssocs m)
getModelDictionary SatExtField{} = M.empty
getModelDictionary Unknown{} = M.empty
getModelDictionary ProofError{} = M.empty
getModelObjectives Unsatisfiable{} = M.empty
getModelObjectives (Satisfiable _ m) = M.fromList (modelObjectives m)
getModelObjectives (SatExtField _ m) = M.fromList (modelObjectives m)
getModelObjectives Unknown{} = M.empty
getModelObjectives ProofError{} = M.empty
parseModelOut :: SatModel a => SMTModel -> a
parseModelOut m = case parseCWs [c | (_, c) <- modelAssocs m] of
Just (x, []) -> x
Just (_, ys) -> error $ "SBV.parseModelOut: Partially constructed model; remaining elements: " ++ show ys
Nothing -> error $ "SBV.parseModelOut: Cannot construct a model from: " ++ show m
displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels disp (AllSatResult (_, _, ms)) = do
inds <- zipWithM display [a | Right a <- map (getModelAssignment . SatResult) ms] [(1::Int)..]
return $ last (0:inds)
where display r i = disp i r >> return i
showSMTResult :: String -> String -> String -> String -> String -> SMTResult -> String
showSMTResult unsatMsg unkMsg satMsg satMsgModel satExtMsg result = case result of
Unsatisfiable _ uc -> unsatMsg ++ showUnsatCore uc
Satisfiable _ (SMTModel _ []) -> satMsg
Satisfiable _ m -> satMsgModel ++ showModel cfg m
SatExtField _ (SMTModel b _) -> satExtMsg ++ showModelDictionary cfg b
Unknown _ r -> unkMsg ++ ".\n" ++ " Reason: " `alignPlain` r
ProofError _ [] -> "*** An error occurred. No additional information available. Try running in verbose mode"
ProofError _ ls -> "*** An error occurred.\n" ++ intercalate "\n" (map ("*** " ++) ls)
where cfg = resultConfig result
showUnsatCore Nothing = ""
showUnsatCore (Just xs) = ". Unsat core:\n" ++ intercalate "\n" [" " ++ x | x <- xs]
showModel :: SMTConfig -> SMTModel -> String
showModel cfg model = showModelDictionary cfg [(n, RegularCW c) | (n, c) <- modelAssocs model]
showModelDictionary :: SMTConfig -> [(String, GeneralizedCW)] -> String
showModelDictionary cfg allVars
| null allVars
= "[There are no variables bound by the model.]"
| null relevantVars
= "[There are no model-variables bound by the model.]"
| True
= intercalate "\n" . display . map shM $ relevantVars
where relevantVars = filter (not . ignore) allVars
ignore (s, _) = "__internal_sbv_" `isPrefixOf` s || isNonModelVar cfg s
shM (s, RegularCW v) = let vs = shCW cfg v in ((length s, s), (vlength vs, vs))
shM (s, other) = let vs = show other in ((length s, s), (vlength vs, vs))
display svs = map line svs
where line ((_, s), (_, v)) = " " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - lTrimRight (valPart v)) v
nameWidth = maximum $ 0 : [l | ((l, _), _) <- svs]
valWidth = maximum $ 0 : [l | (_, (l, _)) <- svs]
right p s = s ++ replicate p ' '
left p s = replicate p ' ' ++ s
vlength s = case dropWhile (/= ':') (reverse (takeWhile (/= '\n') s)) of
(':':':':r) -> length (dropWhile isSpace r)
_ -> length s
valPart "" = ""
valPart (':':':':_) = ""
valPart (x:xs) = x : valPart xs
lTrimRight = length . dropWhile isSpace . reverse
shCW :: SMTConfig -> CW -> String
shCW = sh . printBase
where sh 2 = binS
sh 10 = show
sh 16 = hexS
sh n = \w -> show w ++ " -- Ignoring unsupported printBase " ++ show n ++ ", use 2, 10, or 16."
pipeProcess :: SMTConfig -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
pipeProcess cfg ctx execName opts pgm continuation = do
mbExecPath <- findExecutable execName
case mbExecPath of
Nothing -> error $ unlines [ "Unable to locate executable for " ++ show (name (solver cfg))
, "Executable specified: " ++ show execName
]
Just execPath -> runSolver cfg ctx execPath opts pgm continuation
`C.catches`
[ C.Handler (\(e :: SMTException) -> C.throwIO e)
, C.Handler (\(e :: C.ErrorCall) -> C.throwIO e)
, C.Handler (\(e :: C.SomeException) -> error $ unlines [ "Failed to start the external solver:\n" ++ show e
, "Make sure you can start " ++ show execPath
, "from the command line without issues."
])
]
standardEngine :: String
-> String
-> SMTEngine
standardEngine envName envOptName cfg ctx pgm continuation = do
execName <- getEnv envName `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))
execOpts <- (splitArgs `fmap` getEnv envOptName) `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg) cfg))
let cfg' = cfg {solver = (solver cfg) {executable = execName, options = const execOpts}}
standardSolver cfg' ctx pgm continuation
standardSolver :: SMTConfig
-> State
-> String
-> (State -> IO a)
-> IO a
standardSolver config ctx pgm continuation = do
let msg s = debug config ["** " ++ s]
smtSolver= solver config
exec = executable smtSolver
opts = options smtSolver config
msg $ "Calling: " ++ (exec ++ (if null opts then "" else " ") ++ joinArgs opts)
rnf pgm `seq` pipeProcess config ctx exec opts pgm continuation
data SolverLine = SolverRegular String
| SolverTimeout String
| SolverException String
runSolver :: SMTConfig -> State -> FilePath -> [String] -> String -> (State -> IO a) -> IO a
runSolver cfg ctx execPath opts pgm continuation
= do let nm = show (name (solver cfg))
msg = debug cfg . map ("*** " ++)
(send, ask, getResponseFromSolver, terminateSolver, cleanUp, pid) <- do
(inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing
let
send :: Maybe Int -> String -> IO ()
send mbTimeOut command
| parenDeficit command /= 0
= error $ unlines [ ""
, "*** Data.SBV: Unbalanced input detected."
, "***"
, "*** Sending: " ++ command
, "***"
, "*** This is most likely an SBV bug. Please report!"
]
| True
= do hPutStrLn inh command
hFlush inh
recordTranscript (transcript cfg) $ Left (command, mbTimeOut)
ask :: Maybe Int -> String -> IO String
ask mbTimeOut command =
let cmd = dropWhile isSpace command
in if null cmd || ";" `isPrefixOf` cmd
then return "success"
else do send mbTimeOut command
getResponseFromSolver (Just command) mbTimeOut
getResponseFromSolver :: Maybe String -> Maybe Int -> IO String
getResponseFromSolver mbCommand mbTimeOut = do
response <- go True 0 []
let collated = intercalate "\n" $ reverse response
recordTranscript (transcript cfg) $ Right collated
return collated
where safeGetLine isFirst h =
let timeOutToUse | isFirst = mbTimeOut
| True = Just 5000000
timeOutMsg t | isFirst = "User specified timeout of " ++ showTimeoutValue t ++ " exceeded."
| True = "A multiline complete response wasn't received before " ++ showTimeoutValue t ++ " exceeded."
getFullLine :: IO String
getFullLine = intercalate "\n" . reverse <$> collect False []
where collect inString sofar = do ln <- hGetLine h
let walk inside [] = inside
walk inside ('"':cs) = walk (not inside) cs
walk inside (_:cs) = walk inside cs
stillInside = walk inString ln
sofar' = ln : sofar
if stillInside
then collect True sofar'
else return sofar'
in case timeOutToUse of
Nothing -> SolverRegular <$> getFullLine
Just t -> do r <- Timeout.timeout t getFullLine
case r of
Just l -> return $ SolverRegular l
Nothing -> return $ SolverTimeout $ timeOutMsg t
go isFirst i sofar = do
errln <- safeGetLine isFirst outh `C.catch` (\(e :: C.SomeException) -> return (SolverException (show e)))
case errln of
SolverRegular ln -> let need = i + parenDeficit ln
empty = case dropWhile isSpace ln of
[] -> True
(';':_) -> True
_ -> False
in case (empty, need <= 0) of
(True, _) -> do debug cfg ["[SKIP] " `alignPlain` ln]
go isFirst need sofar
(False, False) -> go False need (ln:sofar)
(False, True) -> return (ln:sofar)
SolverException e -> error $ unlines $ [""
, "*** Error : " ++ e
, "*** Executable: " ++ execPath
, "*** Options : " ++ joinArgs opts
]
++ [ "*** Request : " `alignDiagnostic` command | Just command <- [mbCommand]]
++ [ "*** Response : " `alignDiagnostic` unlines (reverse sofar) | not $ null sofar ]
++ [ "***"
, "*** Giving up!"
]
SolverTimeout e -> do terminateProcess pid
error $ unlines $ [ ""
, "*** Data.SBV: Timeout."
, "***"
, "*** " ++ e
]
++ [ "*** Response so far: " `alignDiagnostic` unlines (reverse sofar) | not $ null sofar]
++ [ "*** Last command sent was: " `alignDiagnostic` command | Just command <- [mbCommand]]
++ [ "*** Run with 'verbose=True' for further information" | not (verbose cfg)]
++ [ "***"
, "*** Giving up!"
]
terminateSolver = do hClose inh
outMVar <- newEmptyMVar
out <- hGetContents outh `C.catch` (\(e :: C.SomeException) -> return (show e))
_ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
err <- hGetContents errh `C.catch` (\(e :: C.SomeException) -> return (show e))
_ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
takeMVar outMVar
takeMVar outMVar
hClose outh `C.catch` (\(_ :: C.SomeException) -> return ())
hClose errh `C.catch` (\(_ :: C.SomeException) -> return ())
ex <- waitForProcess pid `C.catch` (\(_ :: C.SomeException) -> return (ExitFailure (-999)))
return (out, err, ex)
cleanUp
= do (out, err, ex) <- terminateSolver
msg $ [ "Solver : " ++ nm
, "Exit code: " ++ show ex
]
++ [ "Std-out : " ++ intercalate "\n " (lines out) | not (null out)]
++ [ "Std-err : " ++ intercalate "\n " (lines err) | not (null err)]
case ex of
ExitSuccess -> return ()
_ -> if ignoreExitCode cfg
then msg ["Ignoring non-zero exit code of " ++ show ex ++ " per user request!"]
else error $ unlines $ [ ""
, "*** Failed to complete the call to " ++ nm ++ ":"
, "*** Executable : " ++ execPath
, "*** Options : " ++ joinArgs opts
, "*** Exit code : " ++ show ex
]
++ [ "*** Std-out : " ++ intercalate "\n " (lines out)]
++ [ "*** Std-err : " ++ intercalate "\n " (lines err)]
++ ["Giving up.."]
return (send, ask, getResponseFromSolver, terminateSolver, cleanUp, pid)
let executeSolver = do let sendAndGetSuccess :: Maybe Int -> String -> IO ()
sendAndGetSuccess mbTimeOut l
| not (supportsCustomQueries (capabilities (solver cfg)))
= do send mbTimeOut l
debug cfg ["[ISSUE] " `alignPlain` l]
| True
= do r <- ask mbTimeOut l
case words r of
["success"] -> debug cfg ["[GOOD] " `alignPlain` l]
_ -> do debug cfg ["[FAIL] " `alignPlain` l]
let isOption = "(set-option" `isPrefixOf` dropWhile isSpace l
reason | isOption = [ "Backend solver reports it does not support this option."
, "Check the spelling, and if correct please report this as a"
, "bug/feature request with the solver!"
]
| True = [ "Check solver response for further information. If your code is correct,"
, "please report this as an issue either with SBV or the solver itself!"
]
mbExtras <- (Right <$> getResponseFromSolver Nothing (Just 5000000)) `C.catch` (\(e :: C.SomeException) -> return (Left (show e)))
let extras = case mbExtras of
Left _ -> []
Right xs -> xs
(outOrig, errOrig, ex) <- terminateSolver
let out = intercalate "\n" . lines $ outOrig
err = intercalate "\n" . lines $ errOrig
exc = SMTException { smtExceptionDescription = "Data.SBV: Unexpected non-success response from " ++ nm
, smtExceptionSent = l
, smtExceptionExpected = "success"
, smtExceptionReceived = r ++ "\n" ++ extras
, smtExceptionStdOut = out
, smtExceptionStdErr = Just err
, smtExceptionExitCode = Just ex
, smtExceptionConfig = cfg { solver = (solver cfg) {executable = execPath } }
, smtExceptionReason = Just reason
, smtExceptionHint = Nothing
}
C.throwIO exc
sendAndGetSuccess Nothing "; Automatically generated by SBV. Do not edit."
let backend = name $ solver cfg
if not (supportsCustomQueries (capabilities (solver cfg)))
then debug cfg ["** Skipping heart-beat for the solver " ++ show backend]
else do let heartbeat = "(set-option :print-success true)"
r <- ask (Just 5000000) heartbeat
case words r of
["success"] -> debug cfg ["[GOOD] " ++ heartbeat]
["unsupported"] -> error $ unlines [ ""
, "*** Backend solver (" ++ show backend ++ ") does not support the command:"
, "***"
, "*** (set-option :print-success true)"
, "***"
, "*** SBV relies on this feature to coordinate communication!"
, "*** Please request this as a feature!"
]
_ -> error $ unlines [ ""
, "*** Data.SBV: Failed to initiate contact with the solver!"
, "***"
, "*** Sent : " ++ heartbeat
, "*** Expected: success"
, "*** Received: " ++ r
, "***"
, "*** Try running in debug mode for further information."
]
if not (supportsGlobalDecls (capabilities (solver cfg)))
then debug cfg [ "** Backend solver " ++ show backend ++ " does not support global decls."
, "** Some incremental calls, such as pop, will be limited."
]
else sendAndGetSuccess Nothing "(set-option :global-declarations true)"
mapM_ (sendAndGetSuccess Nothing) (mergeSExpr (lines pgm))
let qs = QueryState { queryAsk = ask
, querySend = send
, queryRetrieveResponse = getResponseFromSolver Nothing
, queryConfig = cfg
, queryTerminate = cleanUp
, queryTimeOutValue = Nothing
, queryAssertionStackDepth = 0
}
qsp = queryState ctx
mbQS <- readIORef qsp
case mbQS of
Nothing -> writeIORef qsp (Just qs)
Just _ -> error $ unlines [ ""
, "Data.SBV: Impossible happened, query-state was already set."
, "Please report this as a bug!"
]
continuation ctx
let launchSolver = do startTranscript (transcript cfg) cfg
r <- executeSolver
finalizeTranscript (transcript cfg) Nothing
recordEndTime cfg ctx
return r
launchSolver `C.catch` (\(e :: C.SomeException) -> do terminateProcess pid
ec <- waitForProcess pid
recordException (transcript cfg) (show e)
finalizeTranscript (transcript cfg) (Just ec)
recordEndTime cfg ctx
C.throwIO e)
recordEndTime :: SMTConfig -> State -> IO ()
recordEndTime SMTConfig{timing} state = case timing of
NoTiming -> return ()
PrintTiming -> do e <- elapsed
putStrLn $ "*** SBV: Elapsed time: " ++ showTDiff e
SaveTiming here -> writeIORef here =<< elapsed
where elapsed = getCurrentTime >>= \end -> return $ diffUTCTime end (startTime state)
startTranscript :: Maybe FilePath -> SMTConfig -> IO ()
startTranscript Nothing _ = return ()
startTranscript (Just f) cfg = do ts <- show <$> getZonedTime
mbExecPath <- findExecutable (executable (solver cfg))
writeFile f $ start ts mbExecPath
where SMTSolver{name, options} = solver cfg
start ts mbPath = unlines [ ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
, ";;; SBV: Starting at " ++ ts
, ";;;"
, ";;; Solver : " ++ show name
, ";;; Executable: " ++ fromMaybe "Unable to locate the executable" mbPath
, ";;; Options : " ++ unwords (options cfg)
, ";;;"
, ";;; This file is an auto-generated loadable SMT-Lib file."
, ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
, ""
]
finalizeTranscript :: Maybe FilePath -> Maybe ExitCode -> IO ()
finalizeTranscript Nothing _ = return ()
finalizeTranscript (Just f) mbEC = do ts <- show <$> getZonedTime
appendFile f $ end ts
where end ts = unlines $ [ ""
, ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
, ";;;"
, ";;; SBV: Finished at " ++ ts
]
++ [ ";;;\n;;; Exit code: " ++ show ec | Just ec <- [mbEC] ]
++ [ ";;;"
, ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
]
recordTranscript :: Maybe FilePath -> Either (String, Maybe Int) String -> IO ()
recordTranscript Nothing _ = return ()
recordTranscript (Just f) m = do tsPre <- formatTime defaultTimeLocale "; [%T%Q" <$> getZonedTime
let ts = take 15 $ tsPre ++ repeat '0'
case m of
Left (sent, mbTimeOut) -> appendFile f $ unlines $ (ts ++ "] " ++ to mbTimeOut ++ "Sending:") : lines sent
Right recv -> appendFile f $ unlines $ case lines (dropWhile isSpace recv) of
[] -> [ts ++ "] Received: <NO RESPONSE>"]
[x] -> [ts ++ "] Received: " ++ x]
xs -> (ts ++ "] Received: ") : map ("; " ++) xs
where to Nothing = ""
to (Just i) = "[Timeout: " ++ showTimeoutValue i ++ "] "
{-# INLINE recordTranscript #-}
recordException :: Maybe FilePath -> String -> IO ()
recordException Nothing _ = return ()
recordException (Just f) m = do ts <- show <$> getZonedTime
appendFile f $ exc ts
where exc ts = unlines $ [ ""
, ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
, ";;;"
, ";;; SBV: Caught an exception at " ++ ts
, ";;;"
]
++ [ ";;; " ++ l | l <- dropWhile null (lines m) ]
++ [ ";;;"
, ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
]