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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Smt.Serialize

Contents

Description

This module contains the code for serializing Haskell values into SMTLIB2 format, that is, the instances for the SMTLIB2 typeclass. We split it into a separate module as it depends on Theories (see smt2App).

Documentation

Orphan instances

SMTLIB2 Int Source # 
Instance details

Methods

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

SMTLIB2 LocSymbol Source # 
Instance details

SMTLIB2 Symbol Source # 
Instance details

Methods

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

SMTLIB2 Expr Source # 
Instance details

Methods

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

SMTLIB2 Bop Source # 
Instance details

Methods

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

SMTLIB2 Brel Source # 
Instance details

Methods

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

SMTLIB2 Constant Source # 
Instance details

SMTLIB2 SymConst Source # 
Instance details

SMTLIB2 Command Source # 
Instance details

Methods

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

SMTLIB2 (Triggered Expr) Source # 
Instance details

SMTLIB2 (Symbol, Sort) Source # 
Instance details

Methods

smt2 :: SymEnv -> (Symbol, Sort) -> Builder Source #