The current failures that can be returned by the solver.

A monadic solver interface.

This interface abstract the monadic interface of a solver. All the operations performed in the monad are using a single solver instance. The solver instance is management by the monad's run function.

The commands that can be sent to a solver.

A class that abstracts the creation of a solver instance based on a configuration.

The solver instance will need to be terminated by the user, with the solver interface.

A class that abstracts the solver interface.

Start a solver, run a computation with the solver, and terminate the solver after the computation finishes.

Solve a single formula. Find an assignment to it to make it true.

>>> solve (precise z3) ("a" .&& ("b" :: SymInteger) .== 1)
Right (Model {a -> True :: Bool, b -> 1 :: Integer})
>>> solve (precise z3) ("a" .&& symNot "a")
Left Unsat

Solve a single formula while returning multiple models to make it true. The maximum number of desired models are given.

>>> solveMulti (precise z3) 4 ("a" .|| "b")
[Model {a -> True :: Bool, b -> False :: Bool},Model {a -> False :: Bool, b -> True :: Bool},Model {a -> True :: Bool, b -> True :: Bool}]

A class that abstracts the union-like structures that contains exceptions.

Solver procedure for programs with error handling.

>>> :set -XLambdaCase
>>> import Control.Monad.Except
>>> let x = "x" :: SymInteger
>>> :{
  res :: ExceptT AssertionError UnionM ()
  res = do
    symAssert $ x .> 0       -- constrain that x is positive
    symAssert $ x .< 2       -- constrain that x is less than 2
:}

>>> :{
  translate (Left _) = con False -- errors are not desirable
  translate _ = con True         -- non-errors are desirable
:}

>>> solveExcept (precise z3) translate res
Right (Model {x -> 1 :: Integer})

Solver procedure for programs with error handling. Would return multiple models if possible.