Language.Fixpoint.Smt.Theories

Contents

• Convert theory applications TODO: merge with smt2symbol
• Convert theory sorts
• Convert theory symbols
• Preamble to initialize SMT
• Bit Vector Operations
• Theories

Synopsis

• smt2App :: Expr -> [Text] -> Maybe Text
• smt2Sort :: Sort -> Maybe Text
• smt2Symbol :: Symbol -> Maybe Text
• preamble :: Bool -> SMTSolver -> [Text]
• isBv :: FTycon -> Bool
• sizeBv :: FTycon -> Maybe Int
• isTheorySymbol :: Symbol -> Bool
• theoryEnv :: HashMap Symbol Sort
• theorySymbols :: HashMap Symbol 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

Convert theory applications TODO: merge with smt2symbol

Convert theory sorts

Convert theory symbols

Preamble to initialize SMT

Bit Vector Operations

Theories