Language.Fixpoint.Smt.Theories

Convert theory applications TODO: merge with smt2symbol

smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder

Convert theory sorts

sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort

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

Exported API --------------------------------------------------------------

Preamble to initialize SMT

preamble :: Config -> SMTSolver -> [Text]

Bit Vector Operations

sizeBv :: FTycon -> Maybe Int

Theory Symbols

theorySymbols :: [DataDecl] -> SEnv TheorySymbol

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)]

Constructors, Selectors and Tests from DataDeclarations.

Theories

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

Query Theories

isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int

axiomLiterals :: [(Symbol, Sort)] -> [Expr]

maxLamArg :: Int

Orphan instances

SMTLIB2 SmtSort

Methods

smt2 :: SymEnv -> SmtSort -> Builder