Safe Haskell | None |
---|---|
Language | Haskell98 |
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 :: SMTSolver -> FilePath -> IO Context
- makeContextNoLog :: SMTSolver -> IO Context
- cleanupContext :: Context -> IO ExitCode
- command :: Context -> Command -> IO Response
- smtWrite :: Context -> Text -> IO ()
- smtDecl :: Context -> Symbol -> Sort -> IO ()
- smtAssert :: Context -> Pred -> IO ()
- smtCheckUnsat :: Context -> IO Bool
- smtBracket :: Context -> IO a -> IO a
- smtDistinct :: Context -> [Expr] -> IO ()
- theorySymbols :: HashMap Symbol TheorySymbol
Commands
Commands issued to SMT engine
Responses
Responses received from SMT engine
Typeclass for SMTLIB2 conversion
AST Conversion: Types that can be serialized ---------------------
Types that can be serialized
Creating and killing SMTLIB2 Process
Information about the external SMT process
makeContext :: SMTSolver -> FilePath -> IO Context Source
SMT Context ---------------------------------------------------------
makeContextNoLog :: SMTSolver -> IO Context Source
cleanupContext :: Context -> IO ExitCode Source
Execute Queries
command :: Context -> Command -> IO Response Source
SMT IO --------------------------------------------------------------
Query API
smtCheckUnsat :: Context -> IO Bool Source
smtBracket :: Context -> IO a -> IO a Source
smtDistinct :: Context -> [Expr] -> IO () Source