From 4299991102e0a2b8e509e62b212d0d35b1f8068c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 18 Sep 2014 16:04:15 +0200
Subject: [PATCH] FiniteSets should hold Sets, otherwise {1,2} != {2,1}
---
src/main/scala/leon/codegen/CompilationUnit.scala | 2 +-
src/main/scala/leon/evaluators/RecursiveEvaluator.scala | 8 ++++----
src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 4 ++--
src/main/scala/leon/purescala/Extractors.scala | 6 +++---
src/main/scala/leon/purescala/PrettyPrinter.scala | 2 +-
src/main/scala/leon/purescala/ScalaPrinter.scala | 3 ++-
src/main/scala/leon/purescala/TreeOps.scala | 2 +-
src/main/scala/leon/purescala/Trees.scala | 4 ++--
src/main/scala/leon/purescala/TypeTreeOps.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala | 6 +++---
src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala | 2 +-
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
src/main/scala/leon/synthesis/rules/Tegis.scala | 2 +-
src/test/scala/leon/test/evaluators/EvaluatorsTests.scala | 6 +++---
14 files changed, 26 insertions(+), 25 deletions(-)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 3aa980ef8..6015fa8d2 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -204,7 +204,7 @@ class CompilationUnit(val ctx: LeonContext,
gv
case (set : runtime.Set, SetType(b)) =>
- FiniteSet(set.getElements().asScala.map(jvmToExpr(_, b)).toSeq).setType(SetType(b))
+ FiniteSet(set.getElements().asScala.map(jvmToExpr(_, b)).toSet).setType(SetType(b))
case (map : runtime.Map, MapType(from, to)) =>
val pairs = map.getElements().asScala.map { entry =>
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 18dbe6ced..cb3278c09 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -273,14 +273,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case SetUnion(s1,s2) =>
(e(s1), e(s2)) match {
- case (f@FiniteSet(els1),FiniteSet(els2)) => FiniteSet((els1 ++ els2).distinct).setType(f.getType)
+ case (f@FiniteSet(els1),FiniteSet(els2)) => FiniteSet(els1 ++ els2).setType(f.getType)
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case SetIntersection(s1,s2) =>
(e(s1), e(s2)) match {
case (f @ FiniteSet(els1), FiniteSet(els2)) => {
- val newElems = (els1.toSet intersect els2.toSet).toSeq
+ val newElems = (els1 intersect els2)
val baseType = f.getType.asInstanceOf[SetType].base
FiniteSet(newElems).setType(f.getType)
}
@@ -290,7 +290,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case SetDifference(s1,s2) =>
(e(s1), e(s2)) match {
case (f @ FiniteSet(els1),FiniteSet(els2)) => {
- val newElems = (els1.toSet -- els2.toSet).toSeq
+ val newElems = els1 -- els2
val baseType = f.getType.asInstanceOf[SetType].base
FiniteSet(newElems).setType(f.getType)
}
@@ -312,7 +312,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case _ => throw EvalError(typeErrorMsg(sr, SetType(Untyped)))
}
- case f @ FiniteSet(els) => FiniteSet(els.map(e(_)).distinct).setType(f.getType)
+ case f @ FiniteSet(els) => FiniteSet(els.map(e(_))).setType(f.getType)
case i @ IntLiteral(_) => i
case b @ BooleanLiteral(_) => b
case u @ UnitLiteral() => u
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index e2778a359..2398e51b9 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1148,7 +1148,7 @@ trait CodeExtraction extends ASTExtractors {
case ExFiniteSet(tt, args) =>
val underlying = extractType(tt)
- FiniteSet(args.map(extractTree(_))).setType(SetType(underlying))
+ FiniteSet(args.map(extractTree(_)).toSet).setType(SetType(underlying))
case ExFiniteMultiset(tt, args) =>
val underlying = extractType(tt)
@@ -1156,7 +1156,7 @@ trait CodeExtraction extends ASTExtractors {
case ExEmptySet(tt) =>
val underlying = extractType(tt)
- FiniteSet(Seq()).setType(SetType(underlying))
+ FiniteSet(Set()).setType(SetType(underlying))
case ExEmptyMultiset(tt) =>
val underlying = extractType(tt)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 11a2e7281..be2a14fa5 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -93,12 +93,12 @@ object Extractors {
case And(args) => Some((args, And.apply))
case Or(args) => Some((args, Or.apply))
case FiniteSet(args) =>
- Some((args,
+ Some((args.toSeq,
{ newargs =>
if (newargs.isEmpty) {
- FiniteSet(Seq()).setType(expr.getType)
+ FiniteSet(Set()).setType(expr.getType)
} else {
- FiniteSet(newargs)
+ FiniteSet(newargs.toSet)
}
}
))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 5d97ff989..aafaff753 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -262,7 +262,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case GreaterThan(l,r) => optP { p"$l > $r" }
case LessEquals(l,r) => optP { p"$l <= $r" }
case GreaterEquals(l,r) => optP { p"$l >= $r" }
- case FiniteSet(rs) => p"{$rs}"
+ case FiniteSet(rs) => p"{${rs.toSeq}}"
case FiniteMultiset(rs) => p"{|$rs|)"
case EmptyMultiset(_) => p"\u2205"
case Not(ElementOfSet(e,s)) => p"$e \u2209 $s"
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 8305781b9..f51674901 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -26,7 +26,8 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case Iff(l,r) => p"$l == $r"
case Implies(l,r) => pp(Or(Not(l), r))
case Choose(vars, pred) => p"choose((${typed(vars)}) => $pred)"
- case s @ FiniteSet(rs) => {
+ case s @ FiniteSet(rss) => {
+ val rs = rss.toSeq
s.getType match {
case SetType(ut) =>
p"Set[$ut]($rs)"
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index e9e2c66b1..67cec4c0e 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -780,7 +780,7 @@ object TreeOps {
def simplestValue(tpe: TypeTree) : Expr = tpe match {
case Int32Type => IntLiteral(0)
case BooleanType => BooleanLiteral(false)
- case SetType(baseType) => FiniteSet(Seq()).setType(tpe)
+ case SetType(baseType) => FiniteSet(Set()).setType(tpe)
case MapType(fromType, toType) => FiniteMap(Seq()).setType(tpe)
case TupleType(tpes) => Tuple(tpes.map(simplestValue))
case ArrayType(tpe) => ArrayFill(IntLiteral(0), simplestValue(tpe))
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 7f5d5f4c6..44b98012a 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -519,8 +519,8 @@ object Trees {
}
/* Set expressions */
- case class FiniteSet(elements: Seq[Expr]) extends Expr {
- val tpe = if (elements.isEmpty) None else leastUpperBound(elements.map(_.getType))
+ case class FiniteSet(elements: Set[Expr]) extends Expr {
+ val tpe = if (elements.isEmpty) None else leastUpperBound(elements.toSeq.map(_.getType))
tpe.foreach(t => setType(SetType(t)))
}
// TODO : Figure out what evaluation order is, for this.
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 0cb7e3c6e..469b7606b 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -255,7 +255,7 @@ object TypeTreeOps {
Error(desc).setType(tpeSub(e.getType)).copiedFrom(e)
case s @ FiniteSet(elements) if elements.isEmpty =>
- FiniteSet(Nil).setType(tpeSub(s.getType)).copiedFrom(s)
+ FiniteSet(Set()).setType(tpeSub(s.getType)).copiedFrom(s)
case v @ Variable(id) if idsMap contains id =>
Variable(idsMap(id)).copiedFrom(v)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index d26e4d47d..92907a2e7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -45,15 +45,15 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
GenericValue(tp, n.toInt)
case (QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset"), Seq()), _), SetType(base)) =>
- FiniteSet(Seq()).setType(tpe)
+ FiniteSet(Set()).setType(tpe)
case (FunctionApplication(SimpleSymbol(SSymbol("setenum")), elems), SetType(base)) =>
- FiniteSet(elems.map(fromSMT(_, base))).setType(tpe)
+ FiniteSet(elems.map(fromSMT(_, base)).toSet).setType(tpe)
case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
FiniteSet(elems.map(fromSMT(_, tpe) match {
case FiniteSet(elems) => elems
- }).flatten).setType(tpe)
+ }).flatten.toSet).setType(tpe)
case _ =>
super[SMTLIBTarget].fromSMT(s, tpe)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 4feb6a394..48d602402 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -234,7 +234,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case SetType(base) =>
assert(r.default == BooleanLiteral(false) && r.keyTpe == base)
- FiniteSet(r.elems.keySet.toSeq).setType(tpe)
+ FiniteSet(r.elems.keySet).setType(tpe)
case RawArrayType(from, to) =>
r
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 077602062..1529dc7f7 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -749,7 +749,7 @@ trait AbstractZ3Solver
case None => throw new CantTranslateException(t)
case Some(set) =>
val elems = set.map(e => rec(e))
- FiniteSet(elems.toSeq).setType(tpe)
+ FiniteSet(elems).setType(tpe)
}
case LeonType(UnitType) =>
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index f17f75c96..faaa084e5 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -71,7 +71,7 @@ case object TEGIS extends Rule("TEGIS") {
case st @ SetType(base) =>
List(
- Generator(List(base), { case elems => FiniteSet(elems).setType(st) }),
+ Generator(List(base), { case elems => FiniteSet(elems.toSet).setType(st) }),
Generator(List(st, st), { case Seq(a, b) => SetUnion(a, b) }),
Generator(List(st, st), { case Seq(a, b) => SetIntersection(a, b) }),
Generator(List(st, st), { case Seq(a, b) => SetDifference(a, b) })
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 84c546c05..678373a89 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -315,9 +315,9 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
val nil = mkCaseClass("Nil")
val cons12 = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
- val semp = FiniteSet(Seq.empty).setType(SetType(Int32Type))
- val s123 = FiniteSet(Seq(IL(1), IL(2), IL(3))).setType(SetType(Int32Type))
- val s246 = FiniteSet(Seq(IL(2), IL(4), IL(6))).setType(SetType(Int32Type))
+ val semp = FiniteSet(Set()).setType(SetType(Int32Type))
+ val s123 = FiniteSet(Set(IL(1), IL(2), IL(3))).setType(SetType(Int32Type))
+ val s246 = FiniteSet(Set(IL(2), IL(4), IL(6))).setType(SetType(Int32Type))
for(e <- evaluators) {
checkSetComp(e, mkCall("finite"), Set(1, 2, 3))
--
GitLab