sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Brian Schroeder
Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Trans.Control

Contents

Description

More generalized alternative to Data.SBV.Control for advanced client use

Synopsis

User queries

class MonadIO m => ExtractIO m where Source #

Monads which support IO operations and can extract all IO behavior for interoperation with functions like catches, which takes an IO action in negative position. This function can not be implemented for transformers like ReaderT r or StateT s, whose resultant IO actions are a function of some environment or state.

Methods

extractIO :: m a -> IO (m a) Source #

Law: the m a yielded by IO is pure with respect to IO.

Instances
ExtractIO IO Source #

Trivial IO extraction for IO.

Instance details

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: IO a -> IO (IO a) Source #

ExtractIO m => ExtractIO (MaybeT m) Source #

IO extraction for MaybeT.

Instance details

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: MaybeT m a -> IO (MaybeT m a) Source #

ExtractIO m => ExtractIO (ExceptT e m) Source #

IO extraction for ExceptT.

Instance details

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: ExceptT e m a -> IO (ExceptT e m a) Source #

(Monoid w, ExtractIO m) => ExtractIO (WriterT w m) Source #

IO extraction for lazy WriterT.

Instance details

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: WriterT w m a -> IO (WriterT w m a) Source #

(Monoid w, ExtractIO m) => ExtractIO (WriterT w m) Source #

IO extraction for strict WriterT.

Instance details

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: WriterT w m a -> IO (WriterT w m a) Source #

class Monad m => MonadQuery m where Source #

Computations which support query operations.

Minimal complete definition

Nothing

Methods

queryState :: m State Source #

queryState :: (MonadTrans t, MonadQuery m', m ~ t m') => m State Source #

Instances
MonadQuery Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

