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

class SMTValue a where Source #

A class which allows for sexpr-conversion to values

Minimal complete definition

Nothing

Methods

sexprToVal :: SExpr -> Maybe a Source #

sexprToVal :: Read a => SExpr -> Maybe a Source #

Instances
SMTValue Bool Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Bool Source #

SMTValue Char Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Char Source #

SMTValue Double Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Double Source #

SMTValue Float Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Float Source #

SMTValue Int8 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Int8 Source #

SMTValue Int16 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Int16 Source #

SMTValue Int32 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Int32 Source #

SMTValue Int64 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Int64 Source #

SMTValue Integer Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Integer Source #

SMTValue Word8 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Word8 Source #

SMTValue Word16 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Word16 Source #

SMTValue Word32 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Word32 Source #

SMTValue Word64 Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe Word64 Source #

SMTValue () Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe () Source #

SMTValue AlgReal Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe AlgReal Source #

SMTValue State Source # 
Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

sexprToVal :: SExpr -> Maybe State Source #

SMTValue E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

sexprToVal :: SExpr -> Maybe E Source #

SMTValue Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

sexprToVal :: SExpr -> Maybe Day Source #

SMTValue Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

sexprToVal :: SExpr -> Maybe Color Source #

SMTValue Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

sexprToVal :: SExpr -> Maybe Nationality Source #

SMTValue Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

sexprToVal :: SExpr -> Maybe Beverage Source #

SMTValue Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

sexprToVal :: SExpr -> Maybe Pet Source #

SMTValue Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

sexprToVal :: SExpr -> Maybe Sport Source #

SMTValue Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

sexprToVal :: SExpr -> Maybe Color Source #

SMTValue Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

sexprToVal :: SExpr -> Maybe Color Source #

SMTValue U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

sexprToVal :: SExpr -> Maybe U2Member Source #

SMTValue Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

sexprToVal :: SExpr -> Maybe Location Source #

SMTValue Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

sexprToVal :: SExpr -> Maybe Day Source #

SMTValue BinOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

sexprToVal :: SExpr -> Maybe BinOp Source #

SMTValue UnOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

sexprToVal :: SExpr -> Maybe UnOp Source #

(SMTValue a, Typeable a) => SMTValue [a] Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe [a] Source #

SMTValue a => SMTValue (Maybe a) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (Maybe a) Source #

(Ord a, SymVal a) => SMTValue (RCSet a) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (RCSet a) Source #

(SMTValue a, SMTValue b) => SMTValue (Either a b) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (Either a b) Source #

(SMTValue a, SMTValue b) => SMTValue (a, b) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (a, b) Source #

(SMTValue a, SMTValue b, SMTValue c) => SMTValue (a, b, c) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (a, b, c) Source #

(SMTValue a, SMTValue b, SMTValue c, SMTValue d) => SMTValue (a, b, c, d) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (a, b, c, d) Source #

(SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e) => SMTValue (a, b, c, d, e) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (a, b, c, d, e) Source #

(SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e, SMTValue f) => SMTValue (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (a, b, c, d, e, f) Source #

(SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e, SMTValue f, SMTValue g) => SMTValue (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (a, b, c, d, e, f, g) Source #

(SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e, SMTValue f, SMTValue g, SMTValue h) => SMTValue (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (a, b, c, d, e, f, g, h) Source #

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

Generalization of getValue

getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, 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

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

Generalization of getInterpolant

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.3-KY4PN9PPbrH5uMg2KovlBp" 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]))))))