Data.SBV.Trans.Control

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

User queries

class MonadIO m => ExtractIO m where

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)

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

Instances

ExtractIO IO

Trivial IO extraction for IO.

Defined in Data.SBV.Utils.ExtractIO

Methods

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

ExtractIO m => ExtractIO (MaybeT m)

IO extraction for MaybeT.

Defined in Data.SBV.Utils.ExtractIO

Methods

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

ExtractIO m => ExtractIO (ExceptT e m)

IO extraction for ExceptT.

Defined in Data.SBV.Utils.ExtractIO

Methods

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

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

IO extraction for lazy WriterT.

Defined in Data.SBV.Utils.ExtractIO

Methods

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

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

IO extraction for strict WriterT.

Defined in Data.SBV.Utils.ExtractIO

Methods

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

class Monad m => MonadQuery m where

Computations which support query operations.

Minimal complete definition

Nothing

Methods

queryState :: m State

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

Instances

MonadQuery Q

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

queryState :: Q State

MonadQuery m => MonadQuery (MaybeT m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: MaybeT m State

Monad m => MonadQuery (QueryT m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: QueryT m State

MonadQuery m => MonadQuery (ExceptT e m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: ExceptT e m State

MonadQuery m => MonadQuery (ReaderT r m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: ReaderT r m State

MonadQuery m => MonadQuery (StateT s m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: StateT s m State

MonadQuery m => MonadQuery (StateT s m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: StateT s m State

(MonadQuery m, Monoid w) => MonadQuery (WriterT w m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: WriterT w m State

(MonadQuery m, Monoid w) => MonadQuery (WriterT w m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: WriterT w m State

data QueryT m a

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

Instances

MonadTrans QueryT

Defined in Data.SBV.Core.Symbolic

Methods

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

MonadSymbolic Query

Defined in Data.SBV.Core.Symbolic

Methods

symbolicEnv :: Query State

MonadWriter w m => MonadWriter w (QueryT m)

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)

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)

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)

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)

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

Functor m => Functor (QueryT m)

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)

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)

Defined in Data.SBV.Core.Symbolic

Methods

liftIO :: IO a -> QueryT m a

Monad m => MonadQuery (QueryT m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: QueryT m State

MonadIO m => SolverContext (QueryT m)

QueryT as a SolverContext.

Defined in Data.SBV.Control.Utils

Methods

constrain :: SBool -> QueryT m ()

softConstrain :: SBool -> QueryT m ()

namedConstraint :: String -> SBool -> QueryT m ()

constrainWithAttribute :: [(String, String)] -> SBool -> QueryT m ()

setInfo :: String -> [String] -> QueryT m ()

setOption :: SMTOption -> QueryT m ()

setLogic :: Logic -> QueryT m ()

addAxiom :: String -> [String] -> QueryT m ()

setTimeOut :: Integer -> QueryT m ()

contextState :: QueryT m State

type Query = QueryT IO

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

Run a custom query.

Create a fresh variable

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

Generalization of freshVar_

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

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)

Generalization of freshArray_

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

Generalization of freshArray

Checking satisfiability

data CheckSatResult

Result of a checkSat or checkSatAssuming call.

Constructors

Sat

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

DSat (Maybe String)

Delta-satisfiable: A delta-sat model is available. String is the precision info, if available.

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.

Instances

Eq CheckSatResult

Defined in Data.SBV.Control.Types

Methods

(==) :: CheckSatResult -> CheckSatResult -> Bool

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

Show CheckSatResult

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> CheckSatResult -> ShowS

show :: CheckSatResult -> String

showList :: [CheckSatResult] -> ShowS

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

Generalization of checkSat

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

Generalization of ensureSat

checkSatUsing :: (MonadIO m, MonadQuery m) => String -> m CheckSatResult

Generalization of checkSatUsing

checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult

Generalization of checkSatAssuming

checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])

Generalization of checkSatAssumingWithUnsatisfiableSet

Querying the solver

Extracting values

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

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)

Generalization of getFunction

getUninterpretedValue :: (MonadIO m, MonadQuery m, HasKind a) => SBV a -> m String

Generalization of getUninterpretedValue

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

Generalization of getModel

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

Generalization of getAssignment

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

Generalization of getSMTResult

getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown

Generalization of getUnknownReason

getObservables :: (MonadIO m, MonadQuery m) => m [(Name, CV)]

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]

Generalization of getUnsatCore

Extracting a proof

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

Generalization of getProof

Extracting interpolants

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

Generalization of getInterpolantMathSAT. Use this version with MathSAT.

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

Generalization of getInterpolantZ3. Use this version with Z3.

Extracting assertions

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

Generalization of getAssertions

Getting solver information

data SMTInfoFlag

Collectable information from the solver.

Constructors

AllStatistics

AssertionStackLevels

Authors

ErrorBehavior

Name

ReasonUnknown

Version

InfoKeyword String

Instances

Show SMTInfoFlag

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTInfoFlag -> ShowS

show :: SMTInfoFlag -> String

showList :: [SMTInfoFlag] -> ShowS

data SMTErrorBehavior

Behavior of the solver for errors.

Constructors

ErrorImmediateExit

ErrorContinuedExecution

Instances

Show SMTErrorBehavior

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTErrorBehavior -> ShowS

show :: SMTErrorBehavior -> String

showList :: [SMTErrorBehavior] -> ShowS

data SMTInfoResponse

Collectable information from the solver.

Constructors

Resp_Unsupported

Resp_AllStatistics [(String, String)]

Resp_AssertionStackLevels Integer

Resp_Authors [String]

Resp_Error SMTErrorBehavior

Resp_Name String

Resp_ReasonUnknown SMTReasonUnknown

Resp_Version String

Resp_InfoKeyword String [String]

Instances

Show SMTInfoResponse

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTInfoResponse -> ShowS

show :: SMTInfoResponse -> String

showList :: [SMTInfoResponse] -> ShowS

getInfo :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse

Generalization of getInfo

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

Generalization of getInfo

Entering and exiting assertion stack

getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int

Generalization of getAssertionStackDepth

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

Generalization of push

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

Generalization of pop

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

Generalization of inNewAssertionStack

Higher level tactics

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

Generalization of caseSplit

Resetting the solver state

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

Generalization of resetAssertions

Constructing assignments

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

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

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

Generalization of exit

Controlling the solver behavior

ignoreExitCode :: SMTConfig -> Bool

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

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

Generalization of timeout

Miscellaneous

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

Generalization of queryDebug

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

Generalization of echo

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

Generalization of io

Solver options

data SMTOption

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.

Constructors

DiagnosticOutputChannel FilePath

ProduceAssertions Bool

ProduceAssignments Bool

ProduceProofs Bool

ProduceInterpolants Bool

ProduceUnsatAssumptions Bool

ProduceUnsatCores Bool

RandomSeed Integer

ReproducibleResourceLimit Integer

SMTVerbosity Integer

OptionKeyword String [String]

SetLogic Logic

SetInfo String [String]

Instances

Show SMTOption

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTOption -> ShowS

show :: SMTOption -> String

showList :: [SMTOption] -> ShowS