-
- Downloads
StringZ3 revisiter: Now the conversion is made BEFORE the solver is invoked.
Added SubTreeOps.scala with common operations between type and Expressions.
Showing
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 1 addition, 1 deletionsrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/evaluators/StreamEvaluator.scala 1 addition, 1 deletionsrc/main/scala/leon/evaluators/StreamEvaluator.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 1 addition, 1 deletionsrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/DefOps.scala 1 addition, 0 deletionssrc/main/scala/leon/purescala/DefOps.scala
- src/main/scala/leon/purescala/ExprOps.scala 14 additions, 280 deletionssrc/main/scala/leon/purescala/ExprOps.scala
- src/main/scala/leon/purescala/Extractors.scala 5 additions, 4 deletionssrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/SubTreeOps.scala 286 additions, 0 deletionssrc/main/scala/leon/purescala/SubTreeOps.scala
- src/main/scala/leon/purescala/TypeOps.scala 7 additions, 7 deletionssrc/main/scala/leon/purescala/TypeOps.scala
- src/main/scala/leon/purescala/Types.scala 2 additions, 1 deletionsrc/main/scala/leon/purescala/Types.scala
- src/main/scala/leon/solvers/Model.scala 1 addition, 0 deletionssrc/main/scala/leon/solvers/Model.scala
- src/main/scala/leon/solvers/SolverFactory.scala 2 additions, 1 deletionsrc/main/scala/leon/solvers/SolverFactory.scala
- src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala 114 additions, 0 deletions...cala/leon/solvers/combinators/Z3StringCapableSolver.scala
- src/main/scala/leon/solvers/templates/TemplateGenerator.scala 1 addition, 1 deletion...main/scala/leon/solvers/templates/TemplateGenerator.scala
- src/main/scala/leon/solvers/templates/TemplateManager.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/templates/TemplateManager.scala
- src/main/scala/leon/solvers/z3/Z3StringConversion.scala 40 additions, 3 deletionssrc/main/scala/leon/solvers/z3/Z3StringConversion.scala
- src/main/scala/leon/utils/InliningPhase.scala 1 addition, 1 deletionsrc/main/scala/leon/utils/InliningPhase.scala
- src/main/scala/leon/xlang/ImperativeCodeElimination.scala 1 addition, 1 deletionsrc/main/scala/leon/xlang/ImperativeCodeElimination.scala
Loading
Please register or sign in to comment