smtlib-backends 0.2 → 0.3
raw patch · 3 files changed
+129/−66 lines, 3 filesdep ~basedep ~bytestring
Dependency ranges changed: base, bytestring
Files
- CHANGELOG.md +34/−5
- smtlib-backends.cabal +7/−7
- src/SMTLIB/Backends.hs +88/−54
CHANGELOG.md view
@@ -1,11 +1,40 @@-see also the changelogs of `smtlib-backends-tests`, `smtlib-backends-process` and -`smtlib-backends-z3`+# Changelog -# v0.2+All notable changes to the smtlib-backends library will be documented in this+file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to [PVP versioning](https://pvp.haskell.org/).++The same stands for the changelogs of+[smtlib-backends-tests](smtlib-backends-tests/CHANGELOG.md),+[smtlib-backends-process](smtlib-backends-process/CHANGELOG.md) and+[smtlib-backends-z3](smtlib-backends-z3/CHANGELOG.md), except the version+numbers simply follow that of `smtlib-backends`.++## v0.3 _(2023-02-03)_++### Added+- **(breaking change)** add a datatype `Backends.QueuingFlag` to set the queuing+ mode+ - the `initSolver` function now takes this datatype as argument instead of a+ boolean+- **(breaking change)** add a `send_` method to the `Backends.Backend` datatype+ for sending commands with no output+- add a `Backends.flushQueue` function for forcing the content of the queue to+ be evaluated++### Changed+- **(breaking change)** make the queuing functions thread-unsafe but faster++## v0.2 _(2022-12-16)_++### Changed - split the `Process` module into its own library - rename `SMTLIB.Backends`'s `ackCommand` to `command_`+- improve read-me++### Removed - remove logging abilities - the user can always surround `command` or `command_` with their own logging functions-- improve read-me-
smtlib-backends.cabal view
@@ -1,13 +1,13 @@ name: smtlib-backends-version: 0.2+version: 0.3 synopsis: Low-level functions for SMT-LIB-based interaction with SMT solvers. description: This library provides an extensible interface for interacting with SMT solvers- using SMT-LIB. The smtlib-backends-process provides a backend that runs solvers- as external processes, and the smtlib-backends-z3 package provides a backend that- uses inlined calls to Z3's C API.+ using SMT-LIB. The smtlib-backends-process package provides a backend that+ runs solvers as external processes, and the smtlib-backends-z3 package+ provides a backend that uses inlined calls to Z3's C API. license: MIT license-file: LICENSE@@ -25,7 +25,7 @@ source-repository this type: git location: https://github.com/tweag/smtlib-backends- tag: 0.2+ tag: 0.3 library hs-source-dirs: src@@ -33,7 +33,7 @@ exposed-modules: SMTLIB.Backends other-extensions: Safe build-depends:- base >=4.14 && <4.17.0- , bytestring >=0.10.12 && <0.11+ base >=4.14 && <4.18+ , bytestring >=0.10.12 && <0.12 default-language: Haskell2010
src/SMTLIB/Backends.hs view
@@ -1,11 +1,21 @@ {-# LANGUAGE OverloadedStrings #-} -module SMTLIB.Backends (Backend (..), Solver, initSolver, command, command_) where+module SMTLIB.Backends+ ( Backend (..),+ QueuingFlag (..),+ Solver,+ initSolver,+ command,+ command_,+ flushQueue,+ )+where +import Control.Monad ((<=<)) import Data.ByteString.Builder (Builder) import qualified Data.ByteString.Lazy.Char8 as LBS import Data.Char (isSpace)-import Data.IORef (IORef, atomicModifyIORef, newIORef)+import Data.IORef (IORef, modifyIORef, newIORef, readIORef, writeIORef) import Data.List (intersperse) import Prelude hiding (log) @@ -13,45 +23,60 @@ -- processes them and outputs the solver's response. data Backend = Backend { -- | Send a command to the backend.- send :: Builder -> IO LBS.ByteString+ -- While the implementation depends on the backend, this function is usually+ -- *not* thread-safe.+ send :: Builder -> IO LBS.ByteString,+ -- | Send a command that doesn't produce any response to the backend.+ -- The backend may implement this by not reading the output and leaving it+ -- for a later read, or reading the output and discarding it immediately.+ -- Hence this method should only be used when the command does not produce+ -- any response to be outputted.+ -- Again, this function may not be thread-safe.+ send_ :: Builder -> IO () } type Queue = IORef Builder +-- | A boolean-equivalent datatype indicating whether to enable queuing.+data QueuingFlag = Queuing | NoQueuing+ -- | Push a command on the solver's queue of commands to evaluate. -- The command must not produce any output when evaluated, unless it is the last -- command added before the queue is flushed.-putQueue :: Queue -> Builder -> IO ()-putQueue q cmd = atomicModifyIORef q $ \cmds ->- (cmds <> cmd, ())+-- For a fixed queue, this function is *not* thread-safe.+put :: Queue -> Builder -> IO ()+put q cmd = modifyIORef q (<> cmd) -- | Empty the queue of commands to evaluate and return its content as a bytestring -- builder.-flushQueue :: Queue -> IO Builder-flushQueue q = atomicModifyIORef q $ \cmds ->- (mempty, cmds)+-- For a fixed queue, this function is *not* thread-safe.+flush :: Queue -> IO Builder+flush q = do+ cmds <- readIORef q+ writeIORef q mempty+ return cmds --- | 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.+-- | A solver is essentially a wrapper around a solver backend. It also comes an+-- optional queue of commands to send to the backend. ----- A solver can either be in eager mode or lazy mode. In eager mode, the queue of--- commands isn't used and the commands are sent to the backend immediately. In--- lazy mode, commands whose output are not strictly necessary for the rest of the--- computation (typically the ones whose output should just be "success") and that--- are sent through 'command_' are not sent to the backend immediately, but--- rather written on the solver's queue. When a command whose output is actually--- necessary needs to be sent, the queue is flushed and sent as a batch to the--- backend.+-- A solver can either be in 'Queuing' mode or 'NoQueuing' mode. In 'NoQueuing'+-- mode, the queue of commands isn't used and the commands are sent to the+-- backend immediately. In 'Queuing' mode, commands whose output are not+-- strictly necessary for the rest of the computation (typically the ones whose+-- output should just be @success@) and that are sent through 'command_' are not+-- sent to the backend immediately, but rather written on the solver's queue.+-- When a command whose output is actually necessary needs to be sent, the queue+-- is flushed and sent as a batch to the backend. ----- Lazy mode should be faster as there usually is a non-negligible constant--- overhead in sending a command to the backend. But since the commands are sent by--- batches, a command sent to the solver will only produce an error when the queue--- is flushed, i.e. when a command with interesting output is sent. You thus--- probably want to stick with eager mode when debugging. Moreover, when commands--- are sent by batches, only the last command in the batch may produce an output--- for parsing to work properly. Hence the ":print-success" option is disabled in--- lazy mode, and this should not be overriden manually.+-- 'Queuing' mode should be faster as there usually is a non-negligible constant+-- overhead in sending a command to the backend. But since the commands are sent+-- by batches, a command sent to the solver will only produce an error when the+-- queue is flushed, i.e. when a command with interesting output is sent. You+-- thus probably want to stick with 'NoQueuing' mode when debugging. Moreover,+-- when commands are sent by batches, only the last command in the batch may+-- produce an output for parsing to work properly. Hence the @:print-success@+-- option is disabled in 'Queuing' mode, and this should not be overriden+-- manually. data Solver = Solver { -- | The backend processing the commands. backend :: Backend,@@ -61,29 +86,31 @@ -- | 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--- not be overriden manually.+-- In particular, the "print-success" option is disabled in 'Queuing' mode. This+-- should not be overriden manually. initSolver ::+ -- | whether to enable 'Queuing' mode (see 'Solver' for the meaning of this+ -- flag)+ QueuingFlag ->+ -- | the solver backend Backend ->- -- | whether to enable lazy mode (see 'Solver' for the meaning of this flag)- Bool -> IO Solver-initSolver solverBackend lazy = do- solverQueue <-- if lazy- then do- ref <- newIORef mempty- return $ Just ref- else return Nothing+initSolver queuing solverBackend = do+ solverQueue <- case queuing of+ Queuing -> do+ ref <- newIORef mempty+ return $ Just ref+ NoQueuing -> return Nothing 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- -- the outputs of commands that are actually interesting- -- TODO checking for correctness and enabling laziness can be made compatible- -- but it would require the solver backends to return several outputs at once- -- alternatively, we may consider that the user wanting both features should- -- implement their own backend that deals with this+ case queuing of+ Queuing -> return ()+ NoQueuing ->+ -- this should not be enabled when the queue is used, as it messes with parsing+ -- the outputs of commands that are actually interesting+ -- TODO checking for correctness and enabling laziness can be made compatible+ -- but it would require the solver backends to return several outputs at once+ -- alternatively, we may consider that the user wanting both features should+ -- implement their own backend that deals with this setOption solver "print-success" "true" setOption solver "produce-models" "true" return solver@@ -91,18 +118,20 @@ -- | 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.+-- For a fixed backend, this function is *not* thread-safe. command :: Solver -> Builder -> IO LBS.ByteString command solver cmd = do send (backend solver) =<< case queue solver of- Nothing -> return $ cmd- Just q -> (<> cmd) <$> flushQueue q+ Nothing -> return cmd+ Just q -> (<> cmd) <$> flush q -- | A command with no interesting result.--- In eager mode, the result is checked for correctness.--- In lazy mode, (unless the queue is flushed and evaluated--- right after) the command must not produce any output when evaluated, and--- its output is thus in particular not checked for correctness.+-- In 'NoQueuing' mode, the result is checked for correctness. In 'Queuing'+-- mode, (unless the queue is flushed and evaluated right after) the command+-- must not produce any output when evaluated, and its output is thus in+-- particular not checked for correctness. For a fixed backend, this function is+-- *not* thread-safe. command_ :: Solver -> Builder -> IO () command_ solver cmd = case queue solver of@@ -117,9 +146,14 @@ " Expected: success", " Got: " ++ show res ]- Just q -> putQueue q cmd+ Just q -> put q cmd where trim = LBS.dropWhile isSpace . LBS.reverse . LBS.dropWhile isSpace . LBS.reverse++-- | Force the content of the queue to be sent to the solver.+-- Only useful in queuing mode, does nothing in non-queuing mode.+flushQueue :: Solver -> IO ()+flushQueue solver = maybe (return ()) (send_ (backend solver) <=< flush) $ queue solver setOption :: Solver -> Builder -> Builder -> IO () setOption solver name value = command_ solver $ list ["set-option", ":" <> name, value]