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

Copyright(c) Adam Foltzer
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Bridge.ABC

Contents

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

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