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 |
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
Show SymBiMap Source # | |
MonadIO m => MonadicSolver (SBVIncrementalT n m) Source # | |
Defined in Grisette.Backend.SBV.Data.SMT.Solving monadicSolverPush :: Int -> SBVIncrementalT n m () Source # monadicSolverPop :: Int -> SBVIncrementalT n m () Source # monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model) Source # |