Generalized stopping conditions for symbolic evaluation - Githubissues

tweag / pirouette

Language-generic workbench for building static analysis

MIT License

47 stars 2 forks source link

Generalized stopping conditions for symbolic evaluation #92

Closed serras closed 2 years ago

serras commented 2 years ago

This is a quick generalization of the usage of "fuel" to stop symbolic evaluation. The idea is

Gather different statistics during evaluation (fuel used, # of constructors introduced, etcetera);
The "runner" function take a new StoppingCondition which is nothing more than a predicate SymEvalStatistics -> Bool.

So now our previous runners become:

Infinite runners simply use const False as StoppingCondition,
Runners with limited fuel are implemented as \st -> sestConsumedFuel st > availableFuel,
Runners limited by constructors can now be implemented as \st -> sestConstructors st > maxConstructors.