Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Smt.Serialize

Contents

Orphan instances

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

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

Orphan instances

SMTLIB2 LocSymbol Source #
Methods smt2 :: SymEnv -> LocSymbol -> Builder Source #
SMTLIB2 Symbol Source #
Methods smt2 :: SymEnv -> Symbol -> Builder Source #
SMTLIB2 Expr Source #
Methods smt2 :: SymEnv -> Expr -> Builder Source #
SMTLIB2 Bop Source #
Methods smt2 :: SymEnv -> Bop -> Builder Source #
SMTLIB2 Brel Source #
Methods smt2 :: SymEnv -> Brel -> Builder Source #
SMTLIB2 Constant Source #
Methods smt2 :: SymEnv -> Constant -> Builder Source #
SMTLIB2 SymConst Source #
Methods smt2 :: SymEnv -> SymConst -> Builder Source #
SMTLIB2 Command Source #
Methods smt2 :: SymEnv -> Command -> Builder Source #
SMTLIB2 (Triggered Expr) Source #
Methods smt2 :: SymEnv -> Triggered Expr -> Builder Source #
SMTLIB2 (Symbol, Sort) Source #
Methods smt2 :: SymEnv -> (Symbol, Sort) -> Builder Source #