Copyright | (c) Adam Foltzer |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Data.SBV.Bridge.ABC
Description
Interface to the ABC verification and synthesis tool. Import this module if you want to use ABC as your backend solver. Also see:
- sbvCurrentSolver :: SMTConfig
- prove :: Provable a => a -> IO ThmResult
- sat :: Provable a => a -> IO SatResult
- safe :: SExecutable a => a -> IO [SafeResult]
- allSat :: Provable a => a -> IO AllSatResult
- isVacuous :: Provable a => a -> IO Bool
- isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- module Data.SBV
ABC specific interface
sbvCurrentSolver :: SMTConfig Source #
Current solver instance, pointing to abc.
Proving, checking satisfiability
Arguments
:: Provable a | |
=> a | Property to check |
-> IO ThmResult | Response from the SMT solver, containing the counter-example if found |
Prove theorems, using ABC
Arguments
:: Provable a | |
=> a | Property to check |
-> IO SatResult | Response of the SMT Solver, containing the model if found |
Find satisfying solutions, using ABC
Arguments
:: SExecutable a | |
=> a | Program containing sAssert calls |
-> IO [SafeResult] |
Check all sAssert
calls are safe, using ABC
Arguments
:: Provable a | |
=> a | Property to check |
-> IO AllSatResult | List of all satisfying models |
Find all satisfying solutions, using ABC
Check vacuity of the explicit constraints introduced by calls to the constrain
function, using ABC
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 ABC
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 ABC
Optimization routines
Arguments
:: (SatModel a, SymWord a, Show a, SymWord c, Show c) | |
=> OptimizeOpts | Parameters to optimization (Iterative, Quantified, etc.) |
-> (SBV c -> SBV c -> SBool) | Betterness check: This is the comparison predicate for optimization |
-> ([SBV a] -> SBV c) | Cost function |
-> Int | Number of inputs |
-> ([SBV a] -> SBool) | Validity function |
-> IO (Maybe [a]) | Returns Nothing if there is no valid solution, otherwise an optimal solution |
Optimize cost functions, using ABC
Arguments
:: (SatModel a, SymWord a, Show a, SymWord c, Show c) | |
=> OptimizeOpts | Parameters to optimization (Iterative, Quantified, etc.) |
-> ([SBV a] -> SBV c) | Cost function to minimize |
-> Int | Number of inputs |
-> ([SBV a] -> SBool) | Validity function |
-> IO (Maybe [a]) | Returns Nothing if there is no valid solution, otherwise an optimal solution |
Minimize cost functions, using ABC
Arguments
:: (SatModel a, SymWord a, Show a, SymWord c, Show c) | |
=> OptimizeOpts | Parameters to optimization (Iterative, Quantified, etc.) |
-> ([SBV a] -> SBV c) | Cost function to maximize |
-> Int | Number of inputs |
-> ([SBV a] -> SBool) | Validity function |
-> IO (Maybe [a]) | Returns Nothing if there is no valid solution, otherwise an optimal solution |
Maximize cost functions, using ABC
module Data.SBV