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

Stabilityexperimental
Maintainererkokl@gmail.com
Safe HaskellNone

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 :: SMTConfigSource

Current solver instance, pointing to cvc4.

Proving and checking satisfiability

proveSource

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

satSource

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

allSatSource

Arguments

:: Provable a 
=> a

Property to check

-> IO AllSatResult

List of all satisfying models

Find all satisfying solutions, using the CVC4 SMT solver

isVacuousSource

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

isTheoremSource

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

isSatisfiableSource

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

optimizeSource

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

minimizeSource

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

maximizeSource

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