diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,12 @@ [smtlib-backends-z3](smtlib-backends-z3/CHANGELOG.md), except the version numbers simply follow that of `smtlib-backends`. +## v0.4 _(2024-05-28)_ + +### Changed + +- **(breaking change)** stop changing the default of the `produce-models` option. + ## v0.3 _(2023-02-03)_ ### Added diff --git a/smtlib-backends.cabal b/smtlib-backends.cabal --- a/smtlib-backends.cabal +++ b/smtlib-backends.cabal @@ -1,7 +1,7 @@ name: smtlib-backends -version: 0.3 +version: 0.4 synopsis: - Low-level functions for SMT-LIB-based interaction with SMT solvers. + Low-level functions for SMT-LIB-based interaction with SMT solvers. description: This library provides an extensible interface for interacting with SMT solvers @@ -12,7 +12,9 @@ license: MIT license-file: LICENSE author: Quentin Aristote -maintainer: quentin.aristote@tweag.io +maintainer: + facundo.dominguez@tweag.io, gabriel.hondet@tweag.io, mathieu.montin@tweag.io + build-type: Simple category: SMT cabal-version: >=1.10 @@ -33,7 +35,7 @@ exposed-modules: SMTLIB.Backends other-extensions: Safe build-depends: - base >=4.14 && <4.18 - , bytestring >=0.10.12 && <0.12 + base >=4.14 && <4.20 + , bytestring >=0.10.12 && <0.13 default-language: Haskell2010 diff --git a/src/SMTLIB/Backends.hs b/src/SMTLIB/Backends.hs --- a/src/SMTLIB/Backends.hs +++ b/src/SMTLIB/Backends.hs @@ -16,7 +16,6 @@ import qualified Data.ByteString.Lazy.Char8 as LBS import Data.Char (isSpace) import Data.IORef (IORef, modifyIORef, newIORef, readIORef, writeIORef) -import Data.List (intersperse) import Prelude hiding (log) -- | The type of solver backends. SMTLib2 commands are sent to a backend which @@ -37,8 +36,35 @@ type Queue = IORef Builder --- | A boolean-equivalent datatype indicating whether to enable queuing. -data QueuingFlag = Queuing | NoQueuing +-- | Whether to enable queuing for a 'Solver'. +data QueuingFlag + = -- | In 'NoQueuing' mode, the 'Solver' has no queue and commands are sent to + -- the backend immediately. + -- + -- In this mode, the option @:print-success@ is enabled by 'initSolver' to + -- monitor that commands are being accepted by the SMT solver. + NoQueuing + | -- | In 'Queuing' mode, commands whose output is not strictly necessary for + -- the rest of the computation (typically the ones whose output should just + -- be @success@) are not sent to the backend immediately, but rather written + -- on the solver's queue. + -- + -- It is the responsibility of the caller to identify these commands and + -- sent them through the 'command_' call. + -- + -- When a command is sent whose output is actually necessary, the queue is + -- flushed and sent as a batch to the backend. + -- + -- 'Queuing' mode should be faster as there usually is a non-negligible + -- constant overhead in sending a command to the backend. When commands are + -- sent in batches, a command sent to the solver will only produce an error + -- when it is later sent to the backend. Therefore, you probably want to + -- stick with 'NoQueuing' mode when debugging. + -- + -- For parsing to work properly, at most one of the commands in the batch + -- can produce an output. Hence the @:print-success@ option should not be + -- enabled in 'Queuing' mode. + Queuing -- | 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 @@ -58,25 +84,6 @@ -- | 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 '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. --- --- '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, @@ -89,8 +96,7 @@ -- 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) + -- | whether to enable 'Queuing' mode QueuingFlag -> -- | the solver backend Backend -> @@ -107,18 +113,23 @@ 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" + command_ solver "(set-option :print-success true)" return solver -- | 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. +-- +-- Concurrent calls to different solvers are thread-safe, but not concurrent +-- calls on the same solver or the same backend. +-- +-- Only one command must be given per invocation, or the multiple commands must +-- together produce the output of one command only. command :: Solver -> Builder -> IO LBS.ByteString command solver cmd = do send (backend solver) @@ -130,8 +141,13 @@ -- 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. +-- particular not checked for correctness. +-- +-- Concurrent calls to different solvers are thread-safe, but not concurrent +-- calls on the same solver or the same backend. +-- +-- Only one command must be given per invocation, or the multiple commands must +-- together produce the output of one command only. command_ :: Solver -> Builder -> IO () command_ solver cmd = case queue solver of @@ -154,9 +170,3 @@ -- 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] - -list :: [Builder] -> Builder -list bs = "(" <> mconcat (intersperse " " bs) <> ")"