Grisette.Core.Data.Class.Solver

Note for the examples

The examples assumes a z3 solver available in PATH.

Union with exceptions

class UnionWithExcept t u e v | t -> u e v where

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

Methods

extractUnionExcept :: t -> u (Either e v)

Extract a union of exceptions and values from the structure.

Instances

UnionWithExcept (UnionM (Either e v)) UnionM e v

Defined in Grisette.Core.Control.Monad.UnionM

Methods

extractUnionExcept :: UnionM (Either e v) -> UnionM (Either e v)

UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v

Defined in Grisette.Core.Control.Monad.UnionM

Methods

extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v)

(Monad u, UnionLike u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

extractUnionExcept :: CBMCExceptT e u v -> u (Either e v)

UnionWithExcept (ExceptT e u v) u e v

Defined in Grisette.Core.Data.Class.Solver

Methods

extractUnionExcept :: ExceptT e u v -> u (Either e v)

Solver interfaces

class Solver config failure | config -> failure where

A solver interface.

Methods

solve

Arguments

:: config

solver configuration

-> SymBool

formula to solve, the solver will try to make it true

-> IO (Either failure Model)

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" &&~ nots "a")
Left Unsat

solveMulti

Arguments

:: config

solver configuration

-> Int

maximum number of models to return

-> SymBool

formula to solve, the solver will try to make it true

-> IO ([Model], failure)

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}]

solveAll

Arguments

:: config

solver configuration

-> SymBool

formula to solve, the solver will try to make it true

-> IO [Model]

Solve a single formula while returning multiple models to make it true. All models are returned.

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

Instances

Solver (GrisetteSMTConfig n) SolvingFailure

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

solve :: GrisetteSMTConfig n -> SymBool -> IO (Either SolvingFailure Model)

solveMulti :: GrisetteSMTConfig n -> Int -> SymBool -> IO ([Model], SolvingFailure)

solveAll :: GrisetteSMTConfig n -> SymBool -> IO [Model]

solveExcept

Arguments

:: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure)

=> config

solver configuration

-> (Either e v -> SymBool)

mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true

-> t

the program to be solved, should be a union of exception and values

-> IO (Either failure Model)

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})

solveMultiExcept

Arguments

:: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure)

=> config

solver configuration

-> Int

maximum number of models to return

-> (Either e v -> SymBool)

mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true

-> t

the program to be solved, should be a union of exception and values

-> IO ([Model], failure)

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