| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Smt.Interface
Contents
Description
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
- data Command
- data Response
- class SMTLIB2 a where
- data Context = Ctx {}
- makeContext :: Config -> FilePath -> IO Context
- makeContextNoLog :: Config -> IO Context
- makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
- cleanupContext :: Context -> IO ExitCode
- command :: Context -> Command -> IO Response
- smtWrite :: Context -> Raw -> IO ()
- 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 ()
- smtPop :: Context -> IO ()
- checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> 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]
Commands
Types ---------------------------------------------------------------------
Commands issued to SMT engine
Responses
Responses received from SMT engine
Typeclass for SMTLIB2 conversion
class SMTLIB2 a where Source #
AST Conversion: Types that can be serialized ------------------------------
Minimal complete definition
Creating and killing SMTLIB2 Process
Information about the external SMT process
Constructors
| Ctx | |
Fields
| |
makeContext :: Config -> FilePath -> IO Context Source #
SMT Context ---------------------------------------------------------
Execute Queries
command :: Context -> Command -> IO Response Source #
SMT IO --------------------------------------------------------------
Query API
smtPush :: Context -> IO () Source #
SMT Commands -----------------------------------------------------------
smtPop :: Context -> IO () Source #
SMT Commands -----------------------------------------------------------