SMTLIB.Backends

Documentation

data Backend

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

A boolean-equivalent datatype indicating whether to enable queuing.

Constructors

Queuing

NoQueuing

data Solver

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.

initSolver

Arguments

:: QueuingFlag

whether to enable Queuing mode (see Solver for the meaning of this flag)

-> 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

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

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. For a fixed backend, this function is *not* thread-safe.

flushQueue :: Solver -> IO ()

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