Process backend: add a function for sending (exit)

smtlib-backends-process/src/SMTLIB/Backends/Process.hs

@@ -9,6 +9,7 @@ module SMTLIB.Backends.Process
   ( Config (..),
     Handle (..),
     new,
+    exit,
     wait,
     close,
     with,
@@ -107,6 +108,18 @@ new config = do
           )
     reportError' = (reportError config) . LBS.fromStrict
 
+-- | Send a command to the process without reading its response.
+write :: Handle -> Builder -> IO ()
+write handle cmd = do
+  hPutBuilder (getStdin $ process handle) $ cmd <> "\n"
+  IO.hFlush $ getStdin $ process handle
+
+-- | Send the @(exit)@ command to the process.
+-- Note that using @'write' ('toBackend' handle) "(exit)"@ instead could hang
+-- the process as it would wait for a response.
+exit :: Handle -> IO ()
+exit = flip write "(exit)"
+
 -- | Wait for the process to exit and cleanup its resources.
 wait :: Handle -> IO ExitCode
 wait handle = do
@@ -141,8 +154,7 @@ pattern c :< rest <- (BS.uncons -> Just (c, rest))
 toBackend :: Handle -> Backend
 toBackend handle =
   Backend $ \cmd -> do
-    hPutBuilder (getStdin $ process handle) $ cmd <> "\n"
-    IO.hFlush $ getStdin $ process handle
+    write handle cmd
     toLazyByteString <$> continueNextLine (scanParen 0) mempty
   where
     -- scanParen read lines from the handle's output channel until it has detected

smtlib-backends-process/tests/Examples.hs

@@ -4,7 +4,7 @@ module Examples (examples) where
 
 import qualified Data.ByteString.Lazy.Char8 as LBS
 import Data.Default (def)
-import SMTLIB.Backends (QueuingFlag (..), command, command_, initSolver)
+import SMTLIB.Backends (QueuingFlag (..), command, initSolver)
 import qualified SMTLIB.Backends.Process as Process
 import System.Exit (ExitCode (ExitSuccess))
 import System.IO (BufferMode (LineBuffering), hSetBuffering)
@@ -74,12 +74,11 @@ manualExit :: IO ()
 manualExit = do
   -- launch a new process with 'Process.new'
   handle <- Process.new def
-  let backend = Process.toBackend handle
-  -- here we disable queuing so that we can use 'command_' to ensure the exit
-  -- command will be received successfully
-  solver <- initSolver NoQueuing backend
-  command_ solver "(exit)"
-  -- 'Process.wait' takes care of cleaning resources and waits for the process to
-  -- exit
+  -- to stop the process, we first send an "(exit)" command and then use
+  -- 'Process.wait' which takes care of cleaning resources and waits for the
+  -- process to actually exit
+  -- when an exit code isn't needed and the process doesn't have to stop
+  -- gracefully, another simpler option is to just use 'Process.close'
+  Process.exit handle
   exitCode <- Process.wait handle
   assertBool "the solver process didn't exit properly" $ exitCode == ExitSuccess