| 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 :: TheorySymbols a => a -> SEnv TheorySymbol
- dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
- setEmpty :: IsString a => a
- setEmp :: IsString a => a
- setSng :: IsString a => a
- setAdd :: IsString a => a
- setMem :: IsString a => a
- setCom :: IsString a => a
- setCap :: IsString a => a
- setCup :: IsString a => a
- setDif :: IsString a => a
- setSub :: IsString a => a
- mapDef :: IsString a => a
- mapSel :: IsString a => a
- mapSto :: IsString a => a
- bagEmpty :: IsString a => a
- bagSng :: IsString a => a
- bagCount :: IsString a => a
- bagSub :: IsString a => a
- bagCup :: IsString a => a
- bagMax :: IsString a => a
- bagMin :: IsString a => a
- arrConstM :: Symbol
- arrStoreM :: Symbol
- arrSelectM :: Symbol
- arrConstS :: Symbol
- arrStoreS :: Symbol
- arrSelectS :: Symbol
- arrMapNotS :: Symbol
- arrMapOrS :: Symbol
- arrMapAndS :: Symbol
- arrMapImpS :: Symbol
- arrConstB :: Symbol
- arrStoreB :: Symbol
- arrSelectB :: Symbol
- arrMapPlusB :: Symbol
- arrMapLeB :: Symbol
- arrMapGtB :: Symbol
- arrMapIteB :: 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 :: TheorySymbols a => a -> SEnv TheorySymbol Source #
dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)] Source #
Constructors, Selectors and Tests from DataDeclarations.
Theories
Z3 theory array encodings
arrSelectM :: Symbol Source #
arrSelectS :: Symbol Source #
arrMapNotS :: Symbol Source #
arrMapAndS :: Symbol Source #
arrMapImpS :: Symbol Source #
arrSelectB :: Symbol Source #
arrMapPlusB :: Symbol Source #
arrMapIteB :: Symbol Source #
Query Theories
Orphan instances
| SMTLIB2 SmtSort Source # | |
| TheorySymbols SMTSolver Source # | Theory Symbols : |
Methods | |
| TheorySymbols [Equation] Source # | |
Methods theorySymbols :: [Equation] -> SEnv TheorySymbol Source # | |
| TheorySymbols [DataDecl] Source # | |
Methods theorySymbols :: [DataDecl] -> SEnv TheorySymbol Source # | |