module Data.SBV.SMT.SMT where
import qualified Control.Exception as C
import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)
import Control.DeepSeq (NFData(..))
import Control.Monad (when, zipWithM)
import Data.Char (isSpace)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Function (on)
import Data.List (intercalate, isPrefixOf, isInfixOf, sortBy)
import Data.Word (Word8, Word16, Word32, Word64)
import System.Directory (findExecutable)
import System.Environment (getEnv)
import System.Exit (ExitCode(..))
import System.IO (hClose, hFlush, hPutStr, hGetContents, hGetLine)
import System.Process (runInteractiveProcess, waitForProcess, terminateProcess)
import qualified Data.Map as M
import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.PrettyNum
import Data.SBV.BitVectors.Symbolic (SMTEngine)
import Data.SBV.SMT.SMTLib (interpretSolverOutput, interpretSolverModelLine)
import Data.SBV.Utils.Lib (joinArgs, splitArgs)
import Data.SBV.Utils.TDiff
resultConfig :: SMTResult -> SMTConfig
resultConfig (Unsatisfiable c) = c
resultConfig (Satisfiable c _) = c
resultConfig (Unknown c _) = c
resultConfig (ProofError c _) = c
resultConfig (TimeOut c) = c
newtype ThmResult = ThmResult SMTResult
newtype SatResult = SatResult SMTResult
newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
newtype AllSatResult = AllSatResult (Bool, [SMTResult])
instance Show ThmResult where
show (ThmResult r) = showSMTResult "Q.E.D."
"Unknown" "Unknown. Potential counter-example:\n"
"Falsifiable" "Falsifiable. Counter-example:\n" r
instance Show SatResult where
show (SatResult r) = showSMTResult "Unsatisfiable"
"Unknown" "Unknown. Potential model:\n"
"Satisfiable" "Satisfiable. Model:\n" r
instance Show SafeResult where
show (SafeResult (mbLoc, msg, r)) = showSMTResult (tag "No violations detected")
(tag "Unknown") (tag "Unknown. Potential violating model:\n")
(tag "Violated") (tag "Violated. Model:\n") r
where loc = maybe "" (++ ": ") mbLoc
tag s = loc ++ msg ++ ": " ++ s
instance Show AllSatResult where
show (AllSatResult (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 c of
0 -> "No solutions found."
1 -> "This is the only solution." ++ uniqueWarn
_ -> "Found " ++ show c ++ " different solutions." ++ uniqueWarn
sh i c = (ok, showSMTResult "Unsatisfiable"
"Unknown" "Unknown. Potential model:\n"
("Solution #" ++ show i ++ ":\nSatisfiable") ("Solution #" ++ show i ++ ":\n") c)
where ok = case c of
Satisfiable{} -> True
_ -> False
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
getModel :: 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 getModel a of
Right (_, b) -> Just b
_ -> Nothing
extractModels :: SatModel a => AllSatResult -> [a]
extractModels (AllSatResult (_, xs)) = [ms | Right (_, ms) <- map getModel 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
getModel (ThmResult r) = getModel r
modelExists (ThmResult r) = modelExists r
getModelDictionary (ThmResult r) = getModelDictionary r
instance Modelable SatResult where
getModel (SatResult r) = getModel r
modelExists (SatResult r) = modelExists r
getModelDictionary (SatResult r) = getModelDictionary r
instance Modelable SMTResult where
getModel (Unsatisfiable _) = Left "SBV.getModel: Unsatisfiable result"
getModel (Unknown _ m) = Right (True, parseModelOut m)
getModel (ProofError _ s) = error $ unlines $ "Backend solver complains: " : s
getModel (TimeOut _) = Left "Timeout"
getModel (Satisfiable _ m) = Right (False, parseModelOut m)
modelExists Satisfiable{} = True
modelExists Unknown{} = False
modelExists _ = False
getModelDictionary (Unsatisfiable _) = M.empty
getModelDictionary (Unknown _ m) = M.fromList (modelAssocs m)
getModelDictionary (ProofError _ _) = M.empty
getModelDictionary (TimeOut _) = M.empty
getModelDictionary (Satisfiable _ m) = M.fromList (modelAssocs m)
parseModelOut :: SatModel a => SMTModel -> a
parseModelOut m = case parseCWs [c | (_, c) <- modelAssocs m] of
Just (x, []) -> x
Just (_, ys) -> error $ "SBV.getModel: Partially constructed model; remaining elements: " ++ show ys
Nothing -> error $ "SBV.getModel: 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 (getModel . 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 unkMsgModel satMsg satMsgModel result = case result of
Unsatisfiable _ -> unsatMsg
Satisfiable _ (SMTModel []) -> satMsg
Satisfiable _ m -> satMsgModel ++ showModel cfg m
Unknown _ (SMTModel []) -> unkMsg
Unknown _ m -> unkMsgModel ++ showModel cfg m
ProofError _ [] -> "*** An error occurred. No additional information available. Try running in verbose mode"
ProofError _ ls -> "*** An error occurred.\n" ++ intercalate "\n" (map ("*** " ++) ls)
TimeOut _ -> "*** Timeout"
where cfg = resultConfig result
showModel :: SMTConfig -> SMTModel -> String
showModel cfg model
| 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 allVars = modelAssocs model
relevantVars = filter (not . ignore) allVars
ignore (s, _) = "__internal_sbv_" `isPrefixOf` s || isNonModelVar cfg s
shM (s, v) = let vs = shCW cfg v 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 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."
shUI :: (String, [String]) -> [String]
shUI (flong, cases) = (" -- uninterpreted: " ++ f) : map shC cases
where tf = dropWhile (/= '_') flong
f = if null tf then flong else tail tf
shC s = " " ++ s
shUA :: (String, [String]) -> [String]
shUA (f, cases) = (" -- array: " ++ f) : map shC cases
where shC s = " " ++ s
pipeProcess :: SMTConfig -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])
pipeProcess cfg execName opts script cleanErrs = do
let nm = show (name (solver cfg))
mbExecPath <- findExecutable execName
case mbExecPath of
Nothing -> return $ Left $ "Unable to locate executable for " ++ nm
++ "\nExecutable specified: " ++ show execName
Just execPath ->
do solverResult <- dispatchSolver cfg execPath opts script
case solverResult of
Left s -> return $ Left s
Right (ec, contents, allErrors) ->
let errors = dropWhile isSpace (cleanErrs allErrors)
in case (null errors, ec) of
(True, ExitSuccess) -> return $ Right $ map clean (filter (not . null) (lines contents))
(_, ec') -> let errors' = if null errors
then (if null (dropWhile isSpace contents)
then "(No error message printed on stderr by the executable.)"
else contents)
else errors
finalEC = case (ec', ec) of
(ExitFailure n, _) -> n
(_, ExitFailure n) -> n
_ -> 0
in return $ Left $ "Failed to complete the call to " ++ nm
++ "\nExecutable : " ++ show execPath
++ "\nOptions : " ++ joinArgs opts
++ "\nExit code : " ++ show finalEC
++ "\nSolver output: "
++ "\n" ++ line ++ "\n"
++ intercalate "\n" (filter (not . null) (lines errors'))
++ "\n" ++ line
++ "\nGiving up.."
where clean = reverse . dropWhile isSpace . reverse . dropWhile isSpace
line = replicate 78 '='
standardModel :: (Bool -> [(Quantifier, NamedSymVar)] -> [String] -> SMTModel, SW -> String -> [String])
standardModel = (standardModelExtractor, standardValueExtractor)
standardValueExtractor :: SW -> String -> [String]
standardValueExtractor _ l = [l]
standardModelExtractor :: Bool -> [(Quantifier, NamedSymVar)] -> [String] -> SMTModel
standardModelExtractor isSat qinps solverLines = SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps) solverLines }
where sortByNodeId :: [(Int, a)] -> [(Int, a)]
sortByNodeId = sortBy (compare `on` fst)
inps
| isSat = map snd $ if all (== ALL) (map fst qinps)
then qinps
else reverse $ dropWhile ((== ALL) . fst) $ reverse qinps
| True = map snd $ takeWhile ((== ALL) . fst) qinps
standardEngine :: String
-> String
-> ([String] -> Int -> [String])
-> (Bool -> [(Quantifier, NamedSymVar)] -> [String] -> SMTModel, SW -> String -> [String])
-> SMTEngine
standardEngine envName envOptName addTimeOut (extractMap, extractValue) cfg isSat qinps skolemMap pgm = 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)))
let cfg' = cfg {solver = (solver cfg) {executable = execName, options = maybe execOpts (addTimeOut execOpts) (timeOut cfg)}}
tweaks = case solverTweaks cfg' of
[] -> ""
ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]
cont rm = intercalate "\n" $ concatMap extract skolemMap
where extract (Left s) = extractValue s $ "(echo \"((" ++ show s ++ " " ++ mkSkolemZero rm (kindOf s) ++ "))\")"
extract (Right (s, [])) = extractValue s $ "(get-value (" ++ show s ++ "))"
extract (Right (s, ss)) = extractValue s $ "(get-value (" ++ show s ++ concat [' ' : mkSkolemZero rm (kindOf a) | a <- ss] ++ "))"
script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont (roundingMode cfg))}
standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps))
standardSolver :: SMTConfig -> SMTScript -> (String -> String) -> ([String] -> a) -> ([String] -> a) -> IO a
standardSolver config script cleanErrs failure success = do
let msg = when (verbose config) . putStrLn . ("** " ++)
smtSolver= solver config
exec = executable smtSolver
opts = options smtSolver
isTiming = timing config
nmSolver = show (name smtSolver)
msg $ "Calling: " ++ show (unwords (exec:[joinArgs opts]))
case smtFile config of
Nothing -> return ()
Just f -> do msg $ "Saving the generated script in file: " ++ show f
writeFile f (scriptBody script)
contents <- timeIf isTiming nmSolver $ pipeProcess config exec opts script cleanErrs
msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents
case contents of
Left e -> return $ failure (lines e)
Right xs -> return $ success (mergeSExpr xs)
dispatchSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (Either String (ExitCode, String, String))
dispatchSolver cfg execPath opts script = rnf script `seq` (Right `fmap` runSolver cfg execPath opts script) `C.catch` (\(e::C.SomeException) -> bad (show e))
where bad s = return $ Left $ unlines [ "Failed to start the external solver: " ++ s
, "Make sure you can start " ++ show execPath
, "from the command line without issues."
]
runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)
runSolver cfg execPath opts script
= do (send, ask, cleanUp, pid) <- do
(inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing
let send l = hPutStr inh (l ++ "\n") >> hFlush inh
recv = hGetLine outh
ask l = send l >> recv
cleanUp response
= do hClose inh
outMVar <- newEmptyMVar
out <- hGetContents outh
_ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
err <- hGetContents errh
_ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
takeMVar outMVar
takeMVar outMVar
hClose outh
hClose errh
ex <- waitForProcess pid
return $ case response of
Nothing -> (ex, out, err)
Just (r, vals) ->
let finalOut = intercalate "\n" (r : vals)
notAvail = "model is not available" `isInfixOf` (finalOut ++ out ++ err)
in if "unknown" `isPrefixOf` r && notAvail
then (ExitSuccess, "unknown" , "")
else (ex, finalOut ++ "\n" ++ out, err)
return (send, ask, cleanUp, pid)
let executeSolver = do mapM_ send (lines (scriptBody script))
response <- case scriptModel script of
Nothing -> do send $ satCmd cfg
return Nothing
Just ls -> do r <- ask $ satCmd cfg
vals <- if any (`isPrefixOf` r) ["sat", "unknown"]
then do let mls = lines ls
when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"
mapM_ putStrLn mls
mapM ask mls
else return []
return $ Just (r, vals)
cleanUp response
executeSolver `C.onException` terminateProcess pid
mergeSExpr :: [String] -> [String]
mergeSExpr [] = []
mergeSExpr (x:xs)
| d == 0 = x : mergeSExpr xs
| True = let (f, r) = grab d xs in unwords (x:f) : mergeSExpr r
where d = parenDiff x
parenDiff :: String -> Int
parenDiff = go 0
where go i "" = i
go i ('(':cs) = let i'= i+1 in i' `seq` go i' cs
go i (')':cs) = let i'= i1 in i' `seq` go i' cs
go i (_ :cs) = go i cs
grab i ls
| i <= 0 = ([], ls)
grab _ [] = ([], [])
grab i (l:ls) = let (a, b) = grab (i+parenDiff l) ls in (l:a, b)