SMTLIB.Backends.Process

A module providing a backend that launches solvers as external processes.

Documentation

data Config

Constructors

Config

Fields

• exe :: String

  The command to call to run the solver.

• args :: [String]

  Arguments to pass to the solver's command.

• reportError :: ByteString -> IO ()

  A function for logging the solver process' messages on stderr and file handle exceptions. If you want line breaks between each log message, you need to implement it yourself, e.g use putStr . (<> "n").

Instances

Default Config

By default, use Z3 as an external process and ignore log messages.

Defined in SMTLIB.Backends.Process

Methods

def :: Config

data Handle

Constructors

Handle

Fields

• process :: Process Handle Handle Handle

  The process running the solver.

• errorReader :: Async ()

  A process reading the solver's error messages and logging them.

new

Arguments

:: Config

The solver process' configuration.

-> IO Handle

Run a solver as a process. Failures relative to terminating the process are logged and discarded.

wait :: Handle -> IO ExitCode

Wait for the process to exit and cleanup its resources.

close :: Handle -> IO ()

Terminate the process, wait for it to actually exit and cleanup its resources. Don't use this if you're manually stopping the solver process by sending an (exit) command. Use wait instead.

with

Arguments

:: Config

The solver process' configuration.

-> (Handle -> IO a)

The computation to run with the solver process

-> IO a

Create a solver process, use it to make a computation and stop it. Don't use this if you're manually stopping the solver process by sending an (exit) command. Use \config -> bracket (new config) wait instead.

toBackend :: Handle -> Backend

Make the solver process into an SMT-LIB backend.