Safe Haskell	Safe-Inferred
Language	Haskell2010

SMTLIB.Backends.Process

Description

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

Synopsis

data Config = Config {
- exe :: String
- args :: [String]
- reportError :: ByteString -> IO ()
}
data Handle = Handle {
- process :: Process Handle Handle Handle
- errorReader :: Async ()
}
new :: Config -> IO Handle
wait :: Handle -> IO ExitCode
close :: Handle -> IO ()
with :: Config -> (Handle -> IO a) -> IO a
toBackend :: Handle -> Backend

Documentation

data Config Source #

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

Instances details

Default Config Source #	By default, use Z3 as an external process and ignore log messages.
Instance details Defined in SMTLIB.Backends.Process Methods def :: Config #

data Handle Source #

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

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

Wait for the process to exit and cleanup its resources.

close :: Handle -> IO () Source #

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

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

Make the solver process into an SMT-LIB backend.