Configures how to approximate unbounded values.

For example, if we use Approx (Proxy :: Proxy 4) to approximate the following unbounded integer:

(+ a 9)

We will get

(bvadd a #x9)

Here the value 9 will be approximated to a 4-bit bit vector, and the operation bvadd will be used instead of +.

Note that this approximation may not be sound. See GrisetteSMTConfig for more details.

Grisette specific extra configurations for the SBV backend.

A precise reasoning configuration with the given SBV solver configuration.

An approximate reasoning configuration with the given SBV solver configuration.

Set the timeout for the solver configuration.

Clear the timeout for the solver configuration.

Set the reasoning precision for the solver configuration.

Clear the reasoning precision and perform precise reasoning with the solver configuration.

Solver configuration for the Grisette SBV backend. A Grisette solver configuration consists of a SBV solver configuration and the reasoning precision.

Integers can be unbounded (mathematical integer) or bounded (machine integer/bit vector). The two types of integers have their own use cases, and should be used to model different systems. However, the solvers are known to have bad performance on some unbounded integer operations, for example, when reason about non-linear integer algebraic (e.g., multiplication or division), the solver may not be able to get a result in a reasonable time. In contrast, reasoning about bounded integers is usually more efficient.

To bridge the performance gap between the two types of integers, Grisette allows to model the system with unbounded integers, and evaluate them with infinite precision during the symbolic evaluation, but when solving the queries, they are translated to bit vectors for better performance.

For example, the Grisette term 5 * "a" :: SymInteger should be translated to the following SMT with the unbounded reasoning configuration (the term is t1):

(declare-fun a () Int)           ; declare symbolic constant a
(define-fun c1 () Int 5)         ; define the concrete value 5
(define-fun t1 () Int (* c1 a))  ; define the term

While with reasoning precision 4, it would be translated to the following SMT (the term is t1):

; declare symbolic constant a, the type is a bit vector with bit width 4
(declare-fun a () (_ BitVec 4))
; define the concrete value 1, translated to the bit vector #x1
(define-fun c1 () (_ BitVec 4) #x5)
; define the term, using bit vector addition rather than integer addition
(define-fun t1 () (_ BitVec 4) (bvmul c1 a))

This bounded translation can usually be solved faster than the unbounded one, and should work well when no overflow is possible, in which case the performance can be improved with almost no cost.

We must note that the bounded translation is an approximation and is not sound. As the approximation happens only during the final translation, the symbolic evaluation may aggressively optimize the term based on the properties of mathematical integer arithmetic. This may cause the solver yield results that is incorrect under both unbounded or bounded semantics.

The following is an example that is correct under bounded semantics, while is incorrect under the unbounded semantics:

>>> :set -XTypeApplications -XOverloadedStrings -XDataKinds
>>> let a = "a" :: SymInteger
>>> solve (precise z3) $ a .> 7 .&& a .< 9
Right (Model {a -> 8 :: Integer})
>>> solve (approx (Proxy @4) z3) $ a .> 7 .&& a .< 9
Left Unsat

This may be avoided by setting an large enough reasoning precision to prevent overflows.

Incremental solver monad transformer with the SBV backend.

Incremental solver monad with the SBV backend.

Run the incremental solver monad transformer with a given configuration.

Run the incremental solver monad with a given configuration.

The handle type for the SBV solver.

See ConfigurableSolver and Solver for the interfaces.