diff --git a/SimpleSMT.hs b/SimpleSMT.hs --- a/SimpleSMT.hs +++ b/SimpleSMT.hs @@ -8,6 +8,13 @@ Solver(..) , newSolver , newSolverNotify + , newSolverWithConfig + , Config(..) + , SolverLogger(..) + , defaultConfig + , noSolverLogger + , heraldSolverLogger + , smtSolverLogger , ackCommand , simpleCommand , simpleCommandMaybe @@ -21,6 +28,7 @@ -- ** Logging and Debugging , Logger(..) , newLogger + , newLoggerWithHandle , withLogLevel , logMessageAt , logIndented @@ -39,7 +47,7 @@ , define , defineFun , defineFunRec - , defineFunsRec + , defineFunsRec , assert , check , Result(..) @@ -59,8 +67,8 @@ , quoteSymbol , symbol , keyword - , as - + , as + -- ** Types , tInt , tBool @@ -147,8 +155,9 @@ import Data.Bits(testBit) import Data.IORef(newIORef, atomicModifyIORef, modifyIORef', readIORef, writeIORef) -import System.Process(runInteractiveProcess, waitForProcess) -import System.IO (hFlush, hGetLine, hGetContents, hPutStrLn, stdout, hClose) +import System.Process(runInteractiveProcess, waitForProcess, terminateProcess) +import System.IO (Handle, hFlush, hGetLine, hGetContents, hPutStr, hPutStrLn, + stdout, hClose) import System.Exit(ExitCode) import qualified Control.Exception as X import Control.Concurrent(forkIO) @@ -178,16 +187,35 @@ deriving (Eq, Ord, Show) -- | Show an s-expression. +-- +-- >>> let Just (e, _) = readSExpr "(assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))" +-- >>> putStrLn $ showsSExpr e "" +-- (assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv)) showsSExpr :: SExpr -> ShowS showsSExpr ex = case ex of Atom x -> showString x - List es -> showChar '(' . - foldr (\e m -> showsSExpr e . showChar ' ' . m) - (showChar ')') es + List [] -> showString "()" + List (e0 : es) -> showChar '(' . showsSExpr e0 . + foldr (\e m -> showChar ' ' . showsSExpr e . m) + (showChar ')') es --- | Show an S-expression in a somewhat readbale fashion. +-- | Show an s-expression in a somewhat readable fashion. +-- +-- >>> let Just (e, _) = readSExpr "(assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))" +-- >>> putStrLn $ ppSExpr e "" +-- (assert +-- (= +-- ( +-- (_ +-- map +-- (- +-- (Int Int) +-- Int)) +-- a1Cl +-- a1Cm) +-- a1Cv)) ppSExpr :: SExpr -> ShowS ppSExpr = go 0 where @@ -219,11 +247,14 @@ List es -> showString "(" . many (map (new (n+2)) es) . showString ")" -- | Parse an s-expression. +-- +-- >>> readSExpr "(_ map (- (Int Int) Int)) a1Cl a1Cm)" +-- Just (List [Atom "_",Atom "map",List [Atom "-",List [Atom "Int",Atom "Int"],Atom "Int"]]," a1Cl a1Cm)") readSExpr :: String -> Maybe (SExpr, String) readSExpr (c : more) | isSpace c = readSExpr more readSExpr (';' : more) = readSExpr $ drop 1 $ dropWhile (/= '\n') more readSExpr ('|' : more) = do (sym, '|' : rest) <- pure (span ((/=) '|') more) - Just (Atom ('|' : sym ++ ['|']), rest) + Just (Atom ('|' : sym ++ ['|']), rest) readSExpr ('(' : more) = do (xs,more1) <- list more return (List xs, more1) where @@ -246,7 +277,10 @@ -- ^ Send a command to the solver. , stop :: IO ExitCode - -- ^ Terminate the solver. + -- ^ Wait for the solver to finish and exit gracefully. + + , forceStop :: IO ExitCode + -- ^ Terminate the solver without waiting for it to finish. } @@ -255,7 +289,10 @@ [String] {- ^ Arguments -} -> Maybe Logger {- ^ Optional logging here -} -> IO Solver -newSolver n xs l = newSolverNotify n xs l Nothing +newSolver exe opts mbLog = newSolverWithConfig $ + (defaultConfig exe opts) + { solverLogger = maybe noSolverLogger heraldSolverLogger mbLog + } newSolverNotify :: String {- ^ Executable -} -> @@ -263,15 +300,24 @@ Maybe Logger {- ^ Optional logging here -} -> Maybe (ExitCode -> IO ()) {- ^ Do this when the solver exits -} -> IO Solver -newSolverNotify exe opts mbLog mbOnExit = - do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing +newSolverNotify exe opts mbLog mbOnExit = newSolverWithConfig $ + (defaultConfig exe opts) + { solverOnExit = mbOnExit + , solverLogger = maybe noSolverLogger heraldSolverLogger mbLog + } - let info a = case mbLog of - Nothing -> return () - Just l -> logMessage l a +-- | Start a new solver process using the provided 'Config' options. +newSolverWithConfig :: Config -> IO Solver +newSolverWithConfig + (Config { solverExecutable = exe + , solverArguments = opts + , solverOnExit = mbOnExit + , solverLogger = log + }) = + do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing _ <- forkIO $ forever (do errs <- hGetLine hErr - info ("[stderr] " ++ errs)) + solverLogStdErr log errs) `X.catch` \X.SomeException {} -> return () case mbOnExit of @@ -287,7 +333,7 @@ y : ys -> (ys, Just y) let cmd c = do let txt = showsSExpr c "" - info ("[send->] " ++ txt) + solverLogSend log c hPutStrLn hIn txt hFlush hIn @@ -295,20 +341,25 @@ do cmd c mb <- getResponse case mb of - Just res -> do info ("[<-recv] " ++ showsSExpr res "") + Just res -> do solverLogRecv log res return res Nothing -> fail "Missing response from solver" - stop = - do cmd (List [Atom "exit"]) - `X.catch` (\X.SomeException{} -> pure ()) - ec <- waitForProcess h + waitAndCleanup = + do ec <- waitForProcess h X.catch (do hClose hIn hClose hOut hClose hErr) - (\ex -> info (show (ex::X.IOException))) + (solverLogExcn log) return ec + forceStop = terminateProcess h *> waitAndCleanup + + stop = + do cmd (List [Atom "exit"]) + `X.catch` (\X.SomeException{} -> pure ()) + waitAndCleanup + solver = Solver { .. } setOption solver ":print-success" "true" @@ -316,7 +367,73 @@ return solver +-- | Options for configuring how to start, stop, and interact with an SMT +-- solver process. +data Config = Config + { solverExecutable :: String + -- ^ The SMT solver executable. + , solverArguments :: [String] + -- ^ The command-line arguments to pass to the SMT solver. + , solverOnExit :: Maybe (ExitCode -> IO ()) + -- ^ Do this when the SMT solver exits. + , solverLogger :: SolverLogger + -- ^ How to log solver-related messages. + } +-- | Options for logging SMT solver–related messages. +data SolverLogger = SolverLogger + { solverLogSend :: SExpr -> IO () + -- ^ Log an SMT query ('SExpr') being sent to the SMT solver. + , solverLogRecv :: SExpr -> IO () + -- ^ Log a response ('SExpr') being received from the SMT solver. + , solverLogExcn :: X.IOException -> IO () + -- ^ Log the SMT solver throwing an 'X.IOException'. + , solverLogStdErr :: String -> IO () + -- ^ Log the SMT solver displaying an error to @stderr@. + } + +-- | A reasonable default 'Config' value. +defaultConfig :: + String {- ^ Solver executable -} -> + [String] {- ^ Solver arguments -} -> + Config +defaultConfig exe opts = Config + { solverExecutable = exe + , solverArguments = opts + , solverOnExit = Nothing + , solverLogger = noSolverLogger + } + +-- | A trivial 'SolverLogger' that does not perform any logging. +noSolverLogger :: SolverLogger +noSolverLogger = SolverLogger + { solverLogSend = \_ -> pure () + , solverLogRecv = \_ -> pure () + , solverLogExcn = \_ -> pure () + , solverLogStdErr = \_ -> pure () + } + +-- | A basic 'SolverLogger' that prints out heralds in front of sent and +-- received SMT queries, as well as messages to @stderr@. This is the approach +-- that 'newSolver' and 'newSolverNotify' use for logging. +heraldSolverLogger :: Logger -> SolverLogger +heraldSolverLogger l = SolverLogger + { solverLogSend = \c -> logMessage l ("[send->] " ++ showsSExpr c "") + , solverLogRecv = \c -> logMessage l ("[<-recv] " ++ showsSExpr c "") + , solverLogExcn = \exc -> logMessage l (show exc) + , solverLogStdErr = \errs -> logMessage l ("[stderr] " ++ errs) + } + +-- | A 'SolverLogger' that formats log messages into the SMT-LIB file format so +-- that the resulting log can be parsed as input by an SMT solver. +smtSolverLogger :: Logger -> SolverLogger +smtSolverLogger l = SolverLogger + { solverLogSend = \c -> logMessage l (showsSExpr c "") + , solverLogRecv = \c -> logMessage l ("; " ++ showsSExpr c "") + , solverLogExcn = \exc -> logMessage l (show exc) + , solverLogStdErr = \errs -> logMessage l errs + } + -- | Load the contents of a file. loadFile :: Solver -> FilePath -> IO () loadFile s file = loadString s =<< readFile file @@ -504,7 +621,7 @@ decls = List (map oneArg ds) bodies = List (map (\(_, _, _, body) -> body) ds) - + -- | Assume a fact. assert :: Solver -> SExpr -> IO () assert proc e = ackCommand proc $ fun "assert" [e] @@ -643,7 +760,7 @@ isSimpleSymbol _ = False quoteSymbol :: String -> String -quoteSymbol s +quoteSymbol s | isSimpleSymbol s = s | otherwise = '|' : s ++ "|" @@ -1008,7 +1125,12 @@ -- | A simple stdout logger. Shows only messages logged at a level that is -- greater than or equal to the passed level. newLogger :: Int -> IO Logger -newLogger l = +newLogger = newLoggerWithHandle stdout + +-- | A simple logger that writes to a 'Handle'. Shows only messages logged at a +-- level that is greater than or equal to the passed level. +newLoggerWithHandle :: Handle -> Int -> IO Logger +newLoggerWithHandle h l = do tab <- newIORef 0 lev <- newIORef 0 let logLevel = readIORef lev @@ -1021,17 +1143,9 @@ logMessage x = shouldLog $ do let ls = lines x t <- readIORef tab - putStr $ unlines [ replicate t ' ' ++ l | l <- ls ] - hFlush stdout + hPutStr h $ unlines [ replicate t ' ' ++ l | l <- ls ] + hFlush h logTab = shouldLog (modifyIORef' tab (+ 2)) logUntab = shouldLog (modifyIORef' tab (subtract 2)) return Logger { .. } - - - - - - - - diff --git a/simple-smt.cabal b/simple-smt.cabal --- a/simple-smt.cabal +++ b/simple-smt.cabal @@ -1,5 +1,5 @@ name: simple-smt -version: 0.9.7 +version: 0.9.8 synopsis: A simple way to interact with an SMT solver process. description: A simple way to interact with an SMT solver process. license: BSD3