Language.Fixpoint.Smt.Theories

Convert theory applications TODO: merge with smt2symbol

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

Convert theory sorts

smt2Sort :: Sort -> Maybe Builder

Convert theory symbols

smt2Symbol :: Symbol -> Maybe Builder

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

Preamble to initialize SMT

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

Bit Vector Operations

sizeBv :: FTycon -> Maybe Int

toInt :: Expr -> Sort -> Expr

Converting Non-Int types to Int -------------------------------------------

Theory Symbols

theorySymbols :: HashMap Symbol TheorySymbol

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

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.

String

Theories

setEmpty :: Symbol

setEmp :: Symbol

setCap :: Symbol

setSub :: Symbol

setAdd :: Symbol

setMem :: Symbol

setCom :: Symbol

setCup :: Symbol

setDif :: Symbol

setSng :: Symbol

mapSel :: Symbol

mapSto :: Symbol

Query Theories

isSmt2App :: Expr -> [a] -> Bool

isConName :: Symbol -> FTycon -> Bool

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