Skip to content
Snippets Groups Projects
user avatar
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.)
8dee703b
History