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
- smtExit :: Context -> IO ()
- 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 ()
- smtAssertAsync :: Context -> Expr -> IO ()
- smtCheckUnsatAsync :: Context -> IO ()
- readCheckUnsat :: Context -> IO Bool
- smtBracketAsyncAt :: SrcSpan -> Context -> String -> IO a -> IO a
- smtPushAsync :: Context -> IO ()
- smtPopAsync :: 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
Information about the external SMT process
Constructors
Ctx | |
makeContext :: Config -> FilePath -> IO Context Source #
SMT Context ---------------------------------------------------------
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 -----------------------------------------------------------
smtCheckUnsatAsync :: Context -> IO () Source #
smtPushAsync :: Context -> IO () Source #
smtPopAsync :: Context -> IO () Source #