liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Smt.Serialize

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 Command Source # 
Instance details

Methods

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

SMTLIB2 LocSymbol Source # 
Instance details

SMTLIB2 Symbol Source # 
Instance details

Methods

smt2 :: SymEnv -> Symbol -> 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 Expr Source # 
Instance details

Methods

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

SMTLIB2 SymConst Source # 
Instance details

SMTLIB2 Int Source # 
Instance details

Methods

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

SMTLIB2 (Triggered Expr) Source # 
Instance details

SMTLIB2 (Symbol, Sort) Source # 
Instance details

Methods

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