Safe Haskell	Safe-Inferred
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 Command Source #
Instance details Methods smt2 :: SymEnv -> Command -> Builder Source #
SMTLIB2 LocSymbol Source #
Instance details Methods smt2 :: SymEnv -> LocSymbol -> Builder Source #
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 Methods smt2 :: SymEnv -> Constant -> Builder Source #
SMTLIB2 Expr Source #
Instance details Methods smt2 :: SymEnv -> Expr -> Builder Source #
SMTLIB2 SymConst Source #
Instance details Methods smt2 :: SymEnv -> SymConst -> Builder Source #
SMTLIB2 Int Source #
Instance details Methods smt2 :: SymEnv -> Int -> Builder Source #
SMTLIB2 (Triggered Expr) Source #
Instance details Methods smt2 :: SymEnv -> Triggered Expr -> Builder Source #
SMTLIB2 (Symbol, Sort) Source #
Instance details Methods smt2 :: SymEnv -> (Symbol, Sort) -> Builder Source #