Grisette.Internal.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 Text

The solver has encountered an error.

Terminated

The solver has been terminated.

Instances

Generic SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Associated Types

type Rep SolvingFailure :: Type -> Type

Methods

from :: SolvingFailure -> Rep SolvingFailure x

to :: Rep SolvingFailure x -> SolvingFailure

Show SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

showsPrec :: Int -> SolvingFailure -> ShowS

show :: SolvingFailure -> String

showList :: [SolvingFailure] -> ShowS

Binary SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

put :: SolvingFailure -> Put

get :: Get SolvingFailure

putList :: [SolvingFailure] -> Put

Serial SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

serialize :: MonadPut m => SolvingFailure -> m ()

deserialize :: MonadGet m => m SolvingFailure

Serialize SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

put :: Putter SolvingFailure

get :: Get SolvingFailure

NFData SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

rnf :: SolvingFailure -> ()

Eq SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

(==) :: SolvingFailure -> SolvingFailure -> Bool

(/=) :: SolvingFailure -> SolvingFailure -> Bool

PPrint SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

pformat :: SolvingFailure -> Doc ann

pformatPrec :: Int -> SolvingFailure -> Doc ann

pformatList :: [SolvingFailure] -> Doc ann

Hashable SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

hashWithSalt :: Int -> SolvingFailure -> Int

hash :: SolvingFailure -> Int

Lift SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

Methods

lift :: Quote m => SolvingFailure -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => SolvingFailure -> Code m SolvingFailure

type Rep SolvingFailure

Defined in Grisette.Internal.Core.Data.Class.Solver

type Rep SolvingFailure = D1 ('MetaData "SolvingFailure" "Grisette.Internal.Core.Data.Class.Solver" "grisette-0.9.0.0-8b30m8DmEAJELhVBobm0Vc" 'False) ((C1 ('MetaCons "Unsat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unk" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ResultNumLimitReached" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SolvingError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "Terminated" 'PrefixI 'False) (U1 :: Type -> Type))))

class Monad m => 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 ()

monadicSolverResetAssertions :: m ()

monadicSolverAssert :: SymBool -> m ()

monadicSolverCheckSat :: m (Either SolvingFailure Model)

Instances

MonadIO m => MonadicSolver (SBVIncrementalT m)

Defined in Grisette.Internal.Backend.Solving

Methods

monadicSolverPush :: Int -> SBVIncrementalT m ()

monadicSolverPop :: Int -> SBVIncrementalT m ()

monadicSolverResetAssertions :: SBVIncrementalT m ()

monadicSolverAssert :: SymBool -> SBVIncrementalT m ()

monadicSolverCheckSat :: SBVIncrementalT m (Either SolvingFailure Model)

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

Solve a single formula with a monadic solver. Find an assignment to it to make it true.

data SolverCommand

The commands that can be sent to a solver.

Constructors

SolverAssert !SymBool

SolverCheckSat

SolverPush Int

SolverPop Int

SolverResetAssertions

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 SBVSolverHandle

Defined in Grisette.Internal.Backend.Solving

Methods

newSolver :: GrisetteSMTConfig -> IO SBVSolverHandle

class Solver handle where

A class that abstracts the solver interface.

Minimal complete definition

solverRunCommand, solverCheckSat, solverTerminate, solverForceTerminate

Methods

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

Run a solver command.

solverAssert :: handle -> SymBool -> IO (Either SolvingFailure ())

Assert a formula.

solverCheckSat :: handle -> 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.

solverResetAssertions :: handle -> IO (Either SolvingFailure ())

Reset all assertions in the solver.

The solver keeps all the assertions used in the previous commands:

>>> solver <- newSolver z3
>>> solverSolve solver "a"
Right (Model {a -> true :: Bool})
>>> solverSolve solver $ symNot "a"
Left Unsat

You can clear the assertions using solverResetAssertions:

>>> solverResetAssertions solver
Right ()
>>> solverSolve solver $ symNot "a"
Right (Model {a -> false :: Bool})

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.Internal.Backend.Solving

Methods

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

solverAssert :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure ())

solverCheckSat :: SBVSolverHandle -> IO (Either SolvingFailure Model)

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

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

solverResetAssertions :: SBVSolverHandle -> IO (Either SolvingFailure ())

solverTerminate :: SBVSolverHandle -> IO ()

solverForceTerminate :: SBVSolverHandle -> IO ()

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

Solve a single formula. Find an assignment to it to make it true.

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.

When an exception happens, this will forcibly terminate the solver.

Note: if Grisette is compiled with sbv < 10.10, the solver likely won't be really terminated until it has finished the last action, and this will result in long-running or zombie solver instances.

This was due to a bug in sbv, which is fixed in https://github.com/LeventErkok/sbv/pull/695.

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

solverSolveMulti

Arguments

:: Solver handle

=> handle

solver handle

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

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 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 (Union (Either e v)) Union e v

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

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

UnionWithExcept (Union (CBMCEither e v)) Union e v

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

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

Defined in Grisette.Internal.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.Internal.Core.Data.Class.Solver

Methods

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

solverSolveExcept

Arguments

:: (UnionWithExcept t u e v, PlainUnion u, Functor u, Solver handle)

=> handle

solver handle

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

solveExcept

Arguments

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

>>> import Control.Monad.Except
>>> let x = "x" :: SymInteger
>>> :{
  res :: ExceptT AssertionError Union ()
  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 z3 translate res
Right (Model {x -> 1 :: Integer})

solverSolveMultiExcept

Arguments

:: (UnionWithExcept t u e v, PlainUnion u, Functor u, Solver handle)

=> handle

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.

solveMultiExcept

Arguments

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