Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Smt.Types

Contents

Serialized Representation
Commands
Responses
Typeclass for SMTLIB2 conversion
SMTLIB2 Process Context

Description

This module contains the types defining an SMTLIB2 interface.

Synopsis

data Command
- = Push
- | Pop
- | CheckSat
- | DeclData ![DataDecl]
- | Declare !Symbol [SmtSort] !SmtSort
- | Define !Sort
- | Assert !(Maybe Int) !Expr
- | AssertAx !(Triggered Expr)
- | Distinct [Expr]
- | GetValue [Symbol]
- | CMany [Command]
data Response
- = Ok
- | Sat
- | Unsat
- | Unknown
- | Values [(Symbol, Text)]
- | Error !Text
class SMTLIB2 a where
- smt2 :: SymEnv -> a -> Builder
runSmt2 :: SMTLIB2 a => SymEnv -> a -> Builder
data Context = Ctx {
- ctxPid :: !ProcessHandle
- ctxCin :: !Handle
- ctxCout :: !Handle
- ctxLog :: !(Maybe Handle)
- ctxVerbose :: !Bool
- ctxSymEnv :: !SymEnv
}

Serialized Representation

Commands

data Command Source #

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 #
Instance details Defined in Language.Fixpoint.Smt.Types Methods (==) :: Command -> Command -> Bool # (/=) :: Command -> Command -> Bool #
Show Command Source #
Instance details Defined in Language.Fixpoint.Smt.Types Methods showsPrec :: Int -> Command -> ShowS # show :: Command -> String # showList :: [Command] -> ShowS #
PPrint Command Source #
Instance details Defined in Language.Fixpoint.Smt.Types Methods pprintTidy :: Tidy -> Command -> Doc Source # pprintPrec :: Int -> Tidy -> Command -> Doc Source #
SMTLIB2 Command Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Command -> Builder Source #
Inputable Command Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Command Source # rr' :: String -> String -> Command Source #
Inputable [Command] Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> [Command] Source # rr' :: String -> String -> [Command] Source #

Responses

data Response Source #

Responses received from SMT engine

Constructors

Ok
Sat
Unsat
Unknown
Values [(Symbol, Text)]
Error !Text

Instances

Eq Response Source #
Instance details Defined in Language.Fixpoint.Smt.Types Methods (==) :: Response -> Response -> Bool # (/=) :: Response -> Response -> Bool #
Show Response Source #
Instance details Defined in Language.Fixpoint.Smt.Types Methods showsPrec :: Int -> Response -> ShowS # show :: Response -> String # showList :: [Response] -> ShowS #

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where Source #

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

Methods

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

Instances

SMTLIB2 Int Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Int -> Builder Source #
SMTLIB2 LocSymbol Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> LocSymbol -> Builder Source #
SMTLIB2 Symbol Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Symbol -> Builder Source #
SMTLIB2 Expr Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Expr -> Builder Source #
SMTLIB2 Bop Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Bop -> Builder Source #
SMTLIB2 Brel Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Brel -> Builder Source #
SMTLIB2 Constant Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Constant -> Builder Source #
SMTLIB2 SymConst Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> SymConst -> Builder Source #
SMTLIB2 SmtSort Source #
Instance details Defined in Language.Fixpoint.Smt.Theories Methods smt2 :: SymEnv -> SmtSort -> Builder Source #
SMTLIB2 Command Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Command -> Builder Source #
SMTLIB2 (Triggered Expr) Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Triggered Expr -> Builder Source #
SMTLIB2 (Symbol, Sort) Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> (Symbol, Sort) -> Builder Source #

runSmt2 :: SMTLIB2 a => SymEnv -> a -> Builder Source #

SMTLIB2 Process Context

data Context Source #

Information about the external SMT process

Constructors

Ctx
Fields ctxPid :: !ProcessHandle ctxCin :: !Handle ctxCout :: !Handle ctxLog :: !(Maybe Handle) ctxVerbose :: !Bool ctxSymEnv :: !SymEnv