Grisette.Backend

SMT backend configuration

data GrisetteSMTConfig

Solver configuration for the Grisette SBV backend.

A Grisette solver configuration consists of a SBV solver configuration and some extra configurations.

You should start with the predefined configurations.

Constructors

GrisetteSMTConfig

Fields

• sbvConfig :: SMTConfig
• extraConfig :: ExtraConfig

Instances

ConfigurableSolver GrisetteSMTConfig SBVSolverHandle

Defined in Grisette.Internal.Backend.Solving

Methods

newSolver :: GrisetteSMTConfig -> IO SBVSolverHandle

MonadIO m => MonadicSolver (SBVIncrementalT m)

Defined in Grisette.Internal.Backend.Solving

Methods

monadicSolverPush :: Int -> SBVIncrementalT m ()

monadicSolverPop :: Int -> SBVIncrementalT m ()

monadicSolverResetAssertions :: SBVIncrementalT m ()

monadicSolverAssert :: SymBool -> SBVIncrementalT m ()

monadicSolverCheckSat :: SBVIncrementalT m (Either SolvingFailure Model)

boolector :: GrisetteSMTConfig

Solver configuration for Boolector. https://boolector.github.io/

bitwuzla :: GrisetteSMTConfig

Solver configuration for Bitwuzla. https://bitwuzla.github.io/

cvc4 :: GrisetteSMTConfig

Solver configuration for CVC4. https://cvc4.github.io/

cvc5 :: GrisetteSMTConfig

Solver configuration for CVC5. https://cvc5.github.io/

yices :: GrisetteSMTConfig

Solver configuration for Yices. https://yices.csl.sri.com/

dReal :: GrisetteSMTConfig

Solver configuration for DReal. http://dreal.github.io/

z3 :: GrisetteSMTConfig

Solver configuration for Z3. https://github.com/Z3Prover/z3/

mathSAT :: GrisetteSMTConfig

Solver configuration for MathSAT. http://mathsat.fbk.eu/

abc :: GrisetteSMTConfig

Solver configuration for ABC. http://www.eecs.berkeley.edu/~alanmi/abc/

Changing the extra configurations

newtype ExtraConfig

Grisette specific extra configurations for the SBV backend.

Constructors

ExtraConfig

Fields

• timeout :: Maybe Int

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

withTimeout :: Int -> GrisetteSMTConfig -> GrisetteSMTConfig

Set the timeout for the solver configuration.

The timeout is in microseconds (1e-6 seconds). The timeout is applied to each individual solver query.

clearTimeout :: GrisetteSMTConfig -> GrisetteSMTConfig

Clear the timeout for the solver configuration.

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.

• crackNumSurfaceVals :: [(String, Integer)]

  For crackNum: The surface representation of variables, if available

• 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 -> ()

data Logic

SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the user can override this choice using a call to setLogic This is especially handy if one is experimenting with custom logics that might be supported on new solvers. See https://smt-lib.org/logics.shtml for the official list.

Constructors

AUFLIA

Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.

AUFLIRA

Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value.

AUFNIRA

Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.

LRA

Linear formulas in linear real arithmetic.

QF_ABV

Quantifier-free formulas over the theory of bitvectors and bitvector arrays.

QF_AUFBV

Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.

QF_AUFLIA

Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols.

QF_AX

Quantifier-free formulas over the theory of arrays with extensionality.

QF_BV

Quantifier-free formulas over the theory of fixed-size bitvectors.

QF_IDL

Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.

QF_LIA

Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.

QF_LRA

Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.

QF_NIA

Quantifier-free integer arithmetic.

QF_NRA

Quantifier-free real arithmetic.

QF_RDL

Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.

QF_UF

Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.

QF_UFBV

Unquantified formulas over bitvectors with uninterpreted sort function and symbols.

QF_UFIDL

Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.

QF_UFLIA

Unquantified linear integer arithmetic with uninterpreted sort and function symbols.

QF_UFLRA

Unquantified linear real arithmetic with uninterpreted sort and function symbols.

QF_UFNRA

Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.

QF_UFNIRA

Unquantified non-linear real integer arithmetic with uninterpreted sort and function symbols.

UFLRA

Linear real arithmetic with uninterpreted sort and function symbols.

UFNIA

Non-linear integer arithmetic with uninterpreted sort and function symbols.

QF_FPBV

Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors.

QF_FP

Quantifier-free formulas over the theory of floating point numbers.

QF_FD

Quantifier-free finite domains.

QF_S

Quantifier-free formulas over the theory of strings.

Logic_ALL

The catch-all value.

Logic_NONE

Use this value when you want SBV to simply not set the logic.

CustomLogic String

In case you need a really custom string!

Instances

Show Logic

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> Logic -> ShowS

show :: Logic -> String

showList :: [Logic] -> ShowS

data SMTOption

Option values that can be set in the solver, following the SMTLib specification https://smt-lib.org/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.

Constructors

DiagnosticOutputChannel FilePath

ProduceAssertions Bool

ProduceAssignments Bool

ProduceProofs Bool

ProduceInterpolants Bool

ProduceUnsatAssumptions Bool

ProduceUnsatCores Bool

ProduceAbducts Bool

RandomSeed Integer

ReproducibleResourceLimit Integer

SMTVerbosity Integer

OptionKeyword String [String]

SetLogic Logic

SetInfo String [String]

Instances

Show SMTOption

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTOption -> ShowS

show :: SMTOption -> String

showList :: [SMTOption] -> ShowS

data Timing

Specify how to save timing information, if at all.

Constructors

NoTiming

PrintTiming

SaveTiming (IORef NominalDiffTime)

data SMTSolver

An SMT solver

Constructors

SMTSolver

Fields

• name :: Solver

  The solver in use

• executable :: String

  The path to its executable

• preprocess :: String -> String

  Each line sent to the solver will be passed through this function (typically id)

• options :: SMTConfig -> [String]

  Options to provide to the solver

• engine :: SMTEngine

  The solver engine, responsible for interpreting solver output

• capabilities :: SolverCapabilities

  Various capabilities of the solver