Stability | experimental |
---|---|

Maintainer | erkokl@gmail.com |

Safe Haskell | None |

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

- sbvCurrentSolver :: SMTConfig
- prove :: Provable a => a -> IO ThmResult
- sat :: Provable a => a -> IO SatResult
- allSat :: Provable a => a -> IO AllSatResult
- isVacuous :: Provable a => a -> IO Bool
- isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- module Data.SBV

# Z3 specific interface

sbvCurrentSolver :: SMTConfigSource

Current solver instance, pointing to z3.

## Proving and checking satisfiability

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

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

:: Provable a | |

=> a | Property to check |

-> IO AllSatResult | List of all satisfying models |

Find all satisfying solutions, using the Z3 SMT solver

Check vacuity of the explicit constraints introduced by calls to the `constrain`

function, using the Z3 SMT solver

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

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

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

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

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