Philippe Suter
authored
This commit introduces `leon.purescala.DataGen`, an object that contains two static methods; `generate` and `findModels`. `generate` is a term generator based on composition of streams. It can generate hundreds of instances of recursive types in less than a tenth of a second. `findModels` leverages `generate` to perform (small-)model finding. Pass it an expression and an evaluator (preferably `CodeGenEvaluator`) and watch it find models to your formula. The commit also includes a small regression test suite. (Note that although we have currently no use for this, the `generate` function can in principle be used to generate arbitrary terms. E.g. you could pass variables as fixed generators for certain types.)
Name | Last commit | Last update |
---|---|---|
.. | ||
resources/regression/verification | ||
scala/leon/test |