Skip to content
Snippets Groups Projects
  • Philippe Suter's avatar
    d1592f32
    Generalization of Evaluators, and CodeGenEvaluator. · d1592f32
    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
    Generalization of Evaluators, and CodeGenEvaluator.
    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.