Demonstrates use of programmatic model extraction. When programming with
SBV, we typically use
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.
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
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
getModelDictionary and did fancier programming as well, as necessary. We have: