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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Bridge.CVC4

Contents

Description

Interface to the CVC4 SMT solver. Import this module if you want to use the CVC4 SMT prover as your backend solver. Also see:

Synopsis

CVC4 specific interface

sbvCurrentSolver :: SMTConfig Source #

Current solver instance, pointing to cvc4.

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 the CVC4 SMT solver

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 the CVC4 SMT solver

safe Source #

Arguments

:: SExecutable a 
=> a

Program containing sAssert calls

-> IO [SafeResult] 

Check all sAssert calls are safe, using the CVC4 SMT solver

allSat Source #

Arguments

:: Provable a 
=> a

Property to check

-> IO AllSatResult

List of all satisfying models

Find all satisfying solutions, using the CVC4 SMT solver

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 the CVC4 SMT solver

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 the CVC4 SMT solver

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 the CVC4 SMT solver

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 the CVC4 SMT solver

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 the CVC4 SMT solver

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 the CVC4 SMT solver

Non-CVC4 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