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.

Generalization of freshVar_

Generalization of freshVar

Generalization of freshArray_

Generalization of freshArray

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 getAssertions

Collectable information from the solver.

Behavior of the solver for errors.

Collectable information from the solver.

Generalization of getInfo

Generalization of getInfo

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.

Generalization of timeout

Generalization of queryDebug

Generalization of echo

Generalization of io

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.