Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Core.Data.Class.Solver

Contents

Note for the examples
Union with exceptions
Solver interfaces

Description

Synopsis

class UnionWithExcept t u e v | t -> u e v where
- extractUnionExcept :: t -> u (Either e v)
class Solver config failure | config -> failure where
- solve :: config -> SymBool -> IO (Either failure Model)
- solveMulti :: config -> Int -> SymBool -> IO [Model]
- solveAll :: config -> SymBool -> IO [Model]
solveExcept :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure) => config -> (Either e v -> SymBool) -> t -> IO (Either failure Model)
solveMultiExcept :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure) => config -> Int -> (Either e v -> SymBool) -> t -> IO [Model]

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 Source #

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

Methods

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

Extract a union of exceptions and values from the structure.

Instances

Instances details

UnionWithExcept (UnionM (Either e v)) UnionM e v Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods extractUnionExcept :: UnionM (Either e v) -> UnionM (Either e v) Source #
UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v) Source #
(Monad u, UnionLike u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v Source #
Instance details Defined in Grisette.Core.Control.Monad.CBMCExcept Methods extractUnionExcept :: CBMCExceptT e u v -> u (Either e v) Source #
UnionWithExcept (ExceptT e u v) u e v Source #
Instance details Defined in Grisette.Core.Data.Class.Solver Methods extractUnionExcept :: ExceptT e u v -> u (Either e v) Source #

Solver interfaces

class Solver config failure | config -> failure where Source #

A solver interface.

Methods

solve Source #

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 (UnboundedReasoning z3) ("a" &&~ ("b" :: SymInteger) ==~ 1)
Right (Model {a -> True :: Bool, b -> 1 :: Integer})
>>> solve (UnboundedReasoning z3) ("a" &&~ nots "a")
Left Unsat

solveMulti Source #

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]

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

>>> solveMulti (UnboundedReasoning 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 Source #

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 (UnboundedReasoning 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

Instances details

Solver (GrisetteSMTConfig n) CheckSatResult Source #
Instance details Defined in Grisette.Backend.SBV.Data.SMT.Solving Methods solve :: GrisetteSMTConfig n -> SymBool -> IO (Either CheckSatResult Model) Source # solveMulti :: GrisetteSMTConfig n -> Int -> SymBool -> IO [Model] Source # solveAll :: GrisetteSMTConfig n -> SymBool -> IO [Model] Source #

solveExcept Source #

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 (UnboundedReasoning z3) translate res
Right (Model {x -> 1 :: Integer})

solveMultiExcept Source #

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]

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