SMTLIB.Backends.Z3

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

Documentation

data Handle

new :: IO Handle

Create a new solver instance.

close :: Handle -> IO ()

Release the resources associated with a Z3 instance.

with :: (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.