| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Smt.Interface
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
Synopsis
- 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
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] |
Responses
Typeclass for SMTLIB2 conversion
class SMTLIB2 a where Source #
AST Conversion: Types that can be serialized ------------------------------
Instances
Creating and killing SMTLIB2 Process
Information about the external SMT process
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 -----------------------------------------------------------