Grisette.Internal.Backend.Solving

SBV 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 monadic solver interface

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

Incremental solver monad transformer with the SBV backend.

type SBVIncremental = SBVIncrementalT IO

Incremental solver monad with the SBV backend.

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

Run the incremental solver monad transformer with a given configuration.

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

Run the incremental solver monad with a given configuration.

SBV solver handle

data SBVSolverHandle

The handle type for the SBV solver.

See ConfigurableSolver and Solver for the interfaces.

Instances

Solver SBVSolverHandle

Defined in Grisette.Internal.Backend.Solving

Methods

solverRunCommand :: (SBVSolverHandle -> IO (Either SolvingFailure a)) -> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a)

solverAssert :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure ())

solverCheckSat :: SBVSolverHandle -> IO (Either SolvingFailure Model)

solverPush :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ())

solverPop :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ())

solverResetAssertions :: SBVSolverHandle -> IO (Either SolvingFailure ())

solverTerminate :: SBVSolverHandle -> IO ()

solverForceTerminate :: SBVSolverHandle -> IO ()

ConfigurableSolver GrisetteSMTConfig SBVSolverHandle

Defined in Grisette.Internal.Backend.Solving

Methods

newSolver :: GrisetteSMTConfig -> IO SBVSolverHandle

Internal lowering functions

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

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)

Lower a single primitive term to SBV.

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

Parse an SBV model to a Grisette model.