Data.SBV.Bridge.CVC4

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

• Data.SBV.Bridge.ABC
• Data.SBV.Bridge.Boolector
• Data.SBV.Bridge.MathSAT
• Data.SBV.Bridge.Yices
• Data.SBV.Bridge.Z3

CVC4 specific interface

sbvCurrentSolver :: SMTConfig

Current solver instance, pointing to cvc4.

Proving, checking satisfiability, optimization

prove

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

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

allSat

Arguments

:: Provable a

=> a

Property to check

-> IO AllSatResult

List of all satisfying models

Find all satisfying solutions, using the CVC4 SMT solver

safe

Arguments

:: SExecutable a

=> a

Program containing sAssert calls

-> IO [SafeResult]

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

optimize

Arguments

:: Provable a

=> a

Program with objectives

-> IO OptimizeResult

Optimize objectives, using CVC4

isVacuous

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

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

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

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