diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 1d5dee8b468aaed99dc6742683a28e987c0c5253..ad7ae73770ba92ccb9ce2a9662a759f713c6d43f 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -299,7 +299,7 @@ trait CodeGeneration {
mkUnbox(bs(i - 1), ch)
// Sets
- case FiniteSet(es) =>
+ case FiniteSet(es, _) =>
ch << DefaultNew(SetClass)
for(e <- es) {
ch << DUP
@@ -337,7 +337,7 @@ trait CodeGeneration {
ch << InvokeVirtual(SetClass, "minus", s"(L$SetClass;)L$SetClass;")
// Maps
- case FiniteMap(ss) =>
+ case FiniteMap(ss, _, _) =>
ch << DefaultNew(MapClass)
for((f,t) <- ss) {
ch << DUP
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 138cefc9cd5119df5f5855149428f7191c6a9960..e183533b5ece0fe30b49ba31fe18c045b0236801 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -154,14 +154,14 @@ class CompilationUnit(val ctx: LeonContext,
//case f @ FiniteArray(exprs) if f.getType == ArrayType(BooleanType) =>
// exprs.map(e => exprToJVM(e).asInstanceOf[java.lang.Boolean].booleanValue).toArray
- case s @ FiniteSet(els) =>
+ case s @ FiniteSet(els, _) =>
val s = new leon.codegen.runtime.Set()
for (e <- els) {
s.add(exprToJVM(e))
}
s
- case m @ FiniteMap(els) =>
+ case m @ FiniteMap(els, _, _) =>
val m = new leon.codegen.runtime.Map()
for ((k,v) <- els) {
m.add(exprToJVM(k), exprToJVM(v))
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 0a69169a83fe481fa93302d9ca2916812c0bc0f2..d5bf1facfabd69ae22c8b6d1fcc8f5853b0dba9b 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -128,7 +128,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>
val els = e(set) match {
- case FiniteSet(els) => els
+ case FiniteSet(els, _) => els
case _ => throw EvalError(typeErrorMsg(set, SetType(tp)))
}
val cons = program.library.Cons.get
@@ -211,8 +211,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val rv = e(re)
(lv,rv) match {
- case (FiniteSet(el1),FiniteSet(el2)) => BooleanLiteral(el1.toSet == el2.toSet)
- case (FiniteMap(el1),FiniteMap(el2)) => BooleanLiteral(el1.toSet == el2.toSet)
+ case (FiniteSet(el1, _),FiniteSet(el2, _)) => BooleanLiteral(el1.toSet == el2.toSet)
+ case (FiniteMap(el1, _, _),FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
case (BooleanLiteral(b1),BooleanLiteral(b2)) => BooleanLiteral(b1 == b2)
case _ => BooleanLiteral(lv == rv)
}
@@ -382,7 +382,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case SetUnion(s1,s2) =>
(e(s1), e(s2)) match {
- case (f@FiniteSet(els1),FiniteSet(els2)) =>
+ case (f@FiniteSet(els1, _),FiniteSet(els2, _)) =>
val SetType(tpe) = f.getType
finiteSet(els1 ++ els2, tpe)
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
@@ -390,7 +390,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case SetIntersection(s1,s2) =>
(e(s1), e(s2)) match {
- case (f @ FiniteSet(els1), FiniteSet(els2)) => {
+ case (f @ FiniteSet(els1, _), FiniteSet(els2, _)) => {
val newElems = els1 intersect els2
val SetType(tpe) = f.getType
finiteSet(newElems, tpe)
@@ -400,7 +400,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)) => {
+ case (f @ FiniteSet(els1, _),FiniteSet(els2, _)) => {
val SetType(tpe) = f.getType
val newElems = els1 -- els2
finiteSet(newElems, tpe)
@@ -409,23 +409,22 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
case ElementOfSet(el,s) => (e(el), e(s)) match {
- case (e, f @ FiniteSet(els)) => BooleanLiteral(els.contains(e))
+ case (e, f @ FiniteSet(els, _)) => BooleanLiteral(els.contains(e))
case (l,r) => throw EvalError(typeErrorMsg(r, SetType(l.getType)))
}
case SubsetOf(s1,s2) => (e(s1), e(s2)) match {
- case (f@FiniteSet(els1),FiniteSet(els2)) => BooleanLiteral(els1.toSet.subsetOf(els2.toSet))
+ case (f@FiniteSet(els1, _),FiniteSet(els2, _)) => BooleanLiteral(els1.toSet.subsetOf(els2.toSet))
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case SetCardinality(s) =>
val sr = e(s)
sr match {
- case FiniteSet(els) => IntLiteral(els.size)
+ case FiniteSet(els, _) => IntLiteral(els.size)
case _ => throw EvalError(typeErrorMsg(sr, SetType(Untyped)))
}
- case f @ FiniteSet(els) =>
- val SetType(tp) = f.getType
- finiteSet(els.map(e), tp)
+ case f @ FiniteSet(els, base) =>
+ finiteSet(els.map(e), base)
case i @ IntLiteral(_) => i
case i @ InfiniteIntegerLiteral(_) => i
case b @ BooleanLiteral(_) => b
@@ -465,18 +464,18 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
tp
)
- case f @ FiniteMap(ss) =>
- val MapType(kT, vT) = f.getType
+ case f @ FiniteMap(ss, kT, vT) =>
finiteMap(ss.map{ case (k, v) => (e(k), e(v)) }.distinct, kT, vT)
+
case g @ MapGet(m,k) => (e(m), e(k)) match {
- case (FiniteMap(ss), e) => ss.find(_._1 == e) match {
+ case (FiniteMap(ss, _, _), e) => ss.find(_._1 == e) match {
case Some((_, v0)) => v0
case None => throw RuntimeError("Key not found: " + e)
}
case (l,r) => throw EvalError(typeErrorMsg(l, MapType(r.getType, g.getType)))
}
case u @ MapUnion(m1,m2) => (e(m1), e(m2)) match {
- case (f1@FiniteMap(ss1), FiniteMap(ss2)) => {
+ case (f1@FiniteMap(ss1, _, _), FiniteMap(ss2, _, _)) => {
val filtered1 = ss1.filterNot(s1 => ss2.exists(s2 => s2._1 == s1._1))
val newSs = filtered1 ++ ss2
val MapType(kT, vT) = u.getType
@@ -485,7 +484,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (l, r) => throw EvalError(typeErrorMsg(l, m1.getType))
}
case i @ MapIsDefinedAt(m,k) => (e(m), e(k)) match {
- case (FiniteMap(ss), e) => BooleanLiteral(ss.exists(_._1 == e))
+ case (FiniteMap(ss, _, _), e) => BooleanLiteral(ss.exists(_._1 == e))
case (l, r) => throw EvalError(typeErrorMsg(l, m.getType))
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9e209b5d54f7ba0c02b8ee6c78b4757a9187b2f0..60e5f7a76fb187c990464d60b2e6ded2ecd2a7f2 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1707,7 +1707,7 @@ trait CodeExtraction extends ASTExtractors {
MapIsDefinedAt(a1, a2)
case (IsTyped(a1, mt: MapType), "updated", List(k, v)) =>
- MapUnion(a1, NonemptyMap(Seq((k, v))))
+ MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to))
case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType))) if mt1 == mt2 =>
MapUnion(a1, a2)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 0bc69cb3b74c4018dbf63f0a055697a2f1d8bf74..2c15bdaf386c427365faac434fe64aacd5c6c949 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -188,8 +188,7 @@ object Constructors {
}
def finiteSet(els: Set[Expr], tpe: TypeTree) = {
- if (els.isEmpty) EmptySet(tpe)
- else NonemptySet(els)
+ FiniteSet(els, tpe)
}
def finiteMultiset(els: Seq[Expr], tpe: TypeTree) = {
@@ -198,8 +197,7 @@ object Constructors {
}
def finiteMap(els: Seq[(Expr, Expr)], keyType: TypeTree, valueType: TypeTree) = {
- if (els.isEmpty) EmptyMap(keyType, valueType)
- else NonemptyMap(els.distinct)
+ FiniteMap(els, keyType, valueType)
}
def finiteArray(els: Seq[Expr]): Expr = {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 0c158ec3225c6b136357daff92667dddfbce3e86..8943c6b164f079dba6d5d67da02f00d87a17c9fe 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -967,8 +967,8 @@ object ExprOps {
case CharType => CharLiteral('a')
case BooleanType => BooleanLiteral(false)
case UnitType => UnitLiteral()
- case SetType(baseType) => EmptySet(tpe)
- case MapType(fromType, toType) => EmptyMap(fromType, toType)
+ case SetType(baseType) => FiniteSet(Set(), tpe)
+ case MapType(fromType, toType) => FiniteMap(Nil, fromType, toType)
case TupleType(tpes) => Tuple(tpes.map(simplestValue))
case ArrayType(tpe) => EmptyArray(tpe)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 5aecb99741b38304661ebb30982e2f0f9e058b06..2a75af65cfecee84e2c4f24b061af22f81256f42 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -405,15 +405,10 @@ object Expressions {
}
/* Set expressions */
- case class NonemptySet(elements: Set[Expr]) extends Expr {
- require(elements.nonEmpty)
- val getType = SetType(optionToType(leastUpperBound(elements.toSeq.map(_.getType)))).unveilUntyped
+ case class FiniteSet(elements: Set[Expr], base: TypeTree) extends Expr {
+ val getType = SetType(base).unveilUntyped
}
-
- case class EmptySet(tpe: TypeTree) extends Expr with Terminal {
- val getType = SetType(tpe).unveilUntyped
- }
-
+
case class ElementOfSet(element: Expr, set: Expr) extends Expr {
val getType = BooleanType
}
@@ -435,21 +430,10 @@ object Expressions {
}
/* Map operations. */
- case class NonemptyMap(singletons: Seq[(Expr, Expr)]) extends Expr {
- require(singletons.nonEmpty)
- val getType = {
- val (keys, values) = singletons.unzip
- MapType(
- optionToType(leastUpperBound(keys.map(_.getType))),
- optionToType(leastUpperBound(values.map(_.getType)))
- ).unveilUntyped
- }
- }
-
- case class EmptyMap(keyType: TypeTree, valueType: TypeTree) extends Expr with Terminal {
+ case class FiniteMap(singletons: Seq[(Expr, Expr)], keyType: TypeTree, valueType: TypeTree) extends Expr {
val getType = MapType(keyType, valueType).unveilUntyped
}
-
+
case class MapGet(map: Expr, key: Expr) extends Expr {
val getType = map.getType match {
case MapType(_, to) => to
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index d3186cde0176c0e7e24c5e81886879e22b16365f..249c4622e1c54807404ff64051b7d570bd48b415 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -108,9 +108,9 @@ object Extractors {
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, and))
case Or(args) => Some((args, or))
- case NonemptySet(els) =>
- Some(( els.toSeq, els => NonemptySet(els.toSet) ))
- case NonemptyMap(args) => {
+ case FiniteSet(els, base) =>
+ Some(( els.toSeq, els => FiniteSet(els.toSet, base) ))
+ case FiniteMap(args, f, t) => {
val subArgs = args.flatMap{case (k, v) => Seq(k, v)}
val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]) : Seq[(Expr, Expr)] = kvs match {
@@ -119,7 +119,7 @@ object Extractors {
case Seq() => Seq()
case _ => sys.error("odd number of key/value expressions")
}
- NonemptyMap(rec(as))
+ FiniteMap(rec(as), f, t)
}
Some((subArgs, builder))
}
@@ -267,14 +267,6 @@ object Extractors {
}
}
- object FiniteSet {
- def unapply(e: Expr): Option[Set[Expr]] = e match {
- case EmptySet(_) => Some(Set())
- case NonemptySet(els) => Some(els)
- case _ => None
- }
- }
-
object FiniteMultiset {
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case EmptyMultiset(_) => Some(Seq())
@@ -282,15 +274,7 @@ object Extractors {
case _ => None
}
}
-
- object FiniteMap {
- def unapply(e: Expr): Option[Seq[(Expr, Expr)]] = e match {
- case EmptyMap(_, _) => Some(Seq())
- case NonemptyMap(pairs) => Some(pairs)
- case _ => None
- }
- }
-
+
object FiniteArray {
def unapply(e: Expr): Option[(Map[Int, Expr], Option[Expr], Expr)] = e match {
case EmptyArray(_) =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 41f469eaeeff441c7e6958ab16f555406b8d99d8..b274f8edaaf045ce8f6a1dd8638c2e419317fa01 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -373,8 +373,8 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case BVShiftLeft(l,r) => optP { p"$l << $r" }
case BVAShiftRight(l,r) => optP { p"$l >> $r" }
case BVLShiftRight(l,r) => optP { p"$l >>> $r" }
- case fs @ FiniteSet(rs) => p"{${rs.toSeq}}"
- case fm @ FiniteMap(rs) => p"{$rs}"
+ case fs @ FiniteSet(rs, _) => p"{${rs.toSeq}}"
+ case fm @ FiniteMap(rs, _, _) => p"{$rs}"
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 b586ecdbee24329e6fc3bc52924738517bff4be0..07f5394e48264c56c98dfea2d9fbc6c1c15e670b 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -26,23 +26,9 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case Not(Equals(l, r)) => p"$l != $r"
case Implies(l,r) => pp(or(not(l), r))
case Choose(pred, None) => p"choose($pred)"
- case s @ FiniteSet(rss) => {
- val rs = rss.toSeq
- s.getType match {
- case SetType(ut) =>
- p"Set[$ut]($rs)"
- case _ =>
- p"Set($rs)"
- }
- }
- case m @ FiniteMap(els) => {
- m.getType match {
- case MapType(k,v) =>
- p"Map[$k,$v]($els)"
- case _ =>
- p"Map($els)"
- }
- }
+ case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})"
+ case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
+
case ElementOfSet(e,s) => p"$s.contains(e)"
case SetUnion(l,r) => p"$l ++ $r"
case MapUnion(l,r) => p"$l ++ $r"
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 56f77cabb6d8a408b1c8201b2317dd0a4b363322..635f8a03128d3d896b942c7c1bdab7ff2d506065 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -312,14 +312,11 @@ object TypeOps {
case ens @ Ensuring(body, pred) =>
Ensuring(srec(body), rec(idsMap)(pred)).copiedFrom(ens)
- case s @ FiniteSet(elements) if elements.isEmpty =>
- val SetType(tp) = s.getType
- EmptySet(tpeSub(tp)).copiedFrom(s)
-
- case m @ FiniteMap(elements) if elements.isEmpty =>
- val MapType(a,b) = m.getType
- EmptyMap(tpeSub(a), tpeSub(b)).copiedFrom(m)
+ case s @ FiniteSet(elems, tpe) =>
+ FiniteSet(elems.map(srec), tpeSub(tpe)).copiedFrom(s)
+ case m @ FiniteMap(elems, from, to) =>
+ FiniteMap(elems.map{ case (k, v) => (srec(k), srec(v)) }, tpeSub(from), tpeSub(to)).copiedFrom(m)
case v @ Variable(id) if idsMap contains id =>
Variable(idsMap(id)).copiedFrom(v)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index cfc92dc44ede4f7acf61371fd50e652e86bfee5c..1b91684774ba01cc5e794ed25dfd57fd60800704 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -71,7 +71,7 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
GenericValue(tp, n.toInt)
case (QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset"), Seq()), _), SetType(base)) =>
- EmptySet(base)
+ FiniteSet(Set(), base)
case (FunctionApplication(SimpleSymbol(SSymbol("__array_store_all__")), Seq(_, elem)), RawArrayType(k,v)) =>
RawArrayValue(k, Map(), fromSMT(elem, v))
@@ -92,12 +92,12 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
case (FunctionApplication(SimpleSymbol(SSymbol("insert")), elems), SetType(base)) =>
val selems = elems.init.map(fromSMT(_, base))
- val FiniteSet(se) = fromSMT(elems.last, tpe)
+ val FiniteSet(se, _) = fromSMT(elems.last, tpe)
finiteSet(se ++ selems, base)
case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
finiteSet(elems.map(fromSMT(_, tpe) match {
- case FiniteSet(elems) => elems
+ case FiniteSet(elems, _) => elems
}).flatten.toSet, base)
// FIXME (nicolas)
@@ -126,10 +126,9 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
FunctionApplication(constructors.toB(tpe), Seq(toSMT(size), ar))
- case fm @ FiniteMap(elems) =>
+ case fm @ FiniteMap(elems, from, to) =>
import OptionManager._
- val mt @ MapType(from, to) = fm.getType
- declareSort(mt)
+ declareSort(MapType(from, to))
var m: Term = declareVariable(FreshIdentifier("mapconst", RawArrayType(from, leonOptionType(to))))
@@ -152,7 +151,7 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
*/
- case fs @ FiniteSet(elems) =>
+ case fs @ FiniteSet(elems, _) =>
if (elems.isEmpty) {
QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset")), Some(declareSort(fs.getType)))
} else {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index a4c06d3b8597426eee0aa719631009b7e513ed7f..12a90827696eabf211dcc439e2bf82aa42b49969 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -566,7 +566,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
/**
* ===== Map operations =====
*/
- case m @ FiniteMap(elems) =>
+ case m @ FiniteMap(elems, _, _) =>
import OptionManager._
val mt @ MapType(_, to) = m.getType
val ms = declareSort(mt)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 1fb33303f6db9961d08d4b705ce22cae8aa404b8..37efdd120ba60bcafb27cc325ad7c84782d6c587 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -113,7 +113,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
/**
* ===== Set operations =====
*/
- case fs @ FiniteSet(elems) =>
+ case fs @ FiniteSet(elems, base) =>
val ss = declareSort(fs.getType)
var res: Term = FunctionApplication(
QualifiedIdentifier(SMTIdentifier(SSymbol("const")), Some(ss)),
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index b89713f944f7adc86290ac798b60f445a505fd65..4a5e6ed572d2f2fa74d38facdf0235892e83d4b7 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -636,20 +636,20 @@ trait AbstractZ3Solver
case SetIntersection(s1, s2) => z3.mkSetIntersect(rec(s1), rec(s2))
case SetUnion(s1, s2) => z3.mkSetUnion(rec(s1), rec(s2))
case SetDifference(s1, s2) => z3.mkSetDifference(rec(s1), rec(s2))
- case f @ FiniteSet(elems) => elems.foldLeft(z3.mkEmptySet(typeToSort(f.getType.asInstanceOf[SetType].base)))((ast, el) => z3.mkSetAdd(ast, rec(el)))
+ case f @ FiniteSet(elems, base) => elems.foldLeft(z3.mkEmptySet(typeToSort(base)))((ast, el) => z3.mkSetAdd(ast, rec(el)))
case SetCardinality(s) =>
val rs = rec(s)
setCardDecls(s.getType)(rs)
case SetMin(s) => intSetMinFun(rec(s))
case SetMax(s) => intSetMaxFun(rec(s))
- case f @ FiniteMap(elems) => f.getType match {
- case tpe@MapType(fromType, toType) =>
- typeToSort(tpe) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
+ case f @ FiniteMap(elems, fromType, toType) =>
+ typeToSort(MapType(fromType, toType)) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
val fromSort = typeToSort(fromType)
- 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))
- }
+ elems.foldLeft(z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())){
+ case (ast, (k,v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(toType)(rec(v)))
+ }
+
case mg @ MapGet(m,k) => m.getType match {
case MapType(fromType, toType) =>
val selected = z3.mkSelect(rec(m), rec(k))
@@ -658,7 +658,7 @@ trait AbstractZ3Solver
}
case MapUnion(m1,m2) => m1.getType match {
case MapType(ft, tt) => m2 match {
- case FiniteMap(ss) =>
+ case FiniteMap(ss, _, _) =>
ss.foldLeft(rec(m1)){
case (ast, (k, v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(tt)(rec(v)))
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 9c441813766e133c095d0608038df991a6ec9224..1465cd5325d7ad83cd5e08ef34b607af45f46693 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -82,7 +82,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
val result = checkCompSuccess(evaluator, in)
def asIntSet(e : Expr) : Option[Set[Int]] = e match {
- case FiniteSet(es) =>
+ case FiniteSet(es, _) =>
val ois = es.map {
case IntLiteral(v) => Some(v)
case _ => None
@@ -107,7 +107,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
val result = checkCompSuccess(evaluator, in)
def asIntMap(e : Expr) : Option[Map[Int,Int]] = e match {
- case FiniteMap(ss) =>
+ case FiniteMap(ss, _, _) =>
val oips : Seq[Option[(Int,Int)]] = ss.map {
case (IntLiteral(f), IntLiteral(t)) => Some(f -> t)
case _ => None
@@ -365,8 +365,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
val nil = mkCaseClass("Nil")
val cons12 = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
- val s123 = NonemptySet(Set(IL(1), IL(2), IL(3)))
- val s246 = NonemptySet(Set(IL(2), IL(4), IL(6)))
+ val s123 = FiniteSet(Set(IL(1), IL(2), IL(3)), Int32Type)
+ val s246 = FiniteSet(Set(IL(2), IL(4), IL(6)), Int32Type)
for(e <- evaluators) {
checkSetComp(e, mkCall("finite"), Set(1, 2, 3))