simple-smt 0.9.9 → 1.0

raw patch · 2 files changed

+56/−43 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• SimpleSMT.hs +55/−42
• simple-smt.cabal +1/−1

@@ -166,6 +166,7 @@ import Text.Read(readMaybe) import Data.Ratio((%), numerator, denominator) import Numeric(showHex, readHex, showFFloat)+import System.Mem.Weak(addFinalizer)   -- | Results of checking for satisfiability.@@ -319,63 +320,75 @@           }) =   do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing +     -- Drain stderr      _ <- forkIO $ forever (do errs <- hGetLine hErr                                solverLogStdErr log errs)                     `X.catch` \X.SomeException {} -> return () -     getResponse <--       do txt <- hGetContents hOut                  -- Read *all* output-          ref <- newIORef (unfoldr readSExpr txt)  -- Parse, and store result-          return $ atomicModifyIORef ref $ \xs ->-                      case xs of-                        []     -> (xs, Nothing)-                        y : ys -> (ys, Just y)+     -- Parse responses (lazy)+     txt <- hGetContents hOut                       -- Read *all* output+     responses <- newIORef (unfoldr readSExpr txt) -- Parse, and store result -     let cmd c = do let txt = showsSExpr c ""-                    solverLogSend log c-                    hPutStrLn hIn txt-                    hFlush hIn+     -- Wait for the solver to exit+     exitResult <- newEmptyMVar+     _ <- forkFinally+            (observeExit h hIn hOut hErr)+            (putMVar exitResult) -         command c =-           do cmd c-              mb <- getResponse-              case mb of-                Just res -> do solverLogRecv log res-                               return res-                Nothing  -> fail "Missing response from solver"+     -- Close `stdin` when the Haskell Solver object is GC-ed, so that+     -- we close `stdin` and the solver process exits.+     addFinalizer responses (closeHandle hIn) -         cleanup =-           X.catch (do hClose hIn-                       hClose hOut-                       hClose hErr)-                   (solverLogExcn log)+     let solver =+           Solver+             { command = runCommand hIn responses+             , stop = stopSolver hIn exitResult+             , forceStop = forceStopSolver h exitResult+             } -         observeExit =-           do ec <- waitForProcess h-              (case mbOnExit of-                 Nothing -> pure ()-                 Just this -> this ec)-                `X.finally` cleanup-              return ec+     setOption solver ":print-success" "true"+     setOption solver ":produce-models" "true" -     exitResult <- newEmptyMVar-     _ <- forkFinally observeExit (putMVar exitResult)+     return solver+  where+  send hIn c =+    do let txt = showsSExpr c ""+       solverLogSend log c+       hPutStrLn hIn txt+       hFlush hIn -     let waitForExit = either X.throwIO pure =<< readMVar exitResult+  runCommand hIn responses c =+    do send hIn c+       mb <- atomicModifyIORef responses $ \xs ->+               case xs of+                 []     -> (xs, Nothing)+                 y : ys -> (ys, Just y)+       case mb of+         Just res -> do solverLogRecv log res+                        return res+         Nothing  -> fail "Missing response from solver" -         forceStop = terminateProcess h *> waitForExit+  closeHandle handle =+    X.catch (hClose handle) (solverLogExcn log) -         stop =-           do cmd (List [Atom "exit"])-                `X.catch` (\X.SomeException{} -> pure ())-              waitForExit+  observeExit h hIn hOut hErr =+    do ec <- waitForProcess h+       (case mbOnExit of+          Nothing -> pure ()+          Just this -> this ec)+         `X.finally` mapM_ closeHandle [hIn, hOut, hErr]+       return ec -         solver = Solver { .. }+  waitForExit exitResult =+    either X.throwIO pure =<< readMVar exitResult -     setOption solver ":print-success" "true"-     setOption solver ":produce-models" "true"+  forceStopSolver h exitResult =+    terminateProcess h *> waitForExit exitResult -     return solver+  stopSolver hIn exitResult =+    do send hIn (List [Atom "exit"])+         `X.catch` (\X.SomeException{} -> pure ())+       waitForExit exitResult  -- | Options for configuring how to start, stop, and interact with an SMT -- solver process.

@@ -1,5 +1,5 @@ name:                simple-smt-version:             0.9.9+version:             1.0 synopsis:            A simple way to interact with an SMT solver process. description:         A simple way to interact with an SMT solver process. license:             BSD3