Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Backend.SBV.Data.SMT.Lowering

Description

Documentation

lowerSinglePrim :: forall integerBitWidth a m. (HasCallStack, SBVFreshMonad m) => GrisetteSMTConfig integerBitWidth -> Term a -> m (SymBiMap, TermTy integerBitWidth a) Source #

lowerSinglePrimCached :: forall integerBitWidth a m. (HasCallStack, SBVFreshMonad m) => GrisetteSMTConfig integerBitWidth -> Term a -> SymBiMap -> m (SymBiMap, TermTy integerBitWidth a) Source #

parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model Source #

Instances details

Show SymBiMap Source #
Instance details Defined in Grisette.Backend.SBV.Data.SMT.SymBiMap Methods showsPrec :: Int -> SymBiMap -> ShowS # show :: SymBiMap -> String # showList :: [SymBiMap] -> ShowS #
MonadIO m => MonadicSolver (SBVIncrementalT n m) Source #
Instance details Defined in Grisette.Backend.SBV.Data.SMT.Solving Methods monadicSolverPush :: Int -> SBVIncrementalT n m () Source # monadicSolverPop :: Int -> SBVIncrementalT n m () Source # monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model) Source #