| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Bridge.Boolector
Contents
Description
Interface to the Boolector SMT solver. Import this module if you want to use the Boolector SMT prover as your backend solver. Also see:
- sbvCurrentSolver :: SMTConfig
- prove :: Provable a => a -> IO ThmResult
- sat :: Provable a => a -> IO SatResult
- allSat :: Provable a => a -> IO AllSatResult
- safe :: SExecutable a => a -> IO [SafeResult]
- optimize :: Provable a => a -> IO OptimizeResult
- isVacuous :: Provable a => a -> IO Bool
- isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- module Data.SBV
Boolector specific interface
sbvCurrentSolver :: SMTConfig Source #
Current solver instance, pointing to Boolector.
Proving, checking satisfiability, optimization
Arguments
| :: Provable a | |
| => a | Property to check |
| -> IO ThmResult | Response from the SMT solver, containing the counter-example if found |
Prove theorems, using the Boolector SMT solver
Arguments
| :: Provable a | |
| => a | Property to check |
| -> IO SatResult | Response of the SMT Solver, containing the model if found |
Find satisfying solutions, using the Boolector SMT solver
Arguments
| :: Provable a | |
| => a | Property to check |
| -> IO AllSatResult | List of all satisfying models |
Find all satisfying solutions, using the Boolector SMT solver
Arguments
| :: SExecutable a | |
| => a | Program containing sAssert calls |
| -> IO [SafeResult] |
Check all sAssert calls are safe, using the Boolector SMT solver
Arguments
| :: Provable a | |
| => a | Program with objectives |
| -> IO OptimizeResult |
Optimize objectives, using Boolector
Check vacuity of the explicit constraints introduced by calls to the constrain function, using the Boolector SMT solver
Arguments
| :: Provable a | |
| => Maybe Int | Optional time-out, specify in seconds |
| -> a | Property to check |
| -> IO (Maybe Bool) | Returns Nothing if time-out expires |
Check if the statement is a theorem, with an optional time-out in seconds, using the Boolector SMT solver
Arguments
| :: Provable a | |
| => Maybe Int | Optional time-out, specify in seconds |
| -> a | Property to check |
| -> IO (Maybe Bool) | Returns Nothing if time-out expiers |
Check if the statement is satisfiable, with an optional time-out in seconds, using the Boolector SMT solver
Non-Boolector specific SBV interface
The remainder of the SBV library that is common to all back-end SMT solvers, directly coming from the Data.SBV module.
module Data.SBV