| Safe Haskell | Safe-Inferred |
|---|---|
| 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 ()
- command :: Context -> Command -> IO Response
- smtSetMbqi :: Context -> IO ()
- 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 ()
- 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 | |
| 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] |
Responses
Typeclass for SMTLIB2 conversion
class SMTLIB2 a where Source #
AST Conversion: Types that can be serialized ------------------------------
Instances
Creating and killing SMTLIB2 Process
Additional information around the SMT solver backend
makeContext :: Config -> FilePath -> IO Context Source #
SMT Context ---------------------------------------------------------
cleanupContext :: Context -> IO () Source #
Close file handles and release the solver backend's resources.
Execute Queries
command :: Context -> Command -> IO Response Source #
SMT IO --------------------------------------------------------------------
smtSetMbqi :: Context -> IO () Source #
Query API
smtPush :: Context -> IO () Source #
SMT Commands -----------------------------------------------------------
smtPop :: Context -> IO () Source #
SMT Commands -----------------------------------------------------------