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
Instances
Show SymBiMap Source # | |
MonadIO m => MonadicSolver (SBVIncrementalT n m) Source # | |
Defined in Grisette.Internal.Backend.Solving monadicSolverPush :: Int -> SBVIncrementalT n m () Source # monadicSolverPop :: Int -> SBVIncrementalT n m () Source # monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model) Source # |
addBiMap :: HasCallStack => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap Source #
addBiMapIntermediate :: HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap Source #
findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol Source #
lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic Source #