sbv-3.4: 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.Z3

Contents

Description

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

Synopsis

Z3 specific interface

sbvCurrentSolver :: SMTConfig Source

Current solver instance, pointing to z3.

Proving, checking satisfiability, and safety

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 Z3 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 Z3 SMT solver

safe Source

Arguments

:: SExecutable a 
=> a

Program to check the safety of

-> IO SafeResult

Response of the SMT solver, containing the unsafe model if found

Check safety, i.e., prove that all sAssert conditions are statically true in all paths

allSat Source

Arguments

:: Provable a 
=> a

Property to check

-> IO AllSatResult

List of all satisfying models

Find all satisfying solutions, using the Z3 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 Z3 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 Z3 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 Z3 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 Z3 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 Z3 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 Z3 SMT solver

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