Language.Fixpoint.Smt.Interface

This module contains an SMTLIB2 interface for 1. checking the validity, and, 2. computing satisfying assignments for formulas. By implementing a binary interface over the SMTLIB2 format defined at http://www.smt-lib.org/ http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf

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

Creating and killing SMTLIB2 Process

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

makeContext :: Config -> FilePath -> IO Context

SMT Context ---------------------------------------------------------

makeContextNoLog :: Config -> IO Context

makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context

cleanupContext :: Context -> IO ()

Close file handles and release the solver backend's resources.

Execute Queries

command :: Context -> Command -> IO Response

SMT IO --------------------------------------------------------------------

smtSetMbqi :: Context -> IO ()

Query API

smtDecl :: Context -> Symbol -> Sort -> IO ()

smtDecls :: Context -> [(Symbol, Sort)] -> IO ()

smtDefineFunc :: Context -> Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> IO ()

smtAssert :: Context -> Expr -> IO ()

smtFuncDecl :: Context -> Text -> ([SmtSort], SmtSort) -> IO ()

smtAssertAxiom :: Context -> Triggered Expr -> IO ()

smtCheckUnsat :: Context -> IO Bool

smtCheckSat :: Context -> Expr -> IO Bool

smtBracket :: Context -> String -> IO a -> IO a

smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a

smtDistinct :: Context -> [Expr] -> IO ()

smtPush :: Context -> IO ()

SMT Commands -----------------------------------------------------------

smtPop :: Context -> IO ()

SMT Commands -----------------------------------------------------------

Check Validity

checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool

type ClosedPred E = {v:Pred | subset (vars v) (keys E) } checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool

checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool

checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool

checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]

If you already HAVE a context, where all the variables have declared types (e.g. if you want to make MANY repeated Queries)