Remove EmptySet, EmptyMap and SingletonMap
EmptySet, EmptyMap and SingletonMap are redundant, so they are removed. They are subsumed by FiniteSet and FiniteMap. This commit also deletes two testcases that were testing for equality between EmptySet and FiniteSet of 0 element. Obviously they no longer relevant. Additionnaly, this commit adds some new regression testcases for Maps and Sets.
Showing
- src/main/scala/leon/Evaluator.scala 7 additions, 31 deletionssrc/main/scala/leon/Evaluator.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 0 additions, 3 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/plugin/CodeExtraction.scala 11 additions, 17 deletionssrc/main/scala/leon/plugin/CodeExtraction.scala
- src/main/scala/leon/purescala/Extractors.scala 11 additions, 2 deletionssrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/PrettyPrinter.scala 10 additions, 5 deletionssrc/main/scala/leon/purescala/PrettyPrinter.scala
- src/main/scala/leon/purescala/ScalaPrinter.scala 9 additions, 4 deletionssrc/main/scala/leon/purescala/ScalaPrinter.scala
- src/main/scala/leon/purescala/TreeOps.scala 2 additions, 2 deletionssrc/main/scala/leon/purescala/TreeOps.scala
- src/main/scala/leon/purescala/Trees.scala 1 addition, 4 deletionssrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/solvers/RandomSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/RandomSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 9 additions, 24 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/test/resources/regression/verification/purescala/valid/MyMap.scala 16 additions, 0 deletions...urces/regression/verification/purescala/valid/MyMap.scala
- src/test/resources/regression/verification/purescala/valid/MySet.scala 16 additions, 0 deletions...urces/regression/verification/purescala/valid/MySet.scala
- src/test/scala/leon/test/codegen/CodeGenEvaluation.scala 0 additions, 1 deletionsrc/test/scala/leon/test/codegen/CodeGenEvaluation.scala
- src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala 0 additions, 51 deletionssrc/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
- src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala 0 additions, 70 deletions...st/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala
Loading
Please register or sign in to comment