grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.Solver

Description

 
Synopsis

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

UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

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

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 (precise 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], failure) 

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