Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Smt.Types

Contents

Serialized Representation
Commands
Responses
Typeclass for SMTLIB2 conversion
SMTLIB2 Process Context
SMT monad

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]
- | Comment Text
data Response
- = Ok
- | Sat
- | Unsat
- | Unknown
- | Values [(Symbol, Text)]
- | Error !Text
class SMTLIB2 a where
- smt2 :: a -> SymM Builder
runSmt2 :: SMTLIB2 a => a -> SymM Builder
data Context = Ctx {
- ctxSolver :: Solver
- ctxElabF :: ElabFlags
- ctxClose :: IO ()
- ctxLog :: !(Maybe Handle)
- ctxVerbose :: !Bool
- ctxSymEnv :: !SymEnv
- ctxIxs :: ![Int]
- ctxDefines :: DefinedFuns
- ctxLams :: !Bool
- config :: !Config
}
type SmtM = StateT Context IO
liftSym :: SymM a -> SmtM a
catchSMT :: Exception e => SmtM a -> (e -> IO a) -> SmtM a
bracketSMT :: SmtM a -> (a -> IO b) -> (a -> SmtM c) -> SmtM c

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]
Comment Text

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 :: Command -> SymM 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 :: a -> SymM Builder Source #

Instances

Instances details

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

runSmt2 :: SMTLIB2 a => a -> SymM 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.
ctxElabF :: ElabFlags
ctxClose :: IO ()
The close operation of the SMT solver backend.
ctxLog :: !(Maybe Handle)
ctxVerbose :: !Bool
ctxSymEnv :: !SymEnv
ctxIxs :: ![Int]
The stack of sort indexes which were fresh at the corresponding level of push/pop stack.
ctxDefines :: DefinedFuns
ctxLams :: !Bool
Flag which controls the generation SMT placeholders for lambda arguments See also maxLamArg
config :: !Config
Configuration options

SMT monad

type SmtM = StateT Context IO Source #

SMT monad, used to communicate with the SMT solver backend. The SymM monad embeds into it, as the symbolic state has to be threaded through for gnerating applys and other function sort symbols.

liftSym :: SymM a -> SmtM a Source #

catchSMT :: Exception e => SmtM a -> (e -> IO a) -> SmtM a Source #

bracketSMT :: SmtM a -> (a -> IO b) -> (a -> SmtM c) -> SmtM c Source #