Documentation.SBV.Examples.Misc.ModelExtract

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

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]

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]