diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 5792b973ce934f91cac24a32d5979ef623f9be94..24d0fd06e3b63a17ba67c3647bfecb4f443c1954 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 ae4cf910277552c3ce1be662b910294a113e00ed..6ccb05f24ec05abb2517a6c4cc824ece3ca97559 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 78b75cf4600f6906ebf03ff33333d7a8fc2c9a92..babf6d728b383740202d0802c449d1549509265d 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 b5a349bb189a4cd553defc51c374d73023db1498..904e6e3d3a0abdebf95e057ae57dcf745ea2e26c 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 0f023bfb9ba5ca01d1209d3d76fa5ba8a0822103..8a244a5e897636d1fed3fcd7b7cdc3d96bacb622 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 aad213668f27a941a58219c8bc638f487f24cd38..26a57c62c80be70213ca709c35ed69d4664c3530 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 10a74488f7490ee015fe2ded818fff3a8deb41f3..3409bde31e2f4ad65b8f500615f2b292e928ebc9 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 8877c17afee3b3d3a271a5a099d133263aa8dcea..c783bbb04287e6875cc28c4f396b034979d19571 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 330bd00fc392d9afef2c235484b35e7cc5ce3228..3c72656350b097c795c97d3d1a95af6d608a354a 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 7628c6acb62b451a5a749db9fa84c0ceacdd2b3a..c5f6c0f7eb22e4d283adb5548c641ed3b58e1858 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 0000000000000000000000000000000000000000..c71bfcf526ff0c7f0f0c82e8e7ac6732f66b4557
--- /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 0000000000000000000000000000000000000000..3b6fdf42fc82b4e939a5be8976582aeec98fc355
--- /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 20f41f6412721f236f03ee7b703187004c71b9c1..13d4a49484de741320c90acb8539010adf381cad 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 569dba2a4f131e395c9d86294f170ea1c19b4afc..0000000000000000000000000000000000000000
--- 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 98cf970756012ac4c7e6be4277d0ced361e46e1b..0000000000000000000000000000000000000000
--- 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}""")
- }
-}