MonadQuery m => MonadQuery (MaybeT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Monad m => MonadQuery (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

MonadQuery m => MonadQuery (ExceptT e m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

MonadQuery m => MonadQuery (StateT s m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

MonadQuery m => MonadQuery (StateT s m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

(MonadQuery m, Monoid w) => MonadQuery (WriterT w m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

(MonadQuery m, Monoid w) => MonadQuery (WriterT w m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

MonadQuery m => MonadQuery (ReaderT r m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

data QueryT m a Source #

A query is a user-guided mechanism to directly communicate and extract results from the solver. A generalization of Query.

Instances
MonadTrans QueryT Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

lift :: Monad m => m a -> QueryT m a #

MonadSymbolic Query Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

MonadWriter w m => MonadWriter w (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

writer :: (a, w) -> QueryT m a #

tell :: w -> QueryT m () #

listen :: QueryT m a -> QueryT m (a, w) #

pass :: QueryT m (a, w -> w) -> QueryT m a #

MonadState s m => MonadState s (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

get :: QueryT m s #

put :: s -> QueryT m () #

state :: (s -> (a, s)) -> QueryT m a #

MonadReader r m => MonadReader r (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

ask :: QueryT m r #

local :: (r -> r) -> QueryT m a -> QueryT m a #

reader :: (r -> a) -> QueryT m a #

MonadError e m => MonadError e (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

throwError :: e -> QueryT m a #

catchError :: QueryT m a -> (e -> QueryT m a) -> QueryT m a #

Monad m => Monad (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

(>>=) :: QueryT m a -> (a -> QueryT m b) -> QueryT m b #

(>>) :: QueryT m a -> QueryT m b -> QueryT m b #

return :: a -> QueryT m a #

fail :: String -> QueryT m a #

Functor m => Functor (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

fmap :: (a -> b) -> QueryT m a -> QueryT m b #

(<$) :: a -> QueryT m b -> QueryT m a #

Applicative m => Applicative (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

pure :: a -> QueryT m a #

(<*>) :: QueryT m (a -> b) -> QueryT m a -> QueryT m b #

liftA2 :: (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c #

(*>) :: QueryT m a -> QueryT m b -> QueryT m b #

(<*) :: QueryT m a -> QueryT m b -> QueryT m a #

MonadIO m => MonadIO (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

liftIO :: IO a -> QueryT m a #

Monad m => MonadQuery (QueryT m) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

MonadIO m => SolverContext (QueryT m) Source #

QueryT as a SolverContext.

Instance details

Defined in Data.SBV.Control.Utils

type Query = QueryT IO Source #

A query is a user-guided mechanism to directly communicate and extract results from the solver.

query :: ExtractIO m => QueryT m a -> SymbolicT m a Source #

Run a custom query.

Create a fresh variable

freshVar_ :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => m (SBV a) Source #

Generalization of freshVar_

freshVar :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => String -> m (SBV a) Source #

Generalization of freshVar

Create a fresh array

freshArray_ :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b) Source #

Generalization of freshArray_

freshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b) Source #

Generalization of freshArray

Checking satisfiability

data CheckSatResult Source #

Result of a checkSat or checkSatAssuming call.

Constructors

Sat

Satisfiable: A model is available, which can be queried with getValue.

Unsat

Unsatisfiable: No model is available. Unsat cores might be obtained via getUnsatCore.

Unk

Unknown: Use getUnknownReason to obtain an explanation why this might be the case.

checkSat :: (MonadIO m, MonadQuery m) => m CheckSatResult Source #

Generalization of checkSat

ensureSat :: (MonadIO m, MonadQuery m) => m () Source #

Generalization of ensureSat

Querying the solver

Extracting values

getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a Source #

Generalization of getValue

getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r) => fun -> m ([(a, r)], r) Source #

Generalization of getFunction

getModel :: (MonadIO m, MonadQuery m) => m SMTModel Source #

Generalization of getModel

getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)] Source #

Generalization of getAssignment

getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult Source #

Generalization of getSMTResult

getObservables :: (MonadIO m, MonadQuery m) => m [(String, CV)] Source #

Get observables, i.e., those explicitly labeled by the user with a call to observe.

Extracting the unsat core

getUnsatCore :: (MonadIO m, MonadQuery m) => m [String] Source #

Generalization of getUnsatCore

Extracting a proof

getProof :: (MonadIO m, MonadQuery m) => m String Source #

Generalization of getProof

Extracting interpolants

getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String Source #

Generalization of getInterpolantMathSAT. Use this version with MathSAT.

getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String Source #

Generalization of getInterpolantZ3. Use this version with Z3.

Extracting assertions

getAssertions :: (MonadIO m, MonadQuery m) => m [String] Source #

Generalization of getAssertions

Getting solver information

data SMTInfoFlag Source #

Collectable information from the solver.

Instances
Show SMTInfoFlag Source # 
Instance details

Defined in Data.SBV.Control.Types

data SMTErrorBehavior Source #

Behavior of the solver for errors.

getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption) Source #

Generalization of getInfo

Entering and exiting assertion stack

push :: (MonadIO m, MonadQuery m) => Int -> m () Source #

Generalization of push

pop :: (MonadIO m, MonadQuery m) => Int -> m () Source #

Generalization of pop

inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a Source #

Generalization of inNewAssertionStack

Higher level tactics

caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult)) Source #

Generalization of caseSplit

Resetting the solver state

resetAssertions :: (MonadIO m, MonadQuery m) => m () Source #

Generalization of resetAssertions

Constructing assignments

(|->) :: SymVal a => SBV a -> a -> Assignment infix 1 Source #

Make an assignment. The type Assignment is abstract, the result is typically passed to mkSMTResult:

 mkSMTResult [ a |-> 332
             , b |-> 2.3
             , c |-> True
             ]

End users should use getModel for automatically constructing models from the current solver state. However, an explicit Assignment might be handy in complex scenarios where a model needs to be created manually.

Terminating the query

mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult Source #

Generalization of mkSMTResult NB. This function does not allow users to create interpretations for UI-Funs. But that's probably not a good idea anyhow. Also, if you use the validateModel or optimizeValidateConstraints features, SBV will fail on models returned via this function.

exit :: (MonadIO m, MonadQuery m) => m () Source #

Generalization of exit

Controlling the solver behavior

ignoreExitCode :: SMTConfig -> Bool Source #

If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.

timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a Source #

Generalization of timeout

Miscellaneous

queryDebug :: (MonadIO m, MonadQuery m) => [String] -> m () Source #

Generalization of queryDebug

echo :: (MonadIO m, MonadQuery m) => String -> m () Source #

Generalization of echo

io :: MonadIO m => IO a -> m a Source #

Generalization of io

Solver options

data SMTOption Source #

Option values that can be set in the solver, following the SMTLib specification http://smtlib.cs.uiowa.edu/language.shtml.

Note that not all solvers may support all of these!

Furthermore, SBV doesn't support the following options allowed by SMTLib.

  • :interactive-mode (Deprecated in SMTLib, use ProduceAssertions instead.)
  • :print-success (SBV critically needs this to be True in query mode.)
  • :produce-models (SBV always sets this option so it can extract models.)
  • :regular-output-channel (SBV always requires regular output to come on stdout for query purposes.)
  • :global-declarations (SBV always uses global declarations since definitions are accumulative.)

Note that SetLogic and SetInfo are, strictly speaking, not SMTLib options. However, we treat it as such here uniformly, as it fits better with how options work.

Instances
Show SMTOption Source # 
Instance details

Defined in Data.SBV.Control.Types

Generic SMTOption Source # 
Instance details

Defined in Data.SBV.Control.Types

Associated Types

type Rep SMTOption :: Type -> Type #

NFData SMTOption Source # 
Instance details

Defined in Data.SBV.Control.Types

Methods

rnf :: SMTOption -> () #

type Rep SMTOption Source # 
Instance details

Defined in Data.SBV.Control.Types

type Rep SMTOption = D1 (MetaData "SMTOption" "Data.SBV.Control.Types" "sbv-8.7-DbQHjiKtor73WzWR2O4MT3" False) (((C1 (MetaCons "DiagnosticOutputChannel" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath)) :+: (C1 (MetaCons "ProduceAssertions" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :+: C1 (MetaCons "ProduceAssignments" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))) :+: (C1 (MetaCons "ProduceProofs" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :+: (C1 (MetaCons "ProduceInterpolants" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :+: C1 (MetaCons "ProduceUnsatAssumptions" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))) :+: ((C1 (MetaCons "ProduceUnsatCores" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :+: (C1 (MetaCons "RandomSeed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: C1 (MetaCons "ReproducibleResourceLimit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)))) :+: ((C1 (MetaCons "SMTVerbosity" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: C1 (MetaCons "OptionKeyword" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [String]))) :+: (C1 (MetaCons "SetLogic" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Logic)) :+: C1 (MetaCons "SetInfo" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [String]))))))