| 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.
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]