From 8b61b53aba2db0759c7253e7a2792fe5d9c37aa9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Tue, 13 Dec 2022 12:53:26 -0300 Subject: [PATCH 1/3] Remove logging from sendSolver The logger makes the interface larger and offers no reuse of code. If the user wants logging, she can surround the calls to sendSolver herself with logging calls. --- Z3/tests/Main.hs | 5 ++--- smtlib-backends.cabal | 1 - src/SMTLIB/Backends.hs | 34 ++++++------------------------ tests/smtlib-backends-tests.cabal | 1 - tests/src/Main.hs | 4 +--- tests/src/SMTLIB/Backends/Tests.hs | 9 +++----- 6 files changed, 12 insertions(+), 42 deletions(-) diff --git a/Z3/tests/Main.hs b/Z3/tests/Main.hs index a363a20..afb52de 100644 --- a/Z3/tests/Main.hs +++ b/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 diff --git a/smtlib-backends.cabal b/smtlib-backends.cabal index 5e9553d..2f7bb57 100644 --- a/smtlib-backends.cabal +++ b/smtlib-backends.cabal @@ -51,7 +51,6 @@ test-suite test ghc-options: -threaded -Wall -Wunused-packages build-depends: base >=4.15 && <4.17.0 - , bytestring >=0.10 , data-default , smtlib-backends , tasty diff --git a/src/SMTLIB/Backends.hs b/src/SMTLIB/Backends.hs index 1aa14f8..0b28777 100644 --- a/src/SMTLIB/Backends.hs +++ b/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,18 +56,12 @@ 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 +sendSolver solver cmd = send (backend solver) cmd -- | Create a new solver and initialize it with some options so that it behaves -- correctly for our use. @@ -84,19 +71,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,11 +92,6 @@ 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. diff --git a/tests/smtlib-backends-tests.cabal b/tests/smtlib-backends-tests.cabal index 7a8bcb9..4de8584 100644 --- a/tests/smtlib-backends-tests.cabal +++ b/tests/smtlib-backends-tests.cabal @@ -30,7 +30,6 @@ library other-modules: SMTLIB.Backends.Tests.Sources build-depends: base >=4.15 && <4.17.0 - , bytestring >=0.10 , smtlib-backends , tasty , tasty-hunit diff --git a/tests/src/Main.hs b/tests/src/Main.hs index 509f3c6..aaa6915 100644 --- a/tests/src/Main.hs +++ b/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 () diff --git a/tests/src/SMTLIB/Backends/Tests.hs b/tests/src/SMTLIB/Backends/Tests.hs index aaf7553..a21bc38 100644 --- a/tests/src/SMTLIB/Backends/Tests.hs +++ b/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 From f59ae0549778de513ddaf54c7ed4272780b880fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Tue, 13 Dec 2022 13:27:46 -0300 Subject: [PATCH 2/3] Relax lower bound of base --- Z3/smtlib-backends-z3.cabal | 4 ++-- smtlib-backends.cabal | 4 ++-- tests/smtlib-backends-tests.cabal | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Z3/smtlib-backends-z3.cabal b/Z3/smtlib-backends-z3.cabal index 17898d5..86444ac 100644 --- a/Z3/smtlib-backends-z3.cabal +++ b/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 diff --git a/smtlib-backends.cabal b/smtlib-backends.cabal index 2f7bb57..a4a8483 100644 --- a/smtlib-backends.cabal +++ b/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,7 +50,7 @@ test-suite test ghc-options: -threaded -Wall -Wunused-packages build-depends: - base >=4.15 && <4.17.0 + base >=4.14 && <4.17.0 , data-default , smtlib-backends , tasty diff --git a/tests/smtlib-backends-tests.cabal b/tests/smtlib-backends-tests.cabal index 4de8584..faff737 100644 --- a/tests/smtlib-backends-tests.cabal +++ b/tests/smtlib-backends-tests.cabal @@ -29,7 +29,7 @@ library exposed-modules: SMTLIB.Backends.Tests other-modules: SMTLIB.Backends.Tests.Sources build-depends: - base >=4.15 && <4.17.0 + base >=4.14 && <4.17.0 , smtlib-backends , tasty , tasty-hunit From 1e2711afbef28d5e69a9fb93f00da56b44f4db6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Tue, 13 Dec 2022 13:37:15 -0300 Subject: [PATCH 3/3] Remove sendSolver --- src/SMTLIB/Backends.hs | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/SMTLIB/Backends.hs b/src/SMTLIB/Backends.hs index 0b28777..3203814 100644 --- a/src/SMTLIB/Backends.hs +++ b/src/SMTLIB/Backends.hs @@ -59,10 +59,6 @@ data Solver = Solver queue :: Maybe Queue } --- | Send a command in bytestring builder format to the solver. -sendSolver :: Solver -> Builder -> IO LBS.ByteString -sendSolver solver cmd = send (backend solver) cmd - -- | 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 @@ -97,7 +93,7 @@ initSolver solverBackend lazy = do -- *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 @@ -111,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