grisette-0.9.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.Backend.Solving

Description

 
Synopsis

SBV backend configuration

data GrisetteSMTConfig Source #

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.

boolector :: GrisetteSMTConfig Source #

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

bitwuzla :: GrisetteSMTConfig Source #

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

cvc4 :: GrisetteSMTConfig Source #

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

cvc5 :: GrisetteSMTConfig Source #

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

yices :: GrisetteSMTConfig Source #

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

dReal :: GrisetteSMTConfig Source #

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

mathSAT :: GrisetteSMTConfig Source #

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

Changing the extra configurations

newtype ExtraConfig Source #

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 Source #

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 Source #

Clear the timeout for the solver configuration.

SBV monadic solver interface

type SBVIncrementalT m = ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) Source #

Incremental solver monad transformer with the SBV backend.

type SBVIncremental = SBVIncrementalT IO Source #

Incremental solver monad with the SBV backend.

runSBVIncrementalT :: ExtractIO m => GrisetteSMTConfig -> SBVIncrementalT m a -> m a Source #

Run the incremental solver monad transformer with a given configuration.

runSBVIncremental :: GrisetteSMTConfig -> SBVIncremental a -> IO a Source #

Run the incremental solver monad with a given configuration.

SBV solver handle

Internal lowering functions

lowerSinglePrimCached :: forall t m. (HasCallStack, SBVFreshMonad m) => Term t -> SymBiMap -> m (SymBiMap, QuantifiedStack -> SBVType t, SBool) Source #

Lower a single primitive term to SBV. With an explicitly provided SymBiMap cache.

lowerSinglePrim :: forall a m. (HasCallStack, SBVFreshMonad m) => Term a -> m (SymBiMap, QuantifiedStack -> SBVType a, SBool) Source #

Lower a single primitive term to SBV.

parseModel :: GrisetteSMTConfig -> SMTModel -> SymBiMap -> Model Source #

Parse an SBV model to a Grisette model.