Grisette.Internal.Backend.SymBiMap

Documentation

data SymBiMap

A bidirectional map between symbolic Grisette terms and sbv terms.

Constructors

SymBiMap

Fields

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

Instances

Show SymBiMap

Defined in Grisette.Internal.Backend.SymBiMap

Methods

showsPrec :: Int -> SymBiMap -> ShowS

show :: SymBiMap -> String

showList :: [SymBiMap] -> ShowS

MonadIO m => MonadicSolver (SBVIncrementalT n m)

Defined in Grisette.Internal.Backend.Solving

Methods

monadicSolverPush :: Int -> SBVIncrementalT n m ()

monadicSolverPop :: Int -> SBVIncrementalT n m ()

monadicSolverResetAssertions :: SBVIncrementalT n m ()

monadicSolverAssert :: SymBool -> SBVIncrementalT n m ()

monadicSolverCheckSat :: SBVIncrementalT n m (Either SolvingFailure Model)

emptySymBiMap :: SymBiMap

An empty bidirectional map.

sizeBiMap :: SymBiMap -> Int

The size of the bidirectional map.

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

Add a new entry to the bidirectional map.

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

Add a new entry to the bidirectional map for intermediate values.

findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol

Find a symbolic Grisette term from a string.

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

Look up an sbv value with a symbolic Grisette term in the bidirectional map.