| Copyright | (c) Sirui Lu 2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | None |
| Language | Haskell2010 |
Grisette.Internal.Backend.QuantifiedStack
Description
Synopsis
- newtype QuantifiedSymbols = QuantifiedSymbols {}
- data QuantifiedStack
- addQuantified :: TypedConstantSymbol a -> Dynamic -> QuantifiedStack -> QuantifiedStack
- lookupQuantified :: forall (knd :: SymbolKind). (HasCallStack, IsSymbolKind knd) => SomeTypedSymbol knd -> QuantifiedStack -> Maybe Dynamic
- emptyQuantifiedSymbols :: QuantifiedSymbols
- addQuantifiedSymbol :: TypedConstantSymbol a -> QuantifiedSymbols -> QuantifiedSymbols
- isQuantifiedSymbol :: forall a (knd :: SymbolKind). (SupportedPrim a, IsSymbolKind knd) => TypedSymbol knd a -> QuantifiedSymbols -> Bool
- emptyQuantifiedStack :: QuantifiedStack
Documentation
newtype QuantifiedSymbols Source #
A set of quantified symbols.
Constructors
| QuantifiedSymbols | |
Fields | |
Instances
| Show QuantifiedSymbols Source # | |
Defined in Grisette.Internal.Backend.QuantifiedStack Methods showsPrec :: Int -> QuantifiedSymbols -> ShowS # show :: QuantifiedSymbols -> String # showList :: [QuantifiedSymbols] -> ShowS # | |
data QuantifiedStack Source #
A stack of quantified symbols.
Instances
| Eq QuantifiedStack Source # | |
Defined in Grisette.Internal.Backend.QuantifiedStack Methods (==) :: QuantifiedStack -> QuantifiedStack -> Bool # (/=) :: QuantifiedStack -> QuantifiedStack -> Bool # | |
| Hashable QuantifiedStack Source # | |
Defined in Grisette.Internal.Backend.QuantifiedStack | |
addQuantified :: TypedConstantSymbol a -> Dynamic -> QuantifiedStack -> QuantifiedStack Source #
Add a quantified symbol to the stack.
lookupQuantified :: forall (knd :: SymbolKind). (HasCallStack, IsSymbolKind knd) => SomeTypedSymbol knd -> QuantifiedStack -> Maybe Dynamic Source #
Look up a quantified symbol in the stack.
emptyQuantifiedSymbols :: QuantifiedSymbols Source #
An empty set of quantified symbols.
addQuantifiedSymbol :: TypedConstantSymbol a -> QuantifiedSymbols -> QuantifiedSymbols Source #
Add a quantified symbol to the set.
isQuantifiedSymbol :: forall a (knd :: SymbolKind). (SupportedPrim a, IsSymbolKind knd) => TypedSymbol knd a -> QuantifiedSymbols -> Bool Source #
Check if a symbol is quantified.
emptyQuantifiedStack :: QuantifiedStack Source #
An empty stack of quantified symbols.