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

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

Methods

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

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

Show Command

Methods

showsPrec :: Int -> Command -> ShowS

show :: Command -> String

showList :: [Command] -> ShowS

PPrint Command

Methods

pprintTidy :: Tidy -> Command -> Doc

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

Inputable Command

Methods

rr :: String -> Command

rr' :: String -> String -> Command

Inputable [Command]

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

Eq Response

Methods

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

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

Show Response

Methods

showsPrec :: Int -> Response -> ShowS

show :: Response -> String

showList :: [Response] -> ShowS

Typeclass for SMTLIB2 conversion

class SMTLIB2 a where

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

Minimal complete definition

smt2

Methods

smt2 :: SymEnv -> a -> Builder

Creating and killing SMTLIB2 Process

data Context

Information about the external SMT process

Constructors

Ctx

Fields

• ctxPid :: !ProcessHandle
• ctxCin :: !Handle
• ctxCout :: !Handle
• ctxLog :: !(Maybe Handle)
• ctxVerbose :: !Bool
• ctxExt :: !Bool

  flag to enable function extentionality axioms

• ctxAeq :: !Bool

  flag to enable lambda a-equivalence axioms

• ctxBeq :: !Bool

  flag to enable lambda b-equivalence axioms

• ctxNorm :: !Bool

  flag to enable lambda normal form equivalence axioms

• ctxSymEnv :: !SymEnv

makeContext :: Config -> FilePath -> IO Context

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

makeContextNoLog :: Config -> IO Context

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

cleanupContext :: Context -> IO ExitCode

Execute Queries

command :: Context -> Command -> IO Response

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

smtWrite :: Context -> Raw -> IO ()

Query API

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

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

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

smtFuncDecl :: Context -> Symbol -> ([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)