| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Smt.Theories
Contents
- smt2App :: Expr -> [Text] -> Maybe Text
- smt2Sort :: Sort -> Maybe Text
- smt2Symbol :: Symbol -> Maybe Text
- preamble :: Bool -> SMTSolver -> [Text]
- isBv :: FTycon -> Bool
- sizeBv :: FTycon -> Maybe Int
- isTheorySymbol :: Symbol -> Bool
- theoryEnv :: HashMap Symbol Sort
- theorySymbols :: HashMap Symbol TheorySymbol
- setEmpty :: Symbol
- setEmp :: Symbol
- setCap :: Symbol
- setSub :: Symbol
- setAdd :: Symbol
- setMem :: Symbol
- setCom :: Symbol
- setCup :: Symbol
- setDif :: Symbol
- setSng :: Symbol
- mapSel :: Symbol
- mapSto :: Symbol
Convert theory applications TODO: merge with smt2symbol
Convert theory sorts
Convert theory symbols
smt2Symbol :: Symbol -> Maybe Text Source
Exported API -------------------------------------------------------------
Preamble to initialize SMT
Bit Vector Operations
isTheorySymbol :: Symbol -> Bool Source