| 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 | None |
| Language | Haskell2010 |
Grisette.Internal.Backend.SymBiMap
Description
Synopsis
- data SymBiMap = SymBiMap {}
- emptySymBiMap :: SymBiMap
- sizeBiMap :: SymBiMap -> Int
- addBiMap :: forall (knd :: SymbolKind). HasCallStack => SomeTerm -> Dynamic -> String -> SomeTypedSymbol knd -> SymBiMap -> SymBiMap
- addBiMapIntermediate :: HasCallStack => SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
- findStringToSymbol :: forall (knd :: SymbolKind). IsSymbolKind knd => String -> SymBiMap -> Maybe (SomeTypedSymbol knd)
- lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe (QuantifiedStack -> Dynamic)
- attachNextQuantifiedSymbolInfo :: SymBiMap -> TypedConstantSymbol a -> (SymBiMap, TypedConstantSymbol a)
Documentation
A bidirectional map between symbolic Grisette terms and sbv terms.
Constructors
| SymBiMap | |
Fields | |
Instances
| Show SymBiMap Source # | |
| MonadIO m => MonadicSolver (SBVIncrementalT m) Source # | |
Defined in Grisette.Internal.Backend.Solving Methods 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 # | |
emptySymBiMap :: SymBiMap Source #
An empty bidirectional map.
addBiMap :: forall (knd :: SymbolKind). HasCallStack => SomeTerm -> Dynamic -> String -> SomeTypedSymbol knd -> SymBiMap -> SymBiMap Source #
Add a new entry to the bidirectional map.
addBiMapIntermediate :: HasCallStack => SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap Source #
Add a new entry to the bidirectional map for intermediate values.
findStringToSymbol :: forall (knd :: SymbolKind). IsSymbolKind knd => String -> SymBiMap -> Maybe (SomeTypedSymbol knd) Source #
Find a symbolic Grisette term from a string.
lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe (QuantifiedStack -> Dynamic) Source #
Look up an sbv value with a symbolic Grisette term in the bidirectional map.
attachNextQuantifiedSymbolInfo :: SymBiMap -> TypedConstantSymbol a -> (SymBiMap, TypedConstantSymbol a) Source #
Attach the next quantified symbol info to a symbol.