Fix withOracle and holes semantics, do not treat them as special trees
Showing
- Game.scala 233 additions, 0 deletionsGame.scala
- library/annotation/package.scala 1 addition, 1 deletionlibrary/annotation/package.scala
- library/lang/synthesis/package.scala 11 additions, 8 deletionslibrary/lang/synthesis/package.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 0 additions, 3 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/frontends/scalac/ASTExtractors.scala 12 additions, 2 deletionssrc/main/scala/leon/frontends/scalac/ASTExtractors.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 61 additions, 26 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/PrettyPrinter.scala 5 additions, 1 deletionsrc/main/scala/leon/purescala/PrettyPrinter.scala
- src/main/scala/leon/purescala/ScalaPrinter.scala 1 addition, 1 deletionsrc/main/scala/leon/purescala/ScalaPrinter.scala
- src/main/scala/leon/purescala/TreeOps.scala 1 addition, 33 deletionssrc/main/scala/leon/purescala/TreeOps.scala
- src/main/scala/leon/purescala/Trees.scala 7 additions, 3 deletionssrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 55 additions, 44 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/synthesis/ChooseInfo.scala 0 additions, 20 deletionssrc/main/scala/leon/synthesis/ChooseInfo.scala
- src/main/scala/leon/synthesis/ConvertWithOracles.scala 91 additions, 0 deletionssrc/main/scala/leon/synthesis/ConvertWithOracles.scala
- src/main/scala/leon/synthesis/CostModel.scala 1 addition, 5 deletionssrc/main/scala/leon/synthesis/CostModel.scala
- src/main/scala/leon/synthesis/Rules.scala 2 additions, 2 deletionssrc/main/scala/leon/synthesis/Rules.scala
- src/main/scala/leon/synthesis/Solution.scala 9 additions, 4 deletionssrc/main/scala/leon/synthesis/Solution.scala
- src/main/scala/leon/synthesis/SynthesisOptions.scala 4 additions, 1 deletionsrc/main/scala/leon/synthesis/SynthesisOptions.scala
- src/main/scala/leon/synthesis/SynthesisPhase.scala 5 additions, 1 deletionsrc/main/scala/leon/synthesis/SynthesisPhase.scala
- src/main/scala/leon/synthesis/rules/AngelicHoles.scala 0 additions, 50 deletionssrc/main/scala/leon/synthesis/rules/AngelicHoles.scala
- src/main/scala/leon/synthesis/rules/Cegis.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/rules/Cegis.scala
Loading
Please register or sign in to comment