Copyright | (c) Sirui Lu 2021-2024 |
---|---|
License | BSD-3-Clause (see the LICENSE file) |
Maintainer | siruilu@cs.washington.edu |
Stability | Experimental |
Portability | GHC only |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- data GrisetteSMTConfig = GrisetteSMTConfig {}
- boolector :: GrisetteSMTConfig
- bitwuzla :: GrisetteSMTConfig
- cvc4 :: GrisetteSMTConfig
- cvc5 :: GrisetteSMTConfig
- yices :: GrisetteSMTConfig
- dReal :: GrisetteSMTConfig
- z3 :: GrisetteSMTConfig
- mathSAT :: GrisetteSMTConfig
- abc :: GrisetteSMTConfig
- newtype ExtraConfig = ExtraConfig {}
- withTimeout :: Int -> GrisetteSMTConfig -> GrisetteSMTConfig
- clearTimeout :: GrisetteSMTConfig -> GrisetteSMTConfig
- type SBVIncrementalT m = ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m))
- type SBVIncremental = SBVIncrementalT IO
- runSBVIncrementalT :: ExtractIO m => GrisetteSMTConfig -> SBVIncrementalT m a -> m a
- runSBVIncremental :: GrisetteSMTConfig -> SBVIncremental a -> IO a
- data SBVSolverHandle
- lowerSinglePrimCached :: forall t m. (HasCallStack, SBVFreshMonad m) => Term t -> SymBiMap -> m (SymBiMap, QuantifiedStack -> SBVType t, SBool)
- lowerSinglePrim :: forall a m. (HasCallStack, SBVFreshMonad m) => Term a -> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
- parseModel :: GrisetteSMTConfig -> SMTModel -> SymBiMap -> Model
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.
Instances
ConfigurableSolver GrisetteSMTConfig SBVSolverHandle Source # | |
Defined in Grisette.Internal.Backend.Solving | |
MonadIO m => MonadicSolver (SBVIncrementalT m) Source # | |
Defined in Grisette.Internal.Backend.Solving monadicSolverPush :: Int -> SBVIncrementalT m () Source # monadicSolverPop :: Int -> SBVIncrementalT m () Source # monadicSolverResetAssertions :: SBVIncrementalT m () Source # monadicSolverAssert :: SymBool -> SBVIncrementalT m () Source # monadicSolverCheckSat :: SBVIncrementalT m (Either SolvingFailure Model) Source # |
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/
z3 :: GrisetteSMTConfig Source #
Solver configuration for Z3. https://github.com/Z3Prover/z3/
mathSAT :: GrisetteSMTConfig Source #
Solver configuration for MathSAT. http://mathsat.fbk.eu/
abc :: GrisetteSMTConfig Source #
Solver configuration for ABC. http://www.eecs.berkeley.edu/~alanmi/abc/
Changing the extra configurations
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
data SBVSolverHandle Source #
The handle type for the SBV solver.
See ConfigurableSolver
and Solver
for the interfaces.
Instances
Solver SBVSolverHandle Source # | |
Defined in Grisette.Internal.Backend.Solving solverRunCommand :: (SBVSolverHandle -> IO (Either SolvingFailure a)) -> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a) Source # solverAssert :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure ()) Source # solverCheckSat :: SBVSolverHandle -> IO (Either SolvingFailure Model) Source # solverPush :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ()) Source # solverPop :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ()) Source # solverResetAssertions :: SBVSolverHandle -> IO (Either SolvingFailure ()) Source # solverTerminate :: SBVSolverHandle -> IO () Source # solverForceTerminate :: SBVSolverHandle -> IO () Source # | |
ConfigurableSolver GrisetteSMTConfig SBVSolverHandle Source # | |
Defined in Grisette.Internal.Backend.Solving |
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.