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.

Computations which support query operations.

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

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

Run a custom query.

Result of a checkSat or checkSatAssuming call.

Generalization of checkSat

Generalization of ensureSat

Generalization of checkSatUsing

Generalization of checkSatAssuming

Generalization of checkSatAssumingWithUnsatisfiableSet

Generalization of getValue

Generalization of getFunction

Generalization of getUninterpretedValue

Generalization of getModel

Generalization of getAssignment

Generalization of getSMTResult

Generalization of getUnknownReason

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

Generalization of getUnsatCore

Generalization of getProof

Generalization of getInterpolantMathSAT. Use this version with MathSAT.

Generalization of getInterpolantZ3. Use this version with Z3.

Generalization of getAbduct.

Generalization of getAbductNext.

Generalization of getAssertions

Collectable information from the solver.

Behavior of the solver for errors.

Collectable information from the solver.

Generalization of getInfo

Generalization of getOption

Generalization of getAssertionStackDepth

Generalization of push

Generalization of pop

Generalization of inNewAssertionStack

Generalization of caseSplit

Generalization of resetAssertions

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.

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.

Generalization of exit

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

Timeout a query action, typically a command call to the underlying SMT solver. The duration is in microseconds (1/10^6 seconds). If the duration is negative, then no timeout is imposed. When specifying long timeouts, be careful not to exceed maxBound :: Int. (On a 64 bit machine, this bound is practically infinite. But on a 32 bit machine, it corresponds to about 36 minutes!)

Semantics: The call timeout n q causes the timeout value to be applied to all interactive calls that take place as we execute the query q. That is, each call that happens during the execution of q gets a separate time-out value, as opposed to one timeout value that limits the whole query. This is typically the intended behavior. It is advisable to apply this combinator to calls that involve a single call to the solver for finer control, as opposed to an entire set of interactions. However, different use cases might call for different scenarios.

If the solver responds within the time-out specified, then we continue as usual. However, if the backend solver times-out using this mechanism, there is no telling what the state of the solver will be. Thus, we raise an error in this case.

Generalization of queryDebug

Generalization of echo

Generalization of io

Option values that can be set in the solver, following the SMTLib specification https://smt-lib.org/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.