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 |
Synopsis
- data SolvingFailure
- class MonadicSolver m where
- monadicSolverPush :: Int -> m ()
- monadicSolverPop :: Int -> m ()
- monadicSolverSolve :: SymBool -> m (Either SolvingFailure Model)
- data SolverCommand
- class Solver handle => ConfigurableSolver config handle | config -> handle where
- class Solver handle where
- solverRunCommand :: (handle -> IO (Either SolvingFailure a)) -> handle -> SolverCommand -> IO (Either SolvingFailure a)
- solverSolve :: handle -> SymBool -> IO (Either SolvingFailure Model)
- solverPush :: handle -> Int -> IO (Either SolvingFailure ())
- solverPop :: handle -> Int -> IO (Either SolvingFailure ())
- solverTerminate :: handle -> IO ()
- solverForceTerminate :: handle -> IO ()
- withSolver :: ConfigurableSolver config handle => config -> (handle -> IO a) -> IO a
- solve :: ConfigurableSolver config handle => config -> SymBool -> IO (Either SolvingFailure Model)
- solveMulti :: ConfigurableSolver config handle => config -> Int -> SymBool -> IO ([Model], SolvingFailure)
- class UnionWithExcept t u e v | t -> u e v where
- extractUnionExcept :: t -> u (Either e v)
- solveExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) => config -> (Either e v -> SymBool) -> t -> IO (Either SolvingFailure Model)
- solveMultiExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) => config -> Int -> (Either e v -> SymBool) -> t -> IO ([Model], SolvingFailure)
Note for the examples
The examples assumes that the z3
solver is available in PATH
.
Solver interfaces
data SolvingFailure Source #
The current failures that can be returned by the solver.
Unsat | Unsatisfiable: No model is available. |
Unk | Unknown: The solver cannot determine whether the formula is satisfiable. |
ResultNumLimitReached | The solver has reached the maximum number of models to return. |
SolvingError SomeException | The solver has encountered an error. |
Terminated | The solver has been terminated. |
Instances
Show SolvingFailure Source # | |
Defined in Grisette.Internal.Core.Data.Class.Solver showsPrec :: Int -> SolvingFailure -> ShowS # show :: SolvingFailure -> String # showList :: [SolvingFailure] -> ShowS # |
class MonadicSolver m where Source #
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.
monadicSolverPush :: Int -> m () Source #
monadicSolverPop :: Int -> m () Source #
monadicSolverSolve :: SymBool -> m (Either SolvingFailure Model) Source #
Instances
MonadIO m => MonadicSolver (SBVIncrementalT n m) Source # | |
Defined in Grisette.Internal.Backend.Solving monadicSolverPush :: Int -> SBVIncrementalT n m () Source # monadicSolverPop :: Int -> SBVIncrementalT n m () Source # monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model) Source # |
data SolverCommand Source #
The commands that can be sent to a solver.
class Solver handle => ConfigurableSolver config handle | config -> handle where Source #
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.
Instances
class Solver handle where Source #
A class that abstracts the solver interface.
solverRunCommand :: (handle -> IO (Either SolvingFailure a)) -> handle -> SolverCommand -> IO (Either SolvingFailure a) Source #
Run a solver command.
solverSolve :: handle -> SymBool -> IO (Either SolvingFailure Model) Source #
Solve a formula.
solverPush :: handle -> Int -> IO (Either SolvingFailure ()) Source #
Push n
levels.
solverPop :: handle -> Int -> IO (Either SolvingFailure ()) Source #
Pop n
levels.
solverTerminate :: handle -> IO () Source #
Terminate the solver, wait until the last command is finished.
solverForceTerminate :: handle -> IO () Source #
Force terminate the solver, do not wait for the last command to finish.
Instances
Solver SBVSolverHandle Source # | |
Defined in Grisette.Internal.Backend.Solving solverRunCommand :: (SBVSolverHandle -> IO (Either SolvingFailure a)) -> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a) Source # solverSolve :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure Model) Source # solverPush :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ()) Source # solverPop :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ()) Source # solverTerminate :: SBVSolverHandle -> IO () Source # solverForceTerminate :: SBVSolverHandle -> IO () Source # |
withSolver :: ConfigurableSolver config handle => config -> (handle -> IO a) -> IO a Source #
Start a solver, run a computation with the solver, and terminate the solver after the computation finishes.
:: ConfigurableSolver config handle | |
=> config | solver configuration |
-> SymBool | formula to solve, the solver will try to make it true |
-> IO (Either SolvingFailure 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" .&& symNot "a")
Left Unsat
:: ConfigurableSolver config handle | |
=> config | solver configuration |
-> Int | maximum number of models to return |
-> SymBool | formula to solve, the solver will try to make it true |
-> IO ([Model], SolvingFailure) |
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}]
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.
extractUnionExcept :: t -> u (Either e v) Source #
Extract a union of exceptions and values from the structure.
Instances
UnionWithExcept (UnionM (Either e v)) UnionM e v Source # | |
Defined in Grisette.Internal.Core.Control.Monad.UnionM | |
UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v) Source # | |
(Monad u, TryMerge u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept extractUnionExcept :: CBMCExceptT e u v -> u (Either e v) Source # | |
UnionWithExcept (ExceptT e u v) u e v Source # | |
Defined in Grisette.Internal.Core.Data.Class.Solver extractUnionExcept :: ExceptT e u v -> u (Either e v) Source # |
:: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) | |
=> 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 SolvingFailure 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})
:: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) | |
=> 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], SolvingFailure) |
Solver procedure for programs with error handling. Would return multiple models if possible.