liquid-fixpoint-0.7.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Smt.Theories

Contents

Synopsis

Convert theory applications TODO: merge with smt2symbol

Convert theory sorts

sortSmtSort :: Bool -> SEnv a -> Sort -> SmtSort Source #

'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 :: [DataDecl] -> SEnv TheorySymbol 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.

theorySymbols contains the list of ALL SMT symbols with interpretations, i.e. which are given via `define-fun` (as opposed to `declare-fun`)

Theories

Query Theories

Orphan instances