Grisette.Core.Data.Class.Solver

Note for the examples

The examples assumes that the z3 solver is available in PATH.

Solver interfaces

data SolvingFailure

The current failures that can be returned by the solver.

Constructors

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

Defined in Grisette.Core.Data.Class.Solver

Methods

showsPrec :: Int -> SolvingFailure -> ShowS

show :: SolvingFailure -> String

showList :: [SolvingFailure] -> ShowS

class MonadicSolver m where

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.

Methods

monadicSolverPush :: Int -> m ()

monadicSolverPop :: Int -> m ()

monadicSolverSolve :: SymBool -> m (Either SolvingFailure Model)

Instances

MonadIO m => MonadicSolver (SBVIncrementalT n m)

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

Methods

monadicSolverPush :: Int -> SBVIncrementalT n m ()

monadicSolverPop :: Int -> SBVIncrementalT n m ()

monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model)

data SolverCommand

The commands that can be sent to a solver.

Constructors

SolverSolve SymBool

SolverPush Int

SolverPop Int

SolverTerminate

class Solver handle => ConfigurableSolver config handle | config -> handle where

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.

Methods

newSolver :: config -> IO handle

Instances

ConfigurableSolver (GrisetteSMTConfig n) SBVSolverHandle

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

Methods

newSolver :: GrisetteSMTConfig n -> IO SBVSolverHandle

class Solver handle where

A class that abstracts the solver interface.

Minimal complete definition

solverRunCommand, solverSolve, solverTerminate, solverForceTerminate

Methods

solverRunCommand :: (handle -> IO (Either SolvingFailure a)) -> handle -> SolverCommand -> IO (Either SolvingFailure a)

Run a solver command.

solverSolve :: handle -> SymBool -> IO (Either SolvingFailure Model)

Solve a formula.

solverPush :: handle -> Int -> IO (Either SolvingFailure ())

Push n levels.

solverPop :: handle -> Int -> IO (Either SolvingFailure ())

Pop n levels.

solverTerminate :: handle -> IO ()

Terminate the solver, wait until the last command is finished.

solverForceTerminate :: handle -> IO ()

Force terminate the solver, do not wait for the last command to finish.

Instances

Solver SBVSolverHandle

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

Methods

solverRunCommand :: (SBVSolverHandle -> IO (Either SolvingFailure a)) -> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a)

solverSolve :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure Model)

solverPush :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ())

solverPop :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ())

solverTerminate :: SBVSolverHandle -> IO ()

solverForceTerminate :: SBVSolverHandle -> IO ()

withSolver :: ConfigurableSolver config handle => config -> (handle -> IO a) -> IO a

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

solve

Arguments

:: 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

solveMulti

Arguments

:: 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

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

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)

solveExcept

Arguments

:: (UnionWithExcept t u e v, UnionPrjOp 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})

solveMultiExcept

Arguments

:: (UnionWithExcept t u e v, UnionPrjOp 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.