From 65b1b6af9de0331d88a288fc5db703cdd32557c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 14 Dec 2012 20:53:37 +0100
Subject: [PATCH] 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.
---
src/main/scala/leon/Evaluator.scala | 38 ++--------
.../scala/leon/codegen/CodeGeneration.scala | 3 -
.../scala/leon/plugin/CodeExtraction.scala | 28 +++-----
.../scala/leon/purescala/Extractors.scala | 13 +++-
.../scala/leon/purescala/PrettyPrinter.scala | 15 ++--
.../scala/leon/purescala/ScalaPrinter.scala | 13 ++--
src/main/scala/leon/purescala/TreeOps.scala | 4 +-
src/main/scala/leon/purescala/Trees.scala | 5 +-
.../scala/leon/solvers/RandomSolver.scala | 2 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 33 +++------
.../verification/purescala/valid/MyMap.scala | 16 +++++
.../verification/purescala/valid/MySet.scala | 16 +++++
.../leon/test/codegen/CodeGenEvaluation.scala | 1 -
.../test/solvers/z3/BugWithEmptySet.scala | 51 --------------
.../solvers/z3/BugWithEmptySetNewAPI.scala | 70 -------------------
15 files changed, 93 insertions(+), 215 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/MyMap.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/MySet.scala
delete mode 100644 src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
delete mode 100644 src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 5792b973c..24d0fd06e 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -209,55 +209,38 @@ object Evaluator {
}
case SetUnion(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
- case (EmptySet(_), f2) => f2
- case (f1, EmptySet(_)) => f1
case (f@FiniteSet(els1),FiniteSet(els2)) => FiniteSet((els1 ++ els2).distinct).setType(f.getType)
case (le,re) => throw TypeErrorEx(TypeError(le, s1.getType))
}
case SetIntersection(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
- case (e @ EmptySet(_), _) => e
- case (_, e @ EmptySet(_)) => e
case (f@FiniteSet(els1),FiniteSet(els2)) => {
val newElems = (els1.toSet intersect els2.toSet).toSeq
val baseType = f.getType.asInstanceOf[SetType].base
- if(newElems.isEmpty) {
- EmptySet(baseType).setType(f.getType)
- } else {
- FiniteSet(newElems).setType(f.getType)
- }
+ FiniteSet(newElems).setType(f.getType)
}
case (le,re) => throw TypeErrorEx(TypeError(le, s1.getType))
}
case SetDifference(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
- case (e @ EmptySet(_), _) => e
- case (f , EmptySet(_)) => f
case (f@FiniteSet(els1),FiniteSet(els2)) => {
val newElems = (els1.toSet -- els2.toSet).toSeq
val baseType = f.getType.asInstanceOf[SetType].base
- if(newElems.isEmpty) {
- EmptySet(baseType).setType(f.getType)
- } else {
- FiniteSet(newElems).setType(f.getType)
- }
+ FiniteSet(newElems).setType(f.getType)
}
case (le,re) => throw TypeErrorEx(TypeError(le, s1.getType))
}
case ElementOfSet(el,s) => (rec(ctx,el), rec(ctx,s)) match {
- case (_, EmptySet(_)) => BooleanLiteral(false)
case (e, f @ FiniteSet(els)) => BooleanLiteral(els.contains(e))
case (l,r) => throw TypeErrorEx(TypeError(r, SetType(l.getType)))
}
case SetCardinality(s) => {
val sr = rec(ctx, s)
sr match {
- case EmptySet(_) => IntLiteral(0)
case FiniteSet(els) => IntLiteral(els.size)
case _ => throw TypeErrorEx(TypeError(sr, SetType(AnyType)))
}
}
case f @ FiniteSet(els) => FiniteSet(els.map(rec(ctx,_)).distinct).setType(f.getType)
- case e @ EmptySet(_) => e
case i @ IntLiteral(_) => i
case b @ BooleanLiteral(_) => b
case u @ UnitLiteral => u
@@ -292,31 +275,24 @@ object Evaluator {
FiniteArray(exprs.map(e => rec(ctx, e)))
}
- case f @ FiniteMap(ss) => FiniteMap(ss.map(rec(ctx,_)).distinct.asInstanceOf[Seq[SingletonMap]]).setType(f.getType)
- case e @ EmptyMap(_,_) => e
- case s @ SingletonMap(f,t) => SingletonMap(rec(ctx,f), rec(ctx,t)).setType(s.getType)
+ case f @ FiniteMap(ss) => FiniteMap(ss.map{ case (k, v) => (rec(ctx, k), rec(ctx, v)) }.distinct).setType(f.getType)
case g @ MapGet(m,k) => (rec(ctx,m), rec(ctx,k)) match {
- case (FiniteMap(ss), e) => ss.find(_.from == e) match {
- case Some(SingletonMap(k0,v0)) => v0
+ case (FiniteMap(ss), e) => ss.find(_._1 == e) match {
+ case Some((_, v0)) => v0
case None => throw RuntimeErrorEx("key not found: " + e)
}
- case (EmptyMap(ft,tt), e) => throw RuntimeErrorEx("key not found: " + e)
- // case (SingletonMap(f,t), e) => if (f == e) t else throw RuntimeErrorEx("key not found: " + e)
case (l,r) => throw TypeErrorEx(TypeError(l, MapType(r.getType, g.getType)))
}
case u @ MapUnion(m1,m2) => (rec(ctx,m1), rec(ctx,m2)) match {
- case (EmptyMap(_,_), r) => r
- case (l, EmptyMap(_,_)) => l
case (f1@FiniteMap(ss1), FiniteMap(ss2)) => {
- val filtered1 = ss1.filterNot(s1 => ss2.exists(s2 => s2.from == s1.from))
+ val filtered1 = ss1.filterNot(s1 => ss2.exists(s2 => s2._1 == s1._1))
val newSs = filtered1 ++ ss2
FiniteMap(newSs).setType(f1.getType)
}
case (l, r) => throw TypeErrorEx(TypeError(l, m1.getType))
}
case i @ MapIsDefinedAt(m,k) => (rec(ctx,m), rec(ctx,k)) match {
- case (EmptyMap(_,_),_) => BooleanLiteral(false)
- case (FiniteMap(ss), e) => BooleanLiteral(ss.exists(_.from == e))
+ case (FiniteMap(ss), e) => BooleanLiteral(ss.exists(_._1 == e))
case (l, r) => throw TypeErrorEx(TypeError(l, m.getType))
}
case Distinct(args) => {
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index ae4cf9102..6ccb05f24 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -153,9 +153,6 @@ object CodeGeneration {
ch << InvokeVirtual(TupleClass, "get", "(I)Ljava/lang/Object;")
mkUnbox(bs(i - 1), ch)
- case EmptySet(_) =>
- ch << DefaultNew(SetClass)
-
case FiniteSet(es) =>
ch << DefaultNew(SetClass)
for(e <- es) {
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 78b75cf46..babf6d728 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -754,7 +754,7 @@ trait CodeExtraction extends Extractors {
}
case ExEmptySet(tt) => {
val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptySet(underlying).setType(SetType(underlying))
+ FiniteSet(Seq()).setType(SetType(underlying))
}
case ExEmptyMultiset(tt) => {
val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
@@ -765,28 +765,23 @@ trait CodeExtraction extends Extractors {
val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
val tpe = MapType(fromUnderlying, toUnderlying)
- EmptyMap(fromUnderlying, toUnderlying).setType(tpe)
+ FiniteMap(Seq()).setType(tpe)
}
case ExLiteralMap(ft, tt, elems) => {
val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
val tpe = MapType(fromUnderlying, toUnderlying)
- if (elems.isEmpty) {
- EmptyMap(fromUnderlying, toUnderlying).setType(tpe)
- } else {
- val singletons = elems.collect { case ExTuple(tpes, trees) if (trees.size == 2) =>
- SingletonMap(rec(trees(0)), rec(trees(1))).setType(tpe)
- }
-
-
- if (singletons.size != elems.size) {
- unit.error(nextExpr.pos, "Some map elements could not be extracted as Tuple2")
- throw ImpureCodeEncounteredException(nextExpr)
- }
+ val singletons: Seq[(Expr, Expr)] = elems.collect { case ExTuple(tpes, trees) if (trees.size == 2) =>
+ (rec(trees(0)), rec(trees(1)))
+ }
- FiniteMap(singletons).setType(tpe)
+ if (singletons.size != elems.size) {
+ unit.error(nextExpr.pos, "Some map elements could not be extracted as Tuple2")
+ throw ImpureCodeEncounteredException(nextExpr)
}
+
+ FiniteMap(singletons).setType(tpe)
}
case ExSetMin(t) => {
@@ -890,8 +885,7 @@ trait CodeExtraction extends Extractors {
val rt = rec(t)
rm.getType match {
case MapType(ft, tt) => {
- val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
- MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
+ MapUnion(rm, FiniteMap(Seq((rf, rt))).setType(rm.getType)).setType(rm.getType)
}
case ArrayType(bt) => {
ArrayUpdated(rm, rf, rt).setType(rm.getType).setPosInfo(up.pos.line, up.pos.column)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index b5a349bb1..904e6e3d3 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -61,7 +61,6 @@ object Extractors {
case MultisetUnion(t1,t2) => Some((t1,t2,MultisetUnion))
case MultisetPlus(t1,t2) => Some((t1,t2,MultisetPlus))
case MultisetDifference(t1,t2) => Some((t1,t2,MultisetDifference))
- case SingletonMap(t1,t2) => Some((t1,t2,SingletonMap))
case mg@MapGet(t1,t2) => Some((t1,t2, (t1, t2) => MapGet(t1, t2).setPosInfo(mg)))
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
@@ -88,7 +87,17 @@ object Extractors {
case And(args) => Some((args, And.apply))
case Or(args) => Some((args, Or.apply))
case FiniteSet(args) => Some((args, FiniteSet))
- case FiniteMap(args) => Some((args, (as : Seq[Expr]) => FiniteMap(as.asInstanceOf[Seq[SingletonMap]])))
+ case FiniteMap(args) => {
+ val subArgs = args.flatMap{case (k, v) => Seq(k, v)}
+ val builder: (Seq[Expr]) => Expr = (as: Seq[Expr]) => {
+ val (keys, values, isKey) = as.foldLeft[(List[Expr], List[Expr], Boolean)]((Nil, Nil, true)){
+ case ((keys, values, isKey), rExpr) => if(isKey) (rExpr::keys, values, false) else (keys, rExpr::values, true)
+ }
+ assert(isKey)
+ FiniteMap(keys.zip(values))
+ }
+ Some((subArgs, builder))
+ }
case FiniteMultiset(args) => Some((args, FiniteMultiset))
case ArrayUpdated(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2))))
case FiniteArray(args) => Some((args, FiniteArray))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 0f023bfb9..8a244a5e8 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -142,9 +142,8 @@ object PrettyPrinter {
case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ", lvl) // \leq
case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ", lvl) // \geq
- case FiniteSet(rs) => ppNary(sb, rs, "{", ", ", "}", lvl)
+ case FiniteSet(rs) => if(rs.isEmpty) sb.append("\u2205") /* Ø */ else ppNary(sb, rs, "{", ", ", "}", lvl)
case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", lvl)
- case EmptySet(_) => sb.append("\u2205") // Ø
case EmptyMultiset(_) => sb.append("\u2205") // Ø
case Not(ElementOfSet(s,e)) => ppBinary(sb, s, e, " \u2209 ", lvl) // \notin
case ElementOfSet(s,e) => ppBinary(sb, s, e, " \u2208 ", lvl) // \in
@@ -163,9 +162,15 @@ object PrettyPrinter {
case MultisetCardinality(t) => ppUnary(sb, t, "|", "|", lvl)
case MultisetPlus(l,r) => ppBinary(sb, l, r, " \u228E ", lvl) // U+
case MultisetToSet(e) => pp(e, sb, lvl).append(".toSet")
- case EmptyMap(_,_) => sb.append("{}")
- case SingletonMap(f,t) => ppBinary(sb, f, t, " -> ", lvl)
- case FiniteMap(rs) => ppNary(sb, rs, "{", ", ", "}", lvl)
+ case FiniteMap(rs) => {
+ sb.append("{")
+ val sz = rs.size
+ var c = 0
+ rs.foreach{case (k, v) => {
+ pp(k, sb, lvl); sb.append(" -> "); pp(v, sb, lvl); c += 1 ; if(c < sz) sb.append(", ")
+ }}
+ sb.append("}")
+ }
case MapGet(m,k) => {
var nsb = sb
pp(m, nsb, lvl)
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index aad213668..26a57c62c 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -140,7 +140,6 @@ object ScalaPrinter {
case GreaterEquals(l,r) => ppBinary(sb, l, r, " >= ", lvl) // \geq
case FiniteSet(rs) => ppNary(sb, rs, "Set(", ", ", ")", lvl)
case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", lvl)
- case EmptySet(bt) => sb.append("Set()") // Ø
case EmptyMultiset(_) => sys.error("Not Valid Scala")
case ElementOfSet(s,e) => ppBinary(sb, s, e, " contains ", lvl)
//case ElementOfSet(s,e) => ppBinary(sb, s, e, " \u2208 ", lvl) // \in
@@ -163,9 +162,15 @@ object ScalaPrinter {
// case MultisetCardinality(t) => ppUnary(sb, t, "|", "|", lvl)
// case MultisetPlus(l,r) => ppBinary(sb, l, r, " \u228E ", lvl) // U+
// case MultisetToSet(e) => pp(e, sb, lvl).append(".toSet")
- case EmptyMap(_,_) => sb.append("Map()")
- case SingletonMap(f,t) => ppBinary(sb, f, t, " -> ", lvl)
- case FiniteMap(rs) => ppNary(sb, rs, "Map(", ", ", ")", lvl)
+ case FiniteMap(rs) => {
+ sb.append("{")
+ val sz = rs.size
+ var c = 0
+ rs.foreach{case (k, v) => {
+ pp(k, sb, lvl); sb.append(" -> "); pp(v, sb, lvl); c += 1 ; if(c < sz) sb.append(", ")
+ }}
+ sb.append("}")
+ }
case MapGet(m,k) => {
pp(m, sb, lvl)
ppNary(sb, Seq(k), "(", ",", ")", lvl)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 10a74488f..3409bde31 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -822,8 +822,8 @@ object TreeOps {
case CaseClassType(ccd) =>
val fields = ccd.fields
CaseClass(ccd, fields.map(f => simplestValue(f.getType)))
- case SetType(baseType) => EmptySet(baseType).setType(tpe)
- case MapType(fromType, toType) => EmptyMap(fromType, toType).setType(tpe)
+ case SetType(baseType) => FiniteSet(Seq()).setType(tpe)
+ case MapType(fromType, toType) => FiniteMap(Seq()).setType(tpe)
case _ => throw new Exception("I can't choose simplest value for type " + tpe)
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 8877c17af..c783bbb04 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -402,7 +402,6 @@ object Trees {
}
/* Set expressions */
- case class EmptySet(baseType: TypeTree) extends Expr with Terminal
case class FiniteSet(elements: Seq[Expr]) extends Expr
// TODO : Figure out what evaluation order is, for this.
// Perhaps then rewrite as "contains".
@@ -436,9 +435,7 @@ object Trees {
case class MultisetToSet(multiset: Expr) extends Expr
/* Map operations. */
- case class EmptyMap(fromType: TypeTree, toType: TypeTree) extends Expr with Terminal
- case class SingletonMap(from: Expr, to: Expr) extends Expr
- case class FiniteMap(singletons: Seq[SingletonMap]) extends Expr
+ case class FiniteMap(singletons: Seq[(Expr, Expr)]) extends Expr
case class MapGet(map: Expr, key: Expr) extends Expr with ScalacPositional
case class MapUnion(map1: Expr, map2: Expr) extends Expr
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index 330bd00fc..3c7265635 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -68,7 +68,7 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
CaseClass(cd, cd.fields.map(f => randomValue(f.getType, size / nbFields)))
}
case AnyType => randomValue(randomType(), size)
- case SetType(base) => EmptySet(base)
+ case SetType(base) => FiniteSet(Seq())
case MultisetType(base) => EmptyMultiset(base)
case Untyped => sys.error("I don't know what to do")
case BottomType => sys.error("I don't know what to do")
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 7628c6acb..c5f6c0f7e 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -442,7 +442,6 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
case f @ FunctionInvocation(fd, args) => {
z3.mkApp(functionDefToDecl(fd), args.map(rec(_)): _*)
}
- case e @ EmptySet(_) => z3.mkEmptySet(typeToSort(e.getType.asInstanceOf[SetType].base))
case SetEquals(s1, s2) => z3.mkEq(rec(s1), rec(s2))
case ElementOfSet(e, s) => z3.mkSetSubset(z3.mkSetAdd(z3.mkEmptySet(typeToSort(e.getType)), rec(e)), rec(s))
@@ -457,25 +456,12 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
}
case SetMin(s) => intSetMinFun(rec(s))
case SetMax(s) => intSetMaxFun(rec(s))
- case s @ SingletonMap(from,to) => s.getType match {
- case MapType(fromType, toType) =>
- val fromSort = typeToSort(fromType)
- val toSort = typeToSort(toType)
- val constArray = z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
- z3.mkStore(constArray, rec(from), mapRangeSomeConstructors(toType)(rec(to)))
- case errorType => scala.sys.error("Unexpected type for singleton map: " + (ex, errorType))
- }
- case e @ EmptyMap(fromType, toType) => {
- typeToSort(e.getType) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
- val fromSort = typeToSort(fromType)
- val toSort = typeToSort(toType)
- z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
- }
case f @ FiniteMap(elems) => f.getType match {
- case MapType(fromType, toType) =>
+ case tpe@MapType(fromType, toType) =>
+ typeToSort(tpe) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
val fromSort = typeToSort(fromType)
val toSort = typeToSort(toType)
- elems.foldLeft(z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())){ case (ast, SingletonMap(k,v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(toType)(rec(v))) }
+ elems.foldLeft(z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())){ case (ast, (k,v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(toType)(rec(v))) }
case errorType => scala.sys.error("Unexpected type for finite map: " + (ex, errorType))
}
case mg @ MapGet(m,k) => m.getType match {
@@ -488,9 +474,8 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
case MapType(ft, tt) => m2 match {
case FiniteMap(ss) =>
ss.foldLeft(rec(m1)){
- case (ast, SingletonMap(k, v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(tt)(rec(v)))
+ case (ast, (k, v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(tt)(rec(v)))
}
- case SingletonMap(k, v) => z3.mkStore(rec(m1), rec(k), mapRangeSomeConstructors(tt)(rec(v)))
case _ => scala.sys.error("map updates can only be applied with concrete map instances")
}
case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
@@ -555,17 +540,17 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
model.getArrayValue(t) match {
case None => throw new CantTranslateException(t)
case Some((map, elseValue)) =>
- val singletons = map.map(e => (e, z3.getASTKind(e._2))).collect {
- case ((index, value), Z3AppAST(someCons, arg :: Nil)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(rec(index, Some(kt)), rec(arg, Some(vt)))
- }
- (if (singletons.isEmpty) EmptyMap(kt, vt) else FiniteMap(singletons.toSeq)).setType(expType.get)
+ val singletons: Seq[(Expr, Expr)] = map.map(e => (e, z3.getASTKind(e._2))).collect {
+ case ((index, value), Z3AppAST(someCons, arg :: Nil)) if someCons == mapRangeSomeConstructors(vt) => (rec(index, Some(kt)), rec(arg, Some(vt)))
+ }.toSeq
+ FiniteMap(singletons).setType(expType.get)
}
case Some(SetType(dt)) =>
model.getSetValue(t) match {
case None => throw new CantTranslateException(t)
case Some(set) => {
val elems = set.map(e => rec(e, Some(dt)))
- (if (elems.isEmpty) EmptySet(dt) else FiniteSet(elems.toSeq)).setType(expType.get)
+ FiniteSet(elems.toSeq).setType(expType.get)
}
}
case Some(ArrayType(dt)) => {
diff --git a/src/test/resources/regression/verification/purescala/valid/MyMap.scala b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
new file mode 100644
index 000000000..c71bfcf52
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object MyMap {
+
+ def map1(): Int = {
+ val m = Map(1 -> 2, 2 -> 3, 3 -> 4)
+ m(2)
+ } ensuring(_ == 3)
+
+ def map2(): Boolean = {
+ val m1 = Map[Int, Int]()
+ val m2 = Map.empty[Int, Int]
+ m1 == m2
+ } holds
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MySet.scala b/src/test/resources/regression/verification/purescala/valid/MySet.scala
new file mode 100644
index 000000000..3b6fdf42f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MySet.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object MySet {
+
+ def set1(): Boolean = {
+ val s = Set(1, 2, 3, 4)
+ s.contains(3)
+ } holds
+
+ def set2(): Boolean = {
+ val s1 = Set[Int]()
+ val s2 = Set.empty[Int]
+ s1 == s2
+ } holds
+
+}
diff --git a/src/test/scala/leon/test/codegen/CodeGenEvaluation.scala b/src/test/scala/leon/test/codegen/CodeGenEvaluation.scala
index 20f41f641..13d4a4948 100644
--- a/src/test/scala/leon/test/codegen/CodeGenEvaluation.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenEvaluation.scala
@@ -164,7 +164,6 @@ object Sets {
val unit = out.result.get
def asIntSet(e : Expr) : Option[Set[Int]] = e match {
- case EmptySet(_) => Some(Set.empty)
case FiniteSet(es) =>
val ois = es.map(_ match {
case IntLiteral(v) => Some(v)
diff --git a/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala b/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
deleted file mode 100644
index 569dba2a4..000000000
--- a/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
+++ /dev/null
@@ -1,51 +0,0 @@
-package leon.test.solvers.z3
-
-import leon.LeonContext
-import leon.SilentReporter
-
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-
-import leon.solvers.Solver
-import leon.solvers.z3.UninterpretedZ3Solver
-
-import org.scalatest.FunSuite
-
-class BugWithEmptySet extends FunSuite {
- private val emptyProgram = Program(FreshIdentifier("empty"), ObjectDef(FreshIdentifier("empty"), Nil, Nil))
-
- test("No distinction between Set() and Set.empty") {
- val tInt = Int32Type
- val tIntSet = SetType(Int32Type)
-
- val e1 = EmptySet(tInt).setType(tIntSet)
- assert(e1.getType === tIntSet)
-
- val e2 = FiniteSet(Nil).setType(tIntSet)
- assert(e2.getType === tIntSet)
-
- val s0 = FiniteSet(Seq(IntLiteral(0))).setType(tIntSet)
-
- val f1 = Equals(e1, e2)
-
- val silentContext = LeonContext(reporter = new SilentReporter)
- val solver : Solver = new UninterpretedZ3Solver(silentContext)
- solver.setProgram(emptyProgram)
-
- assert(solver.solve(f1) === Some(true),
- "Z3 should prove the equivalence between Ø and {}.")
-
- val f2 = Equals(e1, SetDifference(e1, s0))
-
- assert(solver.solve(f2) === Some(true),
- """Z3 should prove Ø = Ø \ {0}""")
-
- val f3 = Equals(e2, SetDifference(e2, s0))
-
- assert(solver.solve(f3) === Some(true),
- """Z3 should prove {} = {} \ {0}""")
- }
-}
diff --git a/src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala b/src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala
deleted file mode 100644
index 98cf97075..000000000
--- a/src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala
+++ /dev/null
@@ -1,70 +0,0 @@
-package leon.test.solvers.z3
-
-import leon.LeonContext
-import leon.SilentReporter
-
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-
-import leon.solvers.Solver
-import leon.solvers.z3.{AbstractZ3Solver, UninterpretedZ3Solver}
-
-import org.scalatest.FunSuite
-
-class BugWithEmptySetNewAPI extends FunSuite {
- private val emptyProgram = Program(FreshIdentifier("empty"), ObjectDef(FreshIdentifier("empty"), Nil, Nil))
-
- test("No distinction between Set() and Set.empty") {
- val tInt = Int32Type
- val tIntSet = SetType(Int32Type)
-
- val e1 = EmptySet(tInt).setType(tIntSet)
- assert(e1.getType === tIntSet)
-
- val e2 = FiniteSet(Nil).setType(tIntSet)
- assert(e2.getType === tIntSet)
-
- val s0 = FiniteSet(Seq(IntLiteral(0))).setType(tIntSet)
-
- val f1 = Equals(e1, e2)
-
- val silentContext = LeonContext(reporter = new SilentReporter)
- val solver : AbstractZ3Solver = new UninterpretedZ3Solver(silentContext)
- solver.setProgram(emptyProgram)
- solver.restartZ3
-
-
- val subSolver = solver.getNewSolver
-
- subSolver.push()
- subSolver.assertCnstr(Not(f1))
-
-
- assert(subSolver.check === Some(false),
- "Z3 should prove the equivalence between Ø and {}.")
-
- subSolver.pop(1)
-
- val f2 = Equals(e1, SetDifference(e1, s0))
-
- subSolver.push()
- subSolver.assertCnstr(Not(f2))
-
- assert(subSolver.check === Some(false),
- """Z3 should prove Ø = Ø \ {0}""")
-
-
- subSolver.pop(1)
-
- val f3 = Equals(e2, SetDifference(e2, s0))
-
- subSolver.push()
- subSolver.assertCnstr(Not(f3))
-
- assert(subSolver.check === Some(false),
- """Z3 should prove {} = {} \ {0}""")
- }
-}
--
GitLab