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

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

Documentation.SBV.Examples.Misc.ModelExtract

Description

Demonstrates use of programmatic model extraction. When programming with SBV, we typically use `sat`/`allSat` calls to compute models automatically. In more advanced uses, however, the user might want to use programmable extraction features to do fancier programming. We demonstrate some of these utilities here.

Synopsis

- outside :: [Integer] -> IO SatResult
- genVals :: IO [Integer]

# Documentation

outside :: [Integer] -> IO SatResult Source #

A simple function to generate a new integer value, that is not in the given set of values. We also require the value to be non-negative

genVals :: IO [Integer] Source #

We now use "outside" repeatedly to generate 10 integers, such that we not only disallow previously generated elements, but also any value that differs from previous solutions by less than 5. Here, we use the `getModelValue` function. We could have also extracted the dictionary via `getModelDictionary` and did fancier programming as well, as necessary. We have:

    >>> genVals
    [45,40,35,30,25,20,15,10,5,0]