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.

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

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.

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

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

When an exception happens, this will forcibly terminate the solver.

Note: if Grisette is compiled with sbv < 10.10, the solver likely won't be really terminated until it has finished the last action, and this will result in long-running or zombie solver instances.

This was due to a bug in sbv, which is fixed in https://github.com/LeventErkok/sbv/pull/695.

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

>>> solve z3 ("a" .&& ("b" :: SymInteger) .== 1)
Right (Model {a -> true :: Bool, b -> 1 :: Integer})
>>> solve 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.

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

>>> solveMulti 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.

Solver procedure for programs with error handling.

>>> import Control.Monad.Except
>>> let x = "x" :: SymInteger
>>> :{
  res :: ExceptT AssertionError Union ()
  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 z3 translate res
Right (Model {x -> 1 :: Integer})

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

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