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, and safety
- 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:

Synopsis

ABC specific interface

sbvCurrentSolver :: SMTConfig Source

Current solver instance, pointing to abc.

Proving, checking satisfiability, and safety

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 to check the safety of
-> IO SafeResult	Response of the SMT solver, containing the unsafe model if found

Check safety, i.e., prove that all sAssert conditions are statically true in all paths

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