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.

An queriable value. This is a generalization of the Fresh class, in case one needs to be more specific about how projections/embeddings are done.

Create a fresh variable of some type in the underlying query monad transformer. For further control on how these variables are projected and embedded, see the Queriable class.

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

Run a custom query

Similar to freshVar, except creates unnamed variable.

NB. For a version which generalizes over the underlying monad, see freshVar_

Create a fresh variable in query mode. You should prefer creating input variables using sBool, sInt32, etc., which act as primary inputs to the model and can be existential or universal. Use freshVar only in query mode for anonymous temporary variables. Such variables are always existential. Note that freshVar should hardly be needed: Your input variables and symbolic expressions should suffice for most major use cases.

NB. For a version which generalizes over the underlying monad, see freshVar

Similar to freshArray, except creates unnamed array.

NB. For a version which generalizes over the underlying monad, see freshArray_

Create a fresh array in query mode. Again, you should prefer creating arrays before the queries start using newArray, but this method can come in handy in occasional cases where you need a new array after you start the query based interaction.

NB. For a version which generalizes over the underlying monad, see freshArray

Result of a checkSat or checkSatAssuming call.

Check for satisfiability.

NB. For a version which generalizes over the underlying monad, see checkSat

Ensure that the current context is satisfiable. If not, this function will throw an error.

NB. For a version which generalizes over the underlying monad, see ensureSat

Check for satisfiability with a custom check-sat-using command.

NB. For a version which generalizes over the underlying monad, see checkSatUsing

Check for satisfiability, under the given conditions. Similar to checkSat except it allows making further assumptions as captured by the first argument of booleans. (Also see checkSatAssumingWithUnsatisfiableSet for a variant that returns the subset of the given assumptions that led to the Unsat conclusion.)

NB. For a version which generalizes over the underlying monad, see checkSatAssuming

Check for satisfiability, under the given conditions. Returns the unsatisfiable set of assumptions. Similar to checkSat except it allows making further assumptions as captured by the first argument of booleans. If the result is Unsat, the user will also receive a subset of the given assumptions that led to the Unsat conclusion. Note that while this set will be a subset of the inputs, it is not necessarily guaranteed to be minimal.

You must have arranged for the production of unsat assumptions first via

    setOption $ ProduceUnsatAssumptions True

for this call to not error out!

Usage note: getUnsatCore is usually easier to use than checkSatAssumingWithUnsatisfiableSet, as it allows the use of named assertions, as obtained by namedConstraint. If getUnsatCore fills your needs, you should definitely prefer it over checkSatAssumingWithUnsatisfiableSet.

NB. For a version which generalizes over the underlying monad, see checkSatAssumingWithUnsatisfiableSet

Get the value of a term.

NB. For a version which generalizes over the underlying monad, see getValue

Registering an uninterpreted SMT function. This is typically not necessary as uses of the UI function itself will register it automatically. But there are cases where doing this explicitly can come in handy.

Get the value of an uninterpreted function, as a list of domain, value pairs. The final value is the "else" clause, i.e., what the function maps values outside of the domain of the first list.

Get the value of an uninterpreted sort, as a String

NB. For a version which generalizes over the underlying monad, see getUninterpretedValue

Collect model values. It is implicitly assumed that we are in a check-sat context. See getSMTResult for a variant that issues a check-sat first and returns an SMTResult.

NB. For a version which generalizes over the underlying monad, see getModel

Retrieve the assignment. This is a lightweight version of getValue, where the solver returns the truth value for all named subterms of type Bool.

You must have first arranged for assignments to be produced via

    setOption $ ProduceAssignments True

for this call to not error out!

NB. For a version which generalizes over the underlying monad, see getAssignment

Issue check-sat and get an SMT Result out.

NB. For a version which generalizes over the underlying monad, see getSMTResult

Get the reason unknown. Only internally used.

NB. For a version which generalizes over the underlying monad, see getUnknownReason

Get the observables recorded during a query run.

NB. For a version which generalizes over the underlying monad, see getObservables

Retrieve the unsat-core. Note you must have arranged for unsat cores to be produced first via

    setOption $ ProduceUnsatCores True

for this call to not error out!

NB. There is no notion of a minimal unsat-core, in case unsatisfiability can be derived in multiple ways. Furthermore, Z3 does not guarantee that the generated unsat core does not have any redundant assertions either, as doing so can incur a performance penalty. (There might be assertions in the set that is not needed.) To ensure all the assertions in the core are relevant, use:

    setOption $ OptionKeyword ":smt.core.minimize" ["true"]

Note that this only works with Z3.

NB. For a version which generalizes over the underlying monad, see getUnsatCore

Retrieve the proof. Note you must have arranged for proofs to be produced first via

    setOption $ ProduceProofs True

for this call to not error out!

A proof is simply a String, as returned by the solver. In the future, SBV might provide a better datatype, depending on the use cases. Please get in touch if you use this function and can suggest a better API.

NB. For a version which generalizes over the underlying monad, see getProof

Interpolant extraction for MathSAT. Compare with getInterpolantZ3, which performs similar function (but with a different use model) in Z3.

Retrieve an interpolant after an Unsat result is obtained. Note you must have arranged for interpolants to be produced first via

    setOption $ ProduceInterpolants True

for this call to not error out!

To get an interpolant for a pair of formulas A and B, use a constrainWithAttribute call to attach interplation groups to A and B. Then call getInterpolantMathSAT ["A"], assuming those are the names you gave to the formulas in the A group.

An interpolant for A and B is a formula I such that:

       A .=> I
   and B .=> sNot I

That is, it's evidence that A and B cannot be true together since A implies I but B implies not I; establishing that A and B cannot be satisfied at the same time. Furthermore, I will have only the symbols that are common to A and B.

NB. Interpolant extraction isn't standardized well in SMTLib. Currently both MathSAT and Z3 support them, but with slightly differing APIs. So, we support two APIs with slightly differing types to accommodate both. See Documentation.SBV.Examples.Queries.Interpolants for example usages in these solvers.

NB. For a version which generalizes over the underlying monad, see getInterpolantMathSAT

Interpolant extraction for z3. Compare with getInterpolantMathSAT, which performs similar function (but with a different use model) in MathSAT.

Unlike the MathSAT variant, you should simply call getInterpolantZ3 on symbolic booleans to retrieve the interpolant. Do not call checkSat or create named constraints. This makes it harder to identify formulas, but the current state of affairs in interpolant API requires this kludge.

An interpolant for A and B is a formula I such that:

       A ==> I
   and B ==> not I

That is, it's evidence that A and B cannot be true together since A implies I but B implies not I; establishing that A and B cannot be satisfied at the same time. Furthermore, I will have only the symbols that are common to A and B.

In Z3, interpolants generalize to sequences: If you pass more than two formulas, then you will get a sequence of interpolants. In general, for N formulas that are not satisfiable together, you will be returned N-1 interpolants. If formulas are A1 .. An, then interpolants will be I1 .. I(N-1), such that A1 ==> I1, A2 /\ I1 ==> I2, A3 /\ I2 ==> I3, ..., and finally AN ===> not I(N-1).

Currently, SBV only returns simple and sequence interpolants, and does not support tree-interpolants. If you need these, please get in touch. Furthermore, the result will be a list of mere strings representing the interpolating formulas, as opposed to a more structured type. Please get in touch if you use this function and can suggest a better API.

NB. Interpolant extraction isn't standardized well in SMTLib. Currently both MathSAT and Z3 support them, but with slightly differing APIs. So, we support two APIs with slightly differing types to accommodate both. See Documentation.SBV.Examples.Queries.Interpolants for example usages in these solvers.

NB. For a version which generalizes over the underlying monad, see getInterpolantZ3

Retrieve assertions. Note you must have arranged for assertions to be available first via

    setOption $ ProduceAssertions True

for this call to not error out!

Note that the set of assertions returned is merely a list of strings, just like the case for getProof. In the future, SBV might provide a better datatype, depending on the use cases. Please get in touch if you use this function and can suggest a better API.

NB. For a version which generalizes over the underlying monad, see getAssertions

Collectable information from the solver.

Behavior of the solver for errors.

Collectable information from the solver.

Ask solver for info.

NB. For a version which generalizes over the underlying monad, see getInfo

Retrieve the value of an 'SMTOption.' The curious function argument is on purpose here, simply pass the constructor name. Example: the call getOption ProduceUnsatCores will return either Nothing or Just (ProduceUnsatCores True) or Just (ProduceUnsatCores False).

Result will be Nothing if the solver does not support this option.

NB. For a version which generalizes over the underlying monad, see getOption

The current assertion stack depth, i.e., pops after start. Always non-negative.

NB. For a version which generalizes over the underlying monad, see getAssertionStackDepth

Push the context, entering a new one. Pushes multiple levels if n > 1.

NB. For a version which generalizes over the underlying monad, see push

Pop the context, exiting a new one. Pops multiple levels if n > 1. It's an error to pop levels that don't exist.

NB. For a version which generalizes over the underlying monad, see pop

Run the query in a new assertion stack. That is, we push the context, run the query commands, and pop it back.

NB. For a version which generalizes over the underlying monad, see inNewAssertionStack

Search for a result via a sequence of case-splits, guided by the user. If one of the conditions lead to a satisfiable result, returns Just that result. If none of them do, returns Nothing. Note that we automatically generate a coverage case and search for it automatically as well. In that latter case, the string returned will be Coverage. The first argument controls printing progress messages See Documentation.SBV.Examples.Queries.CaseSplit for an example use case.

NB. For a version which generalizes over the underlying monad, see caseSplit

Reset the solver, by forgetting all the assertions. However, bindings are kept as is, as opposed to a full reset of the solver. Use this variant to clean-up the solver state while leaving the bindings intact. Pops all assertion levels. Declarations and definitions resulting from the setLogic command are unaffected. Note that SBV implicitly uses global-declarations, so bindings will remain intact.

NB. For a version which generalizes over the underlying monad, see 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.

Produce the query result from an assignment.

NB. For a version which generalizes over the underlying monad, see mkSMTResult

Exit the solver. This action will cause the solver to terminate. Needless to say, trying to communicate with the solver after issuing "exit" will simply fail.

NB. For a version which generalizes over the underlying monad, see 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.

NB. For a version which generalizes over the underlying monad, see timeout

If verbose is True, print the message, useful for debugging messages in custom queries. Note that redirectVerbose will be respected: If a file redirection is given, the output will go to the file.

NB. For a version which generalizes over the underlying monad, see queryDebug

Echo a string. Note that the echoing is done by the solver, not by SBV.

NB. For a version which generalizes over the underlying monad, see echo

Perform an arbitrary IO action.

NB. For a version which generalizes over the underlying monad, see 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.