Safe Haskell | None |
---|---|
Language | Haskell98 |
- 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`)