1. Broader equivalence classes for lambdas
2. Evaluation of invariants caches result for valid forall-invariant interactions
Showing
- src/main/scala/leon/Reporter.scala 2 additions, 2 deletionssrc/main/scala/leon/Reporter.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 23 additions, 16 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/codegen/runtime/Monitor.scala 40 additions, 8 deletionssrc/main/scala/leon/codegen/runtime/Monitor.scala
- src/main/scala/leon/evaluators/Evaluator.scala 46 additions, 0 deletionssrc/main/scala/leon/evaluators/Evaluator.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 22 additions, 27 deletionssrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/evaluators/StreamEvaluator.scala 1 addition, 0 deletionssrc/main/scala/leon/evaluators/StreamEvaluator.scala
- src/main/scala/leon/purescala/ExprOps.scala 46 additions, 40 deletionssrc/main/scala/leon/purescala/ExprOps.scala
- src/main/scala/leon/purescala/Quantification.scala 9 additions, 2 deletionssrc/main/scala/leon/purescala/Quantification.scala
- src/main/scala/leon/solvers/unrolling/LambdaManager.scala 9 additions, 8 deletionssrc/main/scala/leon/solvers/unrolling/LambdaManager.scala
- src/main/scala/leon/solvers/unrolling/QuantificationManager.scala 9 additions, 18 deletions.../scala/leon/solvers/unrolling/QuantificationManager.scala
- src/main/scala/leon/solvers/unrolling/TemplateManager.scala 2 additions, 1 deletionsrc/main/scala/leon/solvers/unrolling/TemplateManager.scala
- src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala 7 additions, 1 deletionsrc/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 9 additions, 12 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 17 additions, 10 deletionssrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
- src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
Loading
Please register or sign in to comment