simple-smt 0.9.7 → 0.9.8

raw patch · 2 files changed

+153/−39 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• SimpleSMT.hs +152/−38
• simple-smt.cabal +1/−1

@@ -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 { .. }--------

@@ -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