SMTLIB.Backends.Z3

A module providing a backend that sends commands to Z3 using its C API.

Documentation

newtype Config

Constructors

Config

Fields

• parameters :: [(ByteString, ByteString)]

  A list of options to set during the solver's initialization. Each pair is of the form (paramId, paramValue), e.g. (":produce-models", "true").

data Handle

defaultConfig :: Config

By default, don't set any options during initialization.

new :: Config -> IO Handle

Create a new solver instance.

close :: Handle -> IO ()

Release the resources associated with a Z3 instance.

with :: Config -> (Handle -> IO a) -> IO a

Create a Z3 instance, use it to run a computation and release its resources.

toBackend :: Handle -> Backend

Create a solver backend out of a Z3 instance.