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.

• std_err :: StdStream

  How to handle std_err of the solver.

data Handle

Constructors

Handle

Fields

• process :: ProcessHandle

  The process running the solver.

• hIn :: Handle

  The input channel of the process.

• hOut :: Handle

  The output channel of the process.

• hMaybeErr :: Maybe Handle

  The error channel of the process.

defaultConfig :: Config

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

new

Arguments

:: Config

The solver process' configuration.

-> IO Handle

Run a solver as a process.

close :: Handle -> IO ()

Cleanup the process' resources, terminate it and wait for it to actually exit.

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 close it.

toBackend :: Handle -> Backend

Make the solver process into an SMT-LIB backend.

data StdStream

Constructors

Inherit

Inherit Handle from parent

UseHandle Handle

Use the supplied Handle

CreatePipe

Create a new pipe. The returned Handle will use the default encoding and newline translation mode (just like Handles created by openFile).

NoStream

Close the stream's file descriptor without passing a Handle. On POSIX systems this may lead to strange behavior in the child process because attempting to read or write after the file has been closed throws an error. This should only be used with child processes that don't use the file descriptor at all. If you wish to ignore the child process's output you should either create a pipe and drain it manually or pass a Handle that writes to /dev/null.

Instances

Show StdStream

Defined in System.Process.Common

Methods

showsPrec :: Int -> StdStream -> ShowS

show :: StdStream -> String

showList :: [StdStream] -> ShowS

Eq StdStream

Defined in System.Process.Common

Methods

(==) :: StdStream -> StdStream -> Bool

(/=) :: StdStream -> StdStream -> Bool