Language.Fixpoint.Smt.Types

This module contains the types defining an SMTLIB2 interface.

Serialized Representation

Commands

data Command

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

Show Command

Defined in Language.Fixpoint.Smt.Types

Methods

showsPrec :: Int -> Command -> ShowS

show :: Command -> String

showList :: [Command] -> ShowS

Eq Command

Defined in Language.Fixpoint.Smt.Types

Methods

(==) :: Command -> Command -> Bool

(/=) :: Command -> Command -> Bool

Inputable Command

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Command

rr' :: String -> String -> Command

SMTLIB2 Command

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Command -> Builder

PPrint Command

Defined in Language.Fixpoint.Smt.Types

Methods

pprintTidy :: Tidy -> Command -> Doc

pprintPrec :: Int -> Tidy -> Command -> Doc

Inputable [Command]

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> [Command]

rr' :: String -> String -> [Command]

Responses

data Response

Responses received from SMT engine

Constructors

Ok

Sat

Unsat

Unknown

Values [(Symbol, Text)]

Error !Text

Instances

Show Response

Defined in Language.Fixpoint.Smt.Types

Methods

showsPrec :: Int -> Response -> ShowS

show :: Response -> String

showList :: [Response] -> ShowS

Eq Response

Defined in Language.Fixpoint.Smt.Types

Methods

(==) :: Response -> Response -> Bool

(/=) :: Response -> Response -> Bool

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where

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

Methods

smt2 :: SymEnv -> a -> Builder

Instances

SMTLIB2 Command

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Command -> Builder

SMTLIB2 LocSymbol

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> LocSymbol -> Builder

SMTLIB2 Symbol

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Symbol -> Builder

SMTLIB2 Bop

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Bop -> Builder

SMTLIB2 Brel

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Brel -> Builder

SMTLIB2 Constant

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Constant -> Builder

SMTLIB2 Expr

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Expr -> Builder

SMTLIB2 SymConst

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> SymConst -> Builder

SMTLIB2 SmtSort

Defined in Language.Fixpoint.Smt.Theories

Methods

smt2 :: SymEnv -> SmtSort -> Builder

SMTLIB2 Int

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Int -> Builder

SMTLIB2 (Triggered Expr)

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Triggered Expr -> Builder

SMTLIB2 (Symbol, Sort)

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> (Symbol, Sort) -> Builder

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

SMTLIB2 Process Context

data Context

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