Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Smt.Types

Contents

Description

This module contains the types defining an SMTLIB2 interface.

Synopsis

Serialized Representation

Commands

Types ---------------------------------------------------------------------

Commands issued to SMT engine

Constructors

Push
Pop
CheckSat
DeclData !DataDecl
Declare !Symbol [SmtSort] !SmtSort
Define !Sort
Assert !(Maybe Int) !Expr
AssertAx !(Triggered Expr)
Distinct [Expr]
GetValue [Symbol]
CMany [Command]

Instances

Eq Command Source #
Methods (==) :: Command -> Command -> Bool # (/=) :: Command -> Command -> Bool #
Show Command Source #
Methods showsPrec :: Int -> Command -> ShowS # show :: Command -> String # showList :: [Command] -> ShowS #
PPrint Command Source #
Methods pprintTidy :: Tidy -> Command -> Doc Source # pprintPrec :: Int -> Tidy -> Command -> Doc Source #
Inputable Command Source #
Methods rr :: String -> Command Source # rr' :: String -> String -> Command Source #
Inputable [Command] Source #
Methods rr :: String -> [Command] Source # rr' :: String -> String -> [Command] Source #

Responses received from SMT engine

Constructors

Instances

Eq Response Source #
Methods (==) :: Response -> Response -> Bool # (/=) :: Response -> Response -> Bool #
Show Response Source #
Methods showsPrec :: Int -> Response -> ShowS # show :: Response -> String # showList :: [Response] -> ShowS #

class SMTLIB2 a where Source #

AST Conversion: Types that can be serialized ------------------------------

Minimal complete definition

Methods

Information about the external SMT process

Constructors

Ctx
Fields ctxPid :: !ProcessHandle ctxCin :: !Handle ctxCout :: !Handle ctxLog :: !(Maybe Handle) ctxVerbose :: !Bool ctxExt :: !Bool flag to enable function extentionality axioms ctxAeq :: !Bool flag to enable lambda a-equivalence axioms ctxBeq :: !Bool flag to enable lambda b-equivalence axioms ctxNorm :: !Bool flag to enable lambda normal form equivalence axioms ctxSymEnv :: !SymEnv