-
- Downloads
(a) Renaming & documenting some benchmarks
(b) Added 3 strategies for Conqueue, two of which is verifiable. The best strategy still has one unverified (but simple) axiom that relies on the acyclicity of streams (c) Improved the model and fixed some bugs.
Showing
- Notes-on-laziness 140 additions, 0 deletionsNotes-on-laziness
- leon.out/Conqueue-edited-simplified.scala 0 additions, 520 deletionsleon.out/Conqueue-edited-simplified.scala
- leon.out/Conqueue-strategy2.scala 633 additions, 0 deletionsleon.out/Conqueue-strategy2.scala
- library/lazy/package.scala 28 additions, 2 deletionslibrary/lazy/package.scala
- src/main/scala/leon/invariant/structure/FunctionUtils.scala 3 additions, 0 deletionssrc/main/scala/leon/invariant/structure/FunctionUtils.scala
- src/main/scala/leon/invariant/util/CallGraph.scala 6 additions, 6 deletionssrc/main/scala/leon/invariant/util/CallGraph.scala
- src/main/scala/leon/laziness/LazinessEliminationPhase.scala 61 additions, 26 deletionssrc/main/scala/leon/laziness/LazinessEliminationPhase.scala
- src/main/scala/leon/laziness/LazinessUtil.scala 39 additions, 4 deletionssrc/main/scala/leon/laziness/LazinessUtil.scala
- src/main/scala/leon/laziness/LazyClosureConverter.scala 198 additions, 108 deletionssrc/main/scala/leon/laziness/LazyClosureConverter.scala
- src/main/scala/leon/laziness/LazyFunctionsManager.scala 117 additions, 0 deletionssrc/main/scala/leon/laziness/LazyFunctionsManager.scala
- src/main/scala/leon/laziness/LazyInstrumenter.scala 4 additions, 4 deletionssrc/main/scala/leon/laziness/LazyInstrumenter.scala
- src/main/scala/leon/laziness/RefDataTypeManager.scala 42 additions, 0 deletionssrc/main/scala/leon/laziness/RefDataTypeManager.scala
- src/main/scala/leon/laziness/TypeChecker.scala 18 additions, 4 deletionssrc/main/scala/leon/laziness/TypeChecker.scala
- src/main/scala/leon/laziness/TypeRectifier.scala 33 additions, 6 deletionssrc/main/scala/leon/laziness/TypeRectifier.scala
- src/main/scala/leon/solvers/combinators/UnrollingSolver.scala 31 additions, 27 deletions...main/scala/leon/solvers/combinators/UnrollingSolver.scala
- src/main/scala/leon/transformations/SerialInstrumentationPhase.scala 30 additions, 29 deletions...ala/leon/transformations/SerialInstrumentationPhase.scala
- testcases/lazy-datastructures/BottomUpMegeSort.scala 74 additions, 42 deletionstestcases/lazy-datastructures/BottomUpMegeSort.scala
- testcases/lazy-datastructures/Conqueue-strategy1-with-uniqueness.scala 493 additions, 0 deletions...y-datastructures/Conqueue-strategy1-with-uniqueness.scala
- testcases/lazy-datastructures/Conqueue-strategy2.scala 701 additions, 0 deletionstestcases/lazy-datastructures/Conqueue-strategy2.scala
- testcases/lazy-datastructures/Conqueue-strategy3.scala 698 additions, 0 deletionstestcases/lazy-datastructures/Conqueue-strategy3.scala
Loading
Please register or sign in to comment