smtlib-backends 0.3 → 0.4
raw patch · 3 files changed
+58/−40 lines, 3 filesdep ~basenew-uploader
Dependency ranges changed: base
Files
- CHANGELOG.md +6/−0
- smtlib-backends.cabal +7/−5
- src/SMTLIB/Backends.hs +45/−35
CHANGELOG.md view
@@ -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
smtlib-backends.cabal view
@@ -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
src/SMTLIB/Backends.hs view
@@ -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) <> ")"