Grisette.Backend.SBV.Data.SMT.Solving

Documentation

data ApproximationConfig (n :: Nat) where

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.

Constructors

NoApprox :: ApproximationConfig 0

Approx :: (KnownNat n, IsZero n ~ 'False, BVIsNonZero n) => p n -> ApproximationConfig n

data ExtraConfig (i :: Nat)

Constructors

ExtraConfig

Fields

• timeout :: Maybe Int

  Timeout in milliseconds for each solver call. CEGIS may call the solver multiple times and each call has its own timeout.

• integerApprox :: ApproximationConfig i

  Configures how to approximate unbounded integer values.

precise :: SMTConfig -> GrisetteSMTConfig 0

A precise reasoning configuration with the given SBV solver configuration.

approx :: forall p n. (KnownNat n, IsZero n ~ 'False, BVIsNonZero n) => p n -> SMTConfig -> GrisetteSMTConfig n

An approximate reasoning configuration with the given SBV solver configuration.

withTimeout :: Int -> GrisetteSMTConfig i -> GrisetteSMTConfig i

Set the timeout for the solver configuration.

clearTimeout :: GrisetteSMTConfig i -> GrisetteSMTConfig i

Clear the timeout for the solver configuration.

withApprox :: (KnownNat n, IsZero n ~ 'False, BVIsNonZero n) => p n -> GrisetteSMTConfig i -> GrisetteSMTConfig n

Set the reasoning precision for the solver configuration.

clearApprox :: GrisetteSMTConfig i -> GrisetteSMTConfig 0

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

data GrisetteSMTConfig (i :: Nat)

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.

Constructors

GrisetteSMTConfig

Fields

• sbvConfig :: SMTConfig
• extraConfig :: ExtraConfig i

Instances

CEGISSolver (GrisetteSMTConfig n) SolvingFailure

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

cegisMultiInputs :: (EvaluateSym inputs, ExtractSymbolics inputs) => GrisetteSMTConfig n -> [inputs] -> (inputs -> CEGISCondition) -> IO ([inputs], Either SolvingFailure Model)

Solver (GrisetteSMTConfig n) SolvingFailure

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

solve :: GrisetteSMTConfig n -> SymBool -> IO (Either SolvingFailure Model)

solveMulti :: GrisetteSMTConfig n -> Int -> SymBool -> IO ([Model], SolvingFailure)

solveAll :: GrisetteSMTConfig n -> SymBool -> IO [Model]

data SolvingFailure

Constructors

DSat (Maybe String)

Unsat

Unk

ResultNumLimitReached

SolvingError SBVException

Instances

Show SolvingFailure

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

showsPrec :: Int -> SolvingFailure -> ShowS

show :: SolvingFailure -> String

showList :: [SolvingFailure] -> ShowS

CEGISSolver (GrisetteSMTConfig n) SolvingFailure

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

cegisMultiInputs :: (EvaluateSym inputs, ExtractSymbolics inputs) => GrisetteSMTConfig n -> [inputs] -> (inputs -> CEGISCondition) -> IO ([inputs], Either SolvingFailure Model)

Solver (GrisetteSMTConfig n) SolvingFailure

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

solve :: GrisetteSMTConfig n -> SymBool -> IO (Either SolvingFailure Model)

solveMulti :: GrisetteSMTConfig n -> Int -> SymBool -> IO ([Model], SolvingFailure)

solveAll :: GrisetteSMTConfig n -> SymBool -> IO [Model]

type family TermTy bitWidth b where ...

Equations

TermTy _ Bool = SBool

TermTy n Integer = Aux (IsZero n) n

TermTy n (IntN x) = SBV (IntN x)

TermTy n (WordN x) = SBV (WordN x)

TermTy n (a =-> b) = TermTy n a -> TermTy n b

TermTy n (a --> b) = TermTy n a -> TermTy n b

TermTy _ v = v