-
- Downloads
Generalization of Evaluators, and CodeGenEvaluator.
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.
Showing
- src/main/java/leon/codegen/runtime/CaseClass.java 3 additions, 1 deletionsrc/main/java/leon/codegen/runtime/CaseClass.java
- src/main/java/leon/codegen/runtime/Map.java 53 additions, 9 deletionssrc/main/java/leon/codegen/runtime/Map.java
- src/main/java/leon/codegen/runtime/Set.java 28 additions, 3 deletionssrc/main/java/leon/codegen/runtime/Set.java
- src/main/scala/leon/LeonOption.scala 6 additions, 1 deletionsrc/main/scala/leon/LeonOption.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 106 additions, 12 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/codegen/CompilationUnit.scala 40 additions, 8 deletionssrc/main/scala/leon/codegen/CompilationUnit.scala
- src/main/scala/leon/codegen/CompiledExpression.scala 13 additions, 8 deletionssrc/main/scala/leon/codegen/CompiledExpression.scala
- src/main/scala/leon/evaluators/CodeGenEvaluator.scala 51 additions, 0 deletionssrc/main/scala/leon/evaluators/CodeGenEvaluator.scala
- src/main/scala/leon/evaluators/DefaultEvaluator.scala 65 additions, 92 deletionssrc/main/scala/leon/evaluators/DefaultEvaluator.scala
- src/main/scala/leon/evaluators/Evaluator.scala 40 additions, 0 deletionssrc/main/scala/leon/evaluators/Evaluator.scala
- src/main/scala/leon/purescala/Definitions.scala 11 additions, 0 deletionssrc/main/scala/leon/purescala/Definitions.scala
- src/main/scala/leon/solvers/ParallelSolver.scala 0 additions, 2 deletionssrc/main/scala/leon/solvers/ParallelSolver.scala
- src/main/scala/leon/solvers/RandomSolver.scala 18 additions, 16 deletionssrc/main/scala/leon/solvers/RandomSolver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 55 additions, 36 deletionssrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
- src/main/scala/leon/synthesis/LinearEquations.scala 14 additions, 8 deletionssrc/main/scala/leon/synthesis/LinearEquations.scala
- src/test/resources/regression/codegen/Prog001.scala 0 additions, 18 deletionssrc/test/resources/regression/codegen/Prog001.scala
- src/test/resources/regression/codegen/Prog002.scala 0 additions, 14 deletionssrc/test/resources/regression/codegen/Prog002.scala
- src/test/resources/regression/codegen/Prog003.scala 0 additions, 14 deletionssrc/test/resources/regression/codegen/Prog003.scala
- src/test/resources/regression/codegen/Prog004.scala 0 additions, 17 deletionssrc/test/resources/regression/codegen/Prog004.scala
- src/test/resources/regression/codegen/README 0 additions, 2 deletionssrc/test/resources/regression/codegen/README
Loading
Please register or sign in to comment