Safe Haskell	Safe-Inferred
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
- | Exit
- | SetMbqi
- | CheckSat
- | DeclData ![DataDecl]
- | Declare Text [SmtSort] !SmtSort
- | Define !Sort
- | DefineFunc Symbol [(Symbol, SmtSort)] !SmtSort Expr
- | 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 {
- ctxSolver :: Solver
- ctxClose :: IO ()
- ctxLog :: !(Maybe Handle)
- ctxVerbose :: !Bool
- ctxSymEnv :: !SymEnv
}

Serialized Representation

Commands

data Command Source #

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

Commands issued to SMT engine

Constructors

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

Instances

Instances details

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

Instances details

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

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where Source #

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

Methods

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

Instances

Instances details

SMTLIB2 Command Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Command -> 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 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 Expr Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Expr -> 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 Int Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Int -> 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 #

Additional information around the SMT solver backend

Constructors

Ctx
Fields ctxSolver :: Solver The high-level interface for interacting with the SMT solver backend. ctxClose :: IO () The close operation of the SMT solver backend. ctxLog :: !(Maybe Handle) ctxVerbose :: !Bool ctxSymEnv :: !SymEnv