Safe Haskell | None |
---|---|
Language | Haskell98 |
- smt2App :: Expr -> [Builder] -> Maybe Builder
- smt2Sort :: Sort -> Maybe Builder
- smt2Symbol :: Symbol -> Maybe Builder
- preamble :: Config -> SMTSolver -> [Text]
- sizeBv :: FTycon -> Maybe Int
- toInt :: Expr -> Sort -> Expr
- theorySymbols :: HashMap Symbol TheorySymbol
- theorySEnv :: SEnv Sort
- 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 :: Expr -> [a] -> Bool
- isConName :: Symbol -> FTycon -> Bool
- axiomLiterals :: [(Symbol, Sort)] -> [Expr]
Convert theory applications TODO: merge with smt2symbol
Convert theory sorts
Convert theory symbols
smt2Symbol :: Symbol -> Maybe Builder Source #
Exported API -------------------------------------------------------------
Preamble to initialize SMT
Bit Vector Operations
toInt :: Expr -> Sort -> Expr Source #
Converting Non-Int types to Int -------------------------------------------
Theory Symbols
theorySymbols :: HashMap Symbol TheorySymbol Source #
theorySymbols
contains the list of ALL SMT symbols with interpretations,
i.e. which are given via `define-fun` (as opposed to `declare-fun`)
theorySEnv :: SEnv Sort 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.