Safe Haskell	Safe-Inferred
Language	Haskell2010

SMTLIB.Backends

Synopsis

data Backend = Backend {
- send :: Builder -> IO ByteString
- send_ :: Builder -> IO ()
}
data QueuingFlag
- = NoQueuing
- | Queuing
data Solver
initSolver :: QueuingFlag -> Backend -> IO Solver
command :: Solver -> Builder -> IO ByteString
command_ :: Solver -> Builder -> IO ()
flushQueue :: Solver -> IO ()

Documentation

data Backend Source #

The type of solver backends. SMTLib2 commands are sent to a backend which processes them and outputs the solver's response.

Constructors

Backend

Fields

send :: Builder -> IO ByteString
Send a command to the backend. While the implementation depends on the backend, this function is usually *not* thread-safe.
send_ :: Builder -> IO ()
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.

data QueuingFlag Source #

Whether to enable queuing for a Solver.

Constructors

NoQueuing

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.

Queuing

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.

data Solver Source #

A solver is essentially a wrapper around a solver backend. It also comes an optional queue of commands to send to the backend.

initSolver Source #

Arguments

:: QueuingFlag	whether to enable `Queuing` mode
-> Backend	the solver backend
-> IO Solver

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 Queuing mode. This should not be overriden manually.

command :: Solver -> Builder -> IO ByteString Source #

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.

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 () Source #

A command with no interesting result. 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.

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.

flushQueue :: Solver -> IO () Source #

Force the content of the queue to be sent to the solver. Only useful in queuing mode, does nothing in non-queuing mode.