Merge pull request #14 from tweag/fd/remove_logging

Remove logging from sendSolver

Z3/smtlib-backends-z3.cabal

@@ -28,7 +28,7 @@ library
   ghc-options:      -Wall -Wunused-packages
   exposed-modules:  SMTLIB.Backends.Z3
   build-depends:
-      base             >=4.15 && <4.17.0
+      base             >=4.14 && <4.17.0
     , bytestring       >=0.10
     , containers       >=0.6
     , inline-c
@@ -52,7 +52,7 @@ test-suite test
   main-is:          Main.hs
   ghc-options:      -threaded -Wall -Wunused-packages
   build-depends:
-      base                   >=4.15
+      base                   >=4.14
     , bytestring             >=0.10
     , smtlib-backends
     , smtlib-backends-tests

Z3/tests/Main.hs

@@ -11,12 +11,11 @@ main :: IO ()
 main = do
   defaultMain $
     testGroup "Tests" $
-      [ testBackend "Examples" validSources noLogging z3,
-        testBackend "Error handling" failingSources noLogging z3
+      [ testBackend "Examples" validSources z3,
+        testBackend "Error handling" failingSources z3
       ]
   where
     z3 todo = Z3.with $ todo . Z3.toBackend
-    noLogging = \_ _ -> return ()
     validSources = filter (\source -> name source `notElem` ["assertions", "unsat cores"]) sources
     failingSources =
       [ Source "invalid command" $ \solver -> do

smtlib-backends.cabal

@@ -33,7 +33,7 @@ library
   other-extensions: Safe
   build-depends:
       async
-    , base           >=4.15 && <4.17.0
+    , base           >=4.14 && <4.17.0
     , bytestring     >=0.10
     , data-default
     , typed-process
@@ -50,8 +50,7 @@ test-suite test
 
   ghc-options:      -threaded -Wall -Wunused-packages
   build-depends:
-      base             >=4.15 && <4.17.0
-    , bytestring       >=0.10
+      base             >=4.14 && <4.17.0
     , data-default
     , smtlib-backends
     , tasty

src/SMTLIB/Backends.hs

@@ -1,8 +1,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module SMTLIB.Backends (Backend (..), LogType (..), Solver, initSolver, initSolverNoLogging, command, ackCommand) where
+module SMTLIB.Backends (Backend (..), Solver, initSolver, command, ackCommand) where
 
-import Data.ByteString.Builder (Builder, toLazyByteString)
+import Data.ByteString.Builder (Builder)
 import qualified Data.ByteString.Lazy.Char8 as LBS
 import Data.Char (isSpace)
 import Data.IORef (IORef, atomicModifyIORef, newIORef)
@@ -31,13 +31,6 @@ flushQueue :: Queue -> IO Builder
 flushQueue q = atomicModifyIORef q $ \cmds ->
   (mempty, cmds)
 
--- | The type of messages logged by the solver.
-data LogType
-  = -- | The message is a command that was sent to the backend.
-    Send
-  | -- | The message is a response outputted by the backend.
-    Recv
-
 -- | A solver is essentially a wrapper around a solver backend. It also comes with
 -- a function for logging the solver's activity, and an optional queue of commands
 -- to send to the backend.
@@ -63,19 +56,9 @@ data Solver = Solver
   { -- | The backend processing the commands.
     backend :: Backend,
     -- | An optional queue to write commands that are to be sent to the solver lazily.
-    queue :: Maybe Queue,
-    -- | The function used for logging the solver's activity.
-    log :: LogType -> LBS.ByteString -> IO ()
+    queue :: Maybe Queue
   }
 
--- | Send a command in bytestring builder format to the solver.
-sendSolver :: Solver -> Builder -> IO LBS.ByteString
-sendSolver solver cmd = do
-  log solver Send $ toLazyByteString cmd
-  resp <- send (backend solver) cmd
-  log solver Recv resp
-  return resp
-
 -- | Create a new solver and initialize it with some options so that it behaves
 -- correctly for our use.
 -- In particular, the "print-success" option is disabled in lazy mode. This should
@@ -84,19 +67,15 @@ initSolver ::
   Backend ->
   -- | whether to enable lazy mode (see 'Solver' for the meaning of this flag)
   Bool ->
-  -- | function for logging the solver's activity;
-  -- if you want line breaks between each log message, you need to implement
-  -- it yourself, e.g use @`LBS.putStr` . (<> "\n")@
-  (LogType -> LBS.ByteString -> IO ()) ->
   IO Solver
-initSolver solverBackend lazy logger = do
+initSolver solverBackend lazy = do
   solverQueue <-
     if lazy
       then do
         ref <- newIORef mempty
         return $ Just ref
       else return Nothing
-  let solver = Solver solverBackend solverQueue logger
+  let solver = Solver solverBackend solverQueue
   if lazy
     then return ()
     else -- this should not be enabled when the queue is used, as it messes with parsing
@@ -109,17 +88,12 @@ initSolver solverBackend lazy logger = do
   setOption solver "produce-models" "true"
   return solver
 
--- | Initialize a solver whose logging function doesn't do anything.
--- See `initSolver`.
-initSolverNoLogging :: Backend -> Bool -> IO Solver
-initSolverNoLogging solverBackend lazyMode = initSolver solverBackend lazyMode $ \_ _ -> return ()
-
 -- | Have the solver evaluate a SMT-LIB command.
 -- This forces the queued commands to be evaluated as well, but their results are
 -- *not* checked for correctness.
 command :: Solver -> Builder -> IO LBS.ByteString
 command solver cmd = do
-  sendSolver solver
+  send (backend solver)
     =<< case queue solver of
       Nothing -> return $ cmd
       Just q -> (<> cmd) <$> flushQueue q
@@ -133,7 +107,7 @@ ackCommand :: Solver -> Builder -> IO ()
 ackCommand solver cmd =
   case queue solver of
     Nothing -> do
-      res <- sendSolver solver cmd
+      res <- send (backend solver) cmd
       if trim res == "success"
         then return ()
         else

tests/smtlib-backends-tests.cabal

@@ -29,8 +29,7 @@ library
   exposed-modules:  SMTLIB.Backends.Tests
   other-modules:    SMTLIB.Backends.Tests.Sources
   build-depends:
-      base             >=4.15 && <4.17.0
-    , bytestring       >=0.10
+      base             >=4.14 && <4.17.0
     , smtlib-backends
     , tasty
     , tasty-hunit

tests/src/Main.hs

@@ -8,8 +8,6 @@ main = do
   defaultMain $
     testGroup
       "backends"
-      [ testBackend "process" sources noLogging $ \todo ->
+      [ testBackend "process" sources $ \todo ->
           Process.with def $ todo . Process.toBackend
       ]
-  where
-    noLogging = \_ _ -> return ()

tests/src/SMTLIB/Backends/Tests.hs

@@ -6,8 +6,7 @@ module SMTLIB.Backends.Tests
   )
 where
 
-import Data.ByteString.Lazy.Char8 as LBS
-import SMTLIB.Backends (Backend, LogType, initSolver)
+import SMTLIB.Backends (Backend, initSolver)
 import qualified SMTLIB.Backends.Tests.Sources as Src
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -18,13 +17,11 @@ testBackend ::
   String ->
   -- | A list of examples on which to run the backend.
   [Src.Source] ->
-  -- | A function for logging the solver's activity.
-  (LogType -> LBS.ByteString -> IO ()) ->
   -- | A function that should create a backend, run a given
   -- computation and release the backend's resources.
   ((Backend -> Assertion) -> Assertion) ->
   TestTree
-testBackend name sources logger with =
+testBackend name sources with =
   testGroup name $ do
     lazyMode <- [False, True]
     return $
@@ -38,5 +35,5 @@ testBackend name sources logger with =
           return $
             testCase (Src.name source) $
               with $ \backend -> do
-                solver <- initSolver backend lazyMode logger
+                solver <- initSolver backend lazyMode
                 Src.run source solver