Grisette.Internal.Backend.SymBiMap

Documentation

data SymBiMap

A bidirectional map between symbolic Grisette terms and sbv terms.

Constructors

SymBiMap

Fields

• biMapToSBV :: HashMap SomeTerm (QuantifiedStack -> Dynamic)
• biMapFromSBV :: HashMap String SomeTypedAnySymbol
• quantifiedSymbolNum :: Int

Instances

MonadIO m => MonadicSolver (SBVIncrementalT m)

Defined in Grisette.Internal.Backend.Solving

Methods

monadicSolverPush :: Int -> SBVIncrementalT m ()

monadicSolverPop :: Int -> SBVIncrementalT m ()

monadicSolverResetAssertions :: SBVIncrementalT m ()

monadicSolverAssert :: SymBool -> SBVIncrementalT m ()

monadicSolverCheckSat :: SBVIncrementalT 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 knd -> SymBiMap -> SymBiMap

Add a new entry to the bidirectional map.

addBiMapIntermediate :: HasCallStack => SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap

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

findStringToSymbol :: IsSymbolKind knd => String -> SymBiMap -> Maybe (SomeTypedSymbol knd)

Find a symbolic Grisette term from a string.

lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe (QuantifiedStack -> Dynamic)

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

newtype QuantifiedSymbolInfo

Information about a quantified symbol.

Constructors

QuantifiedSymbolInfo Int

Instances

Generic QuantifiedSymbolInfo

Defined in Grisette.Internal.Backend.SymBiMap

Associated Types

type Rep QuantifiedSymbolInfo :: Type -> Type

Methods

from :: QuantifiedSymbolInfo -> Rep QuantifiedSymbolInfo x

to :: Rep QuantifiedSymbolInfo x -> QuantifiedSymbolInfo

Show QuantifiedSymbolInfo

Defined in Grisette.Internal.Backend.SymBiMap

Methods

showsPrec :: Int -> QuantifiedSymbolInfo -> ShowS

show :: QuantifiedSymbolInfo -> String

showList :: [QuantifiedSymbolInfo] -> ShowS

NFData QuantifiedSymbolInfo

Defined in Grisette.Internal.Backend.SymBiMap

Methods

rnf :: QuantifiedSymbolInfo -> ()

Eq QuantifiedSymbolInfo

Defined in Grisette.Internal.Backend.SymBiMap

Methods

(==) :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> Bool

(/=) :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> Bool

Ord QuantifiedSymbolInfo

Defined in Grisette.Internal.Backend.SymBiMap

Methods

compare :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> Ordering

(<) :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> Bool

(<=) :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> Bool

(>) :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> Bool

(>=) :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> Bool

max :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> QuantifiedSymbolInfo

min :: QuantifiedSymbolInfo -> QuantifiedSymbolInfo -> QuantifiedSymbolInfo

Hashable QuantifiedSymbolInfo

Defined in Grisette.Internal.Backend.SymBiMap

Methods

hashWithSalt :: Int -> QuantifiedSymbolInfo -> Int

hash :: QuantifiedSymbolInfo -> Int

Lift QuantifiedSymbolInfo

Defined in Grisette.Internal.Backend.SymBiMap

Methods

lift :: Quote m => QuantifiedSymbolInfo -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => QuantifiedSymbolInfo -> Code m QuantifiedSymbolInfo

type Rep QuantifiedSymbolInfo

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)

Attach the next quantified symbol info to a symbol.