liquid-fixpoint-0.8.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

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

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 :: [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`)

dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)] Source #

Constructors, Selectors and Tests from DataDeclarations.

Theories

Query Theories

Orphan instances

SMTLIB2 SmtSort Source # 
Instance details

Methods

smt2 :: SymEnv -> SmtSort -> Builder Source #