Language.Fixpoint.Smt.Serialize

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

smt2SortMono :: PPrint a => a -> SymEnv -> Sort -> Builder

Orphan instances

SMTLIB2 Int

Methods

smt2 :: SymEnv -> Int -> Builder

SMTLIB2 LocSymbol

Methods

smt2 :: SymEnv -> LocSymbol -> Builder

SMTLIB2 Symbol

Methods

smt2 :: SymEnv -> Symbol -> Builder

SMTLIB2 Expr

Methods

smt2 :: SymEnv -> Expr -> Builder

SMTLIB2 Bop

Methods

smt2 :: SymEnv -> Bop -> Builder

SMTLIB2 Brel

Methods

smt2 :: SymEnv -> Brel -> Builder

SMTLIB2 Constant

Methods

smt2 :: SymEnv -> Constant -> Builder

SMTLIB2 SymConst

Methods

smt2 :: SymEnv -> SymConst -> Builder

SMTLIB2 Command

Methods

smt2 :: SymEnv -> Command -> Builder

SMTLIB2 (Triggered Expr)

Methods

smt2 :: SymEnv -> Triggered Expr -> Builder

SMTLIB2 (Symbol, Sort)

Methods

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