Grisette.Backend.SBV.Data.SMT.SymBiMap

Documentation

data SymBiMap

Constructors

SymBiMap

Fields

• biMapToSBV :: HashMap SomeTerm Dynamic
• biMapFromSBV :: HashMap String SomeTypedSymbol

Instances

Show SymBiMap

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)

Defined in Grisette.Backend.SBV.Data.SMT.Solving

Methods

monadicSolverPush :: Int -> SBVIncrementalT n m ()

monadicSolverPop :: Int -> SBVIncrementalT n m ()

monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model)

emptySymBiMap :: SymBiMap

sizeBiMap :: SymBiMap -> Int

addBiMap :: HasCallStack => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap

addBiMapIntermediate :: HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap

findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol

lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic