Skip to content
Snippets Groups Projects
user avatar
Philippe Suter authored
Evaluators now have a common interface, and need to be instantiated
before they can be used. This makes them more like solvers, and allows
us to switch between them completely transparently.

Evaluators should support `eval` and `compile`. The default
implementation for `compile` returns a closure that invokes `eval` each
time.

`eval` returns one of three results:
  - EvaluationSuccessful: evaluation terminated with a value
  - EvaluationFailure: evaluation resulted in a runtime error
  - EvaluationError: evaluation resulted in an internal error

CodeGenEvaluator is a drop-in substitute for DefaultEvaluator. It works
by compiling Leon methods to Java bytecode which is loaded dynamically.
The `compile` method should be used as much as possible, as `eval` will
recompile the expression each time (the functions from the Leon program
are always compiled only once, though). CodeGenEvaluator intercepts most
runtime errors and rewrites them into `EvaluationFailure` results.

Use --codegen to use code generation as the evaluator of choice within
FairZ3Solver. (Has no effect if neither --feelinglucky nor --checkmodels
is used.)

Improvements of EvaluatorsTests testing suite, and verification
regression suite is now run twice (with different options). As a result,
the original tests for codegen are obsolete.
d1592f32
History
Name Last commit Last update