sbv-6.1: 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, optimization

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

allSat Source #

Arguments

:: Provable a 
=> a

Property to check

-> IO AllSatResult

List of all satisfying models

Find all satisfying solutions, using ABC

safe Source #

Arguments

:: SExecutable a 
=> a

Program containing sAssert calls

-> IO [SafeResult] 

Check all sAssert calls are safe, using ABC

optimize Source #

Arguments

:: Provable a 
=> a

Program with objectives

-> IO OptimizeResult 

Optimize objectives, 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

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