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

Grisette.Internal.Backend.SymBiMap

Description

 
Synopsis

Documentation

emptySymBiMap :: SymBiMap Source #

An empty bidirectional map.

sizeBiMap :: SymBiMap -> Int Source #

The size of the bidirectional map.

addBiMap :: 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 :: 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.

newtype QuantifiedSymbolInfo Source #

Information about a quantified symbol.

Instances

Instances details
Generic QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

Associated Types

type Rep QuantifiedSymbolInfo :: Type -> Type #

Show QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

NFData QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

Methods

rnf :: QuantifiedSymbolInfo -> () #

Eq QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

Ord QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

Hashable QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

Lift QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

type Rep QuantifiedSymbolInfo Source # 
Instance details

Defined in Grisette.Internal.Backend.SymBiMap

type Rep QuantifiedSymbolInfo = D1 ('MetaData "QuantifiedSymbolInfo" "Grisette.Internal.Backend.SymBiMap" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'True) (C1 ('MetaCons "QuantifiedSymbolInfo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

attachNextQuantifiedSymbolInfo :: SymBiMap -> TypedConstantSymbol a -> (SymBiMap, TypedConstantSymbol a) Source #

Attach the next quantified symbol info to a symbol.