| 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 -> DefinedFuns -> IO Context
- cleanupContext :: Context -> IO ()
- command :: HasCallStack => Command -> SmtM Response
- smtSetMbqi :: SmtM ()
- smtDecl :: Symbol -> Sort -> SmtM ()
- smtDecls :: [(Symbol, Sort)] -> SmtM ()
- smtDefineFunc :: Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> SmtM ()
- smtAssert :: Expr -> SmtM ()
- smtAssertDecl :: HasCallStack => Expr -> SmtM ()
- smtFuncDecl :: Text -> ([SmtSort], SmtSort) -> SmtM ()
- smtAssertAxiom :: Triggered Expr -> SmtM ()
- smtCheckUnsat :: HasCallStack => SmtM Bool
- smtBracket :: String -> SmtM a -> SmtM a
- smtBracketAt :: SrcSpan -> String -> SmtM a -> SmtM a
- smtDistinct :: [Expr] -> SmtM ()
- smtPush :: SmtM ()
- smtPop :: SmtM ()
- smtComment :: Text -> SmtM ()
- checkValid :: HasCallStack => Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
- checkValid' :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
- checkValidWithContext :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
- checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
- funcSortVars :: Bool -> SymEnv -> [(Text, ([SmtSort], SmtSort))]
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] | |
| Comment Text |
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
Constructors
| Ctx | |
Fields
| |
makeContext :: Config -> FilePath -> IO Context Source #
SMT Context ---------------------------------------------------------
makeContextWithSEnv :: Config -> FilePath -> SymEnv -> DefinedFuns -> IO Context Source #
cleanupContext :: Context -> IO () Source #
Close file handles and release the solver backend's resources.
Execute Queries
smtSetMbqi :: SmtM () Source #
Query API
smtAssertDecl :: HasCallStack => Expr -> SmtM () Source #
smtCheckUnsat :: HasCallStack => SmtM Bool Source #
smtBracket :: String -> SmtM a -> SmtM a Source #
smtBracket adds a new level to the apply stack and saves the last fresh index
on the index stack before the action, and reverts these changes after the action.
smtDistinct :: [Expr] -> SmtM () Source #
smtComment :: Text -> SmtM () Source #
Check Validity
checkValid :: HasCallStack => Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool Source #
type ClosedPred E = {v:Pred | subset (vars v) (keys E) } checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool
checkValid' :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool Source #
checkValidWithContext :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool Source #
checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool] Source #
If you already HAVE a context, where all the variables have declared types (e.g. if you want to make MANY repeated Queries)
funcSortVars :: Bool -> SymEnv -> [(Text, ([SmtSort], SmtSort))] Source #
See seApplsCur for explanation.