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

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 #

data SymBiMap Source #

Instances

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 #