| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Smt.Theories
Synopsis
- smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder
- sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort
- smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
- preamble :: Config -> SMTSolver -> [Builder]
- sizeBv :: FTycon -> Maybe Int
- theorySymbols :: [DataDecl] -> SEnv TheorySymbol
- dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
- setEmpty :: Symbol
- setEmp :: Symbol
- setCap :: Symbol
- setSub :: Symbol
- setAdd :: Symbol
- setMem :: Symbol
- setCom :: Symbol
- setCup :: Symbol
- setDif :: Symbol
- setSng :: Symbol
- mapSel :: Symbol
- mapCup :: Symbol
- mapSto :: Symbol
- mapDef :: 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 DataDecl -> Sort -> SmtSort Source #
The poly parameter is True when we are *declaring* sorts,
and so we need to leave the top type variables be; it is False when
we are declaring variables etc., and there, we serialize them
using Int (though really, there SHOULD BE NO floating tyVars...
'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`)
dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)] Source #
Constructors, Selectors and Tests from DataDeclarations.