Finished transitivity of propositions
Showing
- src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala 149 additions, 0 deletionssrc/main/scala/leon/codegen/runtime/SolverEntryPoint.scala
- src/main/scala/leon/frontends/scalac/ASTExtractors.scala 0 additions, 1 deletionsrc/main/scala/leon/frontends/scalac/ASTExtractors.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 3 additions, 0 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/Expressions.scala 4 additions, 2 deletionssrc/main/scala/leon/purescala/Expressions.scala
- src/main/scala/leon/purescala/FunctionClosure.scala 3 additions, 1 deletionsrc/main/scala/leon/purescala/FunctionClosure.scala
- src/main/scala/leon/solvers/templates/QuantificationManager.scala 229 additions, 126 deletions.../scala/leon/solvers/templates/QuantificationManager.scala
- src/main/scala/leon/solvers/templates/TemplateGenerator.scala 12 additions, 9 deletions...main/scala/leon/solvers/templates/TemplateGenerator.scala
- src/main/scala/leon/solvers/templates/Templates.scala 75 additions, 60 deletionssrc/main/scala/leon/solvers/templates/Templates.scala
- src/main/scala/leon/solvers/templates/UnrollingBank.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/templates/UnrollingBank.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala 2 additions, 0 deletionssrc/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
Loading
Please register or sign in to comment