sbv-5.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Adam Foltzer
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Bridge.ABC

Contents

- ABC specific interface
  - Proving, checking satisfiability
  - Optimization routines

Description

Interface to the ABC verification and synthesis tool. Import this module if you want to use ABC as your backend solver. Also see:

- Data.SBV.Bridge.Boolector
- Data.SBV.Bridge.CVC4
- Data.SBV.Bridge.MathSAT
- Data.SBV.Bridge.Yices
- Data.SBV.Bridge.Z3

Synopsis

- 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

prove Source

Arguments

:: Provable a |
=> a | Property to check
-> IO ThmResult | Response from the SMT solver, containing the counter-example if found

Prove theorems, using ABC

sat Source

Arguments

:: Provable a |
=> a | Property to check
-> IO SatResult | Response of the SMT Solver, containing the model if found

Find satisfying solutions, using ABC

safe Source

Arguments

:: SExecutable a |
=> a | Program containing sAssert calls
-> IO [SafeResult] |

Check all `sAssert` calls are safe, using ABC

allSat Source

Arguments

:: Provable a |
=> a | Property to check
-> IO AllSatResult | List of all satisfying models

Find all satisfying solutions, using ABC

isVacuous Source

Arguments

:: Provable a |
=> a | Property to check
-> IO Bool | True if the constraints are unsatisifiable

Check vacuity of the explicit constraints introduced by calls to the `constrain` function, using ABC

isTheorem Source

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

isSatisfiable Source

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

optimize Source

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

minimize Source

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

maximize Source

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