Grisette.Backend.SBV

Grisette SBV backend configuration

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)

Grisette specific extra configurations for the SBV backend.

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

ConfigurableSolver (GrisetteSMTConfig n) SBVSolverHandle

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

Methods

newSolver :: GrisetteSMTConfig n -> IO SBVSolverHandle

MonadIO m => MonadicSolver (SBVIncrementalT n m)

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

Methods

monadicSolverPush :: Int -> SBVIncrementalT n m ()

monadicSolverPop :: Int -> SBVIncrementalT n m ()

monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model)

SBV backend solver configuration

data SMTConfig

Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc. which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}.)

Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after the decimal point. The default value is 16, but it can be set to any positive integer.

When printing, SBV will add the suffix ... at the end of a real-value, if the given bound is not sufficient to represent the real-value exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation of the real value is not finite, i.e., if it is not rational.

The printBase field can be used to print numbers in base 2, 10, or 16.

The crackNum field can be used to display numbers in detail, all its bits and how they are laid out in memory. Works with all bounded number types (i.e., SWord and SInt), but also with floats. It is particularly useful with floating-point numbers, as it shows you how they are laid out in memory following the IEEE754 rules.

Constructors

SMTConfig

Fields

• verbose :: Bool

  Debug mode

• timing :: Timing

  Print timing information on how long different phases took (construction, solving, etc.)

• printBase :: Int

  Print integral literals in this base (2, 10, and 16 are supported.)

• printRealPrec :: Int

  Print algebraic real values with this precision. (SReal, default: 16)

• crackNum :: Bool

  For each numeric value, show it in detail in the model with its bits spliced out. Good for floats.

• satCmd :: String

  Usually "(check-sat)". However, users might tweak it based on solver characteristics.

• allSatMaxModelCount :: Maybe Int

  In a allSat call, return at most this many models. If nothing, return all.

• allSatPrintAlong :: Bool

  In a allSat call, print models as they are found.

• allSatTrackUFs :: Bool

  In a allSat call, should we try to extract values of uninterpreted functions?

• isNonModelVar :: String -> Bool

  When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)

• validateModel :: Bool

  If set, SBV will attempt to validate the model it gets back from the solver.

• optimizeValidateConstraints :: Bool

  Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.

• transcript :: Maybe FilePath

  If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)

• smtLibVersion :: SMTLibVersion

  What version of SMT-lib we use for the tool

• dsatPrecision :: Maybe Double

  Delta-sat precision

• solver :: SMTSolver

  The actual SMT solver.

• extraArgs :: [String]

  Extra command line arguments to pass to the solver.

• roundingMode :: RoundingMode

  Rounding mode to use for floating-point conversions

• solverSetOptions :: [SMTOption]

  Options to set as we start the solver

• ignoreExitCode :: Bool

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

• redirectVerbose :: Maybe FilePath

  Redirect the verbose output to this file if given. If Nothing, stdout is implied.

Instances

Show SMTConfig

We show the name of the solver for the config. Arguably this is misleading, but better than nothing.

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> SMTConfig -> ShowS

show :: SMTConfig -> String

showList :: [SMTConfig] -> ShowS

NFData SMTConfig

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTConfig -> ()

boolector :: SMTConfig

Default configuration for the Boolector SMT solver

cvc4 :: SMTConfig

Default configuration for the CVC4 SMT Solver.

yices :: SMTConfig

Default configuration for the Yices SMT Solver.

dReal :: SMTConfig

Default configuration for the Yices SMT Solver.

z3 :: SMTConfig

Default configuration for the Z3 SMT solver

mathSAT :: SMTConfig

Default configuration for the MathSAT SMT solver

abc :: SMTConfig

Default configuration for the ABC synthesis and verification tool.

data Timing

Specify how to save timing information, if at all.

Constructors

NoTiming

PrintTiming

SaveTiming (IORef NominalDiffTime)