Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Data.SBV.Bridge.Z3

Contents

Z3 specific interface
- Proving, checking satisfiability, and safety
- Optimization routines
Non-Z3 specific SBV interface

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:

Data.SBV.Bridge.Boolector

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