| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Smt.Theories
Contents
- smt2App :: SymEnv -> Expr -> [Builder] -> Maybe Builder
- sortSmtSort :: Bool -> SEnv a -> Sort -> SmtSort
- smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
- preamble :: Config -> SMTSolver -> [Text]
- sizeBv :: FTycon -> Maybe Int
- theorySymbols :: [DataDecl] -> SEnv 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
- isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int
- axiomLiterals :: [(Symbol, Sort)] -> [Expr]
- maxLamArg :: Int
Convert theory applications TODO: merge with smt2symbol
Convert theory sorts
sortSmtSort :: Bool -> SEnv a -> Sort -> SmtSort Source #
'smtSort True msg t' serializes a sort t using type variables,
'smtSort False msg t' serializes a sort t using Int instead of tyvars.
Convert theory symbols
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder Source #
Exported API --------------------------------------------------------------
Preamble to initialize SMT
Bit Vector Operations
Theory Symbols
theorySymbols :: [DataDecl] -> SEnv TheorySymbol Source #
Theory Symbols : uninterpSEnv should be disjoint from see interpSEnv
to avoid duplicate SMT definitions. uninterpSEnv is for uninterpreted
symbols, and interpSEnv is for interpreted symbols.
theorySymbols contains the list of ALL SMT symbols with interpretations,
i.e. which are given via `define-fun` (as opposed to `declare-fun`)