Skip to content
Snippets Groups Projects
  1. Sep 27, 2013
  2. Aug 15, 2013
  3. Jul 16, 2013
  4. Jul 11, 2013
    • Etienne Kneuss's avatar
      Fix Scalaz3 library · c33c5361
      Etienne Kneuss authored
      c33c5361
    • Etienne Kneuss's avatar
      Upgrade Leon to Scala 2.10.x · c521d3bd
      Etienne Kneuss authored
      - Refactor code extraction
        - Standardize extractors
        - Fix type identification by resolving type aliases
      
      - Redo reporter integration with Scalac
        - Fix relining to prevent bizarre compile-errors
      
      - Refactor Pretty-Printers
        - Extensible class interface
        - Not returning mutable string-buffers anymore
      
      - Fixes according to 2.10
          - 100% false warnings in Tests
          - imports for postfix-ops or implicits
      
      - Upgrade ScalaZ3 to 2.10
      
      - Upgrade Cafebabe to 2.10
      c521d3bd
  5. Jan 11, 2013
    • Philippe Suter's avatar
      Fixed ClassLoader issue and type errors in evaluation. · 198a5489
      Philippe Suter authored
      This fixes the classloader issue that we had, where, in codegen, a
      library class would be loaded twice and be incompatible with itself.
      
      It also fixes an oversight in evaluating expressions, where the returned
      ground term was sometimes untyped (typically: empty sets and the like).
      We now copy the type of the (unevaluated) expression in such situations.
      198a5489
  6. Dec 17, 2012
    • Philippe Suter's avatar
      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
  7. Dec 10, 2012
Loading