diff --git a/build.sbt b/build.sbt
index ccace259172b0feb5b2c551c625e2ee8fbb8b44f..111613dd1cc2dbcc2c069b031b1866b302b8cd98 100644
--- a/build.sbt
+++ b/build.sbt
@@ -170,7 +170,7 @@ parallelExecution in GenCTest := false
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "10eaaee4ea0ff6567f4f866922cb871bae2da0ac")
-lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "f3c5c174ff30c18e171f919ccc300d590e7762a0")
+lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "57834acfe2e3bc36862be52e4d99829bb8ff0ca7")
lazy val root = (project in file(".")).
configs(RegressionTest, IsabelleTest, GenCTest, IntegrTest).
diff --git a/library/lang/Bag.scala b/library/lang/Bag.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2825bd1fa4d5ca5136adb9dd0afc391b10ca5cbb
--- /dev/null
+++ b/library/lang/Bag.scala
@@ -0,0 +1,37 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.lang
+import leon.annotation._
+
+object Bag {
+ @library
+ def empty[T] = Bag[T]()
+
+ @ignore
+ def apply[T](elems: (T, BigInt)*) = {
+ new Bag[T](scala.collection.immutable.Map[T, BigInt](elems : _*))
+ }
+}
+
+@ignore
+case class Bag[T](theBag: scala.collection.immutable.Map[T, BigInt]) {
+ def +(a: T): Bag[T] = new Bag(theBag + (a -> (theBag.getOrElse(a, BigInt(0)) + 1)))
+ def ++(that: Bag[T]): Bag[T] = new Bag[T]((theBag.keys ++ that.theBag.keys).toSet.map { (k: T) =>
+ k -> (theBag.getOrElse(k, BigInt(0)) + that.theBag.getOrElse(k, BigInt(0)))
+ }.toMap)
+
+ def --(that: Bag[T]): Bag[T] = new Bag[T](theBag.flatMap { case (k,v) =>
+ val res = v - that.get(k)
+ if (res <= 0) Nil else List(k -> res)
+ })
+
+ def &(that: Bag[T]): Bag[T] = new Bag[T](theBag.flatMap { case (k,v) =>
+ val res = v min that.get(k)
+ if (res <= 0) Nil else List(k -> res)
+ })
+
+ def get(a: T): BigInt = theBag.getOrElse(a, BigInt(0))
+ def apply(a: T): BigInt = get(a)
+ def isEmpty: Boolean = theBag.isEmpty
+}
+
diff --git a/library/lang/Set.scala b/library/lang/Set.scala
index d27fd18bbab181e148c1246dd104f322a69e7c4a..351af3f6abb256229cfe27d3a13ce7ad9c191e17 100644
--- a/library/lang/Set.scala
+++ b/library/lang/Set.scala
@@ -4,25 +4,25 @@ package leon.lang
import leon.annotation._
object Set {
- @library
- def empty[T] = Set[T]()
+ @library
+ def empty[T] = Set[T]()
- @ignore
- def apply[T](elems: T*) = {
- new Set[T](scala.collection.immutable.Set[T](elems : _*))
- }
+ @ignore
+ def apply[T](elems: T*) = {
+ new Set[T](scala.collection.immutable.Set[T](elems : _*))
+ }
}
@ignore
case class Set[T](val theSet: scala.collection.immutable.Set[T]) {
- def +(a: T): Set[T] = new Set[T](theSet + a)
- def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet)
- def -(a: T): Set[T] = new Set[T](theSet - a)
- def --(a: Set[T]): Set[T] = new Set[T](theSet -- a.theSet)
- def size: BigInt = theSet.size
- def contains(a: T): Boolean = theSet.contains(a)
- def isEmpty: Boolean = theSet.isEmpty
- def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
- def &(a: Set[T]): Set[T] = new Set[T](theSet & a.theSet)
+ def +(a: T): Set[T] = new Set[T](theSet + a)
+ def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet)
+ def -(a: T): Set[T] = new Set[T](theSet - a)
+ def --(a: Set[T]): Set[T] = new Set[T](theSet -- a.theSet)
+ def size: BigInt = theSet.size
+ def contains(a: T): Boolean = theSet.contains(a)
+ def isEmpty: Boolean = theSet.isEmpty
+ def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
+ def &(a: Set[T]): Set[T] = new Set[T](theSet & a.theSet)
}
diff --git a/library/theories/Bag.scala b/library/theories/Bag.scala
new file mode 100644
index 0000000000000000000000000000000000000000..53089dcd200b379277feae1c18d7bc98bfbeb581
--- /dev/null
+++ b/library/theories/Bag.scala
@@ -0,0 +1,24 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.theories
+import leon.lang.forall
+import leon.annotation._
+
+@library
+sealed case class Bag[T](f: T => BigInt) {
+ def get(x: T): BigInt = f(x)
+ def add(elem: T): Bag[T] = Bag((x: T) => f(x) + (if (x == elem) 1 else 0))
+ def union(that: Bag[T]): Bag[T] = Bag((x: T) => f(x) + that.f(x))
+ def difference(that: Bag[T]): Bag[T] = Bag((x: T) => {
+ val res = f(x) - that.f(x)
+ if (res < 0) 0 else res
+ })
+
+ def intersect(that: Bag[T]): Bag[T] = Bag((x: T) => {
+ val r1 = f(x)
+ val r2 = that.f(x)
+ if (r1 > r2) r2 else r1
+ })
+
+ def equals(that: Bag[T]): Boolean = forall((x: T) => f(x) == that.f(x))
+}
diff --git a/library/theories/String.scala b/library/theories/String.scala
new file mode 100644
index 0000000000000000000000000000000000000000..85e4d90c7e1eca5a72a2d7c74aa0c63437d6c872
--- /dev/null
+++ b/library/theories/String.scala
@@ -0,0 +1,32 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.theories
+import leon.annotation._
+
+@library
+sealed abstract class String {
+ def size: BigInt = (this match {
+ case StringCons(_, tail) => 1 + tail.size
+ case StringNil() => BigInt(0)
+ }) ensuring (_ >= 0)
+
+ def concat(that: String): String = this match {
+ case StringCons(head, tail) => StringCons(head, tail concat that)
+ case StringNil() => that
+ }
+
+ def take(i: BigInt): String = this match {
+ case StringCons(head, tail) if i > 0 => StringCons(head, tail take (i - 1))
+ case _ => StringNil()
+ }
+
+ def drop(i: BigInt): String = this match {
+ case StringCons(head, tail) if i > 0 => tail drop (i - 1)
+ case _ => this
+ }
+
+ def slice(from: BigInt, to: BigInt): String = drop(from).take(to - from)
+}
+
+case class StringCons(head: Char, tail: String) extends String
+case class StringNil() extends String
diff --git a/src/main/java/leon/codegen/runtime/Bag.java b/src/main/java/leon/codegen/runtime/Bag.java
new file mode 100644
index 0000000000000000000000000000000000000000..e7404f522b8170523ff70e2a8e94059d05c1317b
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/Bag.java
@@ -0,0 +1,117 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.codegen.runtime;
+
+import java.util.Iterator;
+import java.util.HashMap;
+
+/** If someone wants to make it an efficient implementation of immutable
+ * sets, go ahead. */
+public final class Bag {
+ private final HashMap<Object, BigInt> _underlying;
+
+ protected final HashMap<Object, BigInt> underlying() {
+ return _underlying;
+ }
+
+ public Bag() {
+ _underlying = new HashMap<Object, BigInt>();
+ }
+
+ private Bag(HashMap<Object, BigInt> u) {
+ _underlying = u;
+ }
+
+ // Uses mutation! Useful at building time.
+ public void add(Object e) {
+ add(e, BigInt.ONE);
+ }
+
+ // Uses mutation! Useful at building time.
+ public void add(Object e, BigInt count) {
+ _underlying.put(e, get(e).add(count));
+ }
+
+ public Iterator<java.util.Map.Entry<Object, BigInt>> getElements() {
+ return _underlying.entrySet().iterator();
+ }
+
+ public BigInt get(Object element) {
+ BigInt r = _underlying.get(element);
+ if (r == null) return BigInt.ZERO;
+ else return r;
+ }
+
+ public Bag plus(Object e) {
+ Bag n = new Bag(new HashMap<Object, BigInt>(_underlying));
+ n.add(e);
+ return n;
+ }
+
+ public Bag union(Bag b) {
+ Bag n = new Bag(new HashMap<Object, BigInt>(_underlying));
+ for (java.util.Map.Entry<Object, BigInt> entry : b.underlying().entrySet()) {
+ n.add(entry.getKey(), entry.getValue());
+ }
+ return n;
+ }
+
+ public Bag intersect(Bag b) {
+ Bag n = new Bag();
+ for (java.util.Map.Entry<Object, BigInt> entry : _underlying.entrySet()) {
+ BigInt b1 = entry.getValue(), b2 = b.get(entry.getKey());
+ BigInt m = b1.lessThan(b2) ? b1 : b2;
+ if (m.greaterThan(BigInt.ZERO)) n.add(entry.getKey(), m);
+ }
+ return n;
+ }
+
+ public Bag difference(Bag b) {
+ Bag n = new Bag();
+ for (java.util.Map.Entry<Object, BigInt> entry : _underlying.entrySet()) {
+ BigInt m = entry.getValue().sub(b.get(entry.getKey()));
+ if (m.greaterThan(BigInt.ZERO)) n.add(entry.getKey(), m);
+ }
+ return n;
+ }
+
+ @Override
+ public boolean equals(Object that) {
+ if(that == this) return true;
+ if(!(that instanceof Bag)) return false;
+
+ Bag other = (Bag) that;
+ for (Object key : _underlying.keySet()) {
+ if (!get(key).equals(other.get(key))) return false;
+ }
+
+ for (Object key : other.underlying().keySet()) {
+ if (!get(key).equals(other.get(key))) return false;
+ }
+
+ return true;
+ }
+
+ @Override
+ public String toString() {
+ StringBuilder sb = new StringBuilder();
+ sb.append("Bag(");
+ boolean first = true;
+ for (java.util.Map.Entry<Object, BigInt> entry : _underlying.entrySet()) {
+ if(!first) {
+ sb.append(", ");
+ first = false;
+ }
+ sb.append(entry.getKey().toString());
+ sb.append(" -> ");
+ sb.append(entry.getValue().toString());
+ }
+ sb.append(")");
+ return sb.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return _underlying.hashCode();
+ }
+}
diff --git a/src/main/java/leon/codegen/runtime/BigInt.java b/src/main/java/leon/codegen/runtime/BigInt.java
index c4e3412b3539d56b21880734a8c63b36d06a38db..338419c11b75c058576d6630071f19e282086e8c 100644
--- a/src/main/java/leon/codegen/runtime/BigInt.java
+++ b/src/main/java/leon/codegen/runtime/BigInt.java
@@ -5,6 +5,8 @@ package leon.codegen.runtime;
import java.math.BigInteger;
public final class BigInt {
+ public static final BigInt ZERO = new BigInt(BigInteger.ZERO);
+ public static final BigInt ONE = new BigInt(BigInteger.ONE);
private final BigInteger _underlying;
diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java
index 42cadce43616eeafaaf7133d3ac7b55d229c56fb..c361ba9e662a5b84bbd84391c856ab9853d66860 100644
--- a/src/main/java/leon/codegen/runtime/Set.java
+++ b/src/main/java/leon/codegen/runtime/Set.java
@@ -23,6 +23,10 @@ public final class Set {
_underlying = new HashSet<Object>(Arrays.asList(elements));
}
+ private Set(HashSet<Object> u) {
+ _underlying = u;
+ }
+
// Uses mutation! Useful at building time.
public void add(Object e) {
_underlying.add(e);
@@ -32,14 +36,16 @@ public final class Set {
return _underlying.iterator();
}
- private Set(HashSet<Object> u) {
- _underlying = u;
- }
-
public boolean contains(Object element) {
return _underlying.contains(element);
}
+ public Set plus(Object e) {
+ Set n = new Set(new HashSet<Object>(_underlying));
+ n.add(e);
+ return n;
+ }
+
public boolean subsetOf(Set s) {
for(Object o : _underlying) {
if(!s.underlying().contains(o)) {
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 960e57ff8179e4d3f96667bf0c73842754f91781..d7a3b12c13c9ebdf55e2217b32022e4901643d54 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -72,6 +72,7 @@ trait CodeGeneration {
private[codegen] val TupleClass = "leon/codegen/runtime/Tuple"
private[codegen] val SetClass = "leon/codegen/runtime/Set"
+ private[codegen] val BagClass = "leon/codegen/runtime/Bag"
private[codegen] val MapClass = "leon/codegen/runtime/Map"
private[codegen] val BigIntClass = "leon/codegen/runtime/BigInt"
private[codegen] val RealClass = "leon/codegen/runtime/Real"
@@ -126,6 +127,9 @@ trait CodeGeneration {
case _ : SetType =>
"L" + SetClass + ";"
+ case _ : BagType =>
+ "L" + BagClass + ";"
+
case _ : MapType =>
"L" + MapClass + ";"
@@ -544,6 +548,11 @@ trait CodeGeneration {
ch << InvokeVirtual(SetClass, "add", s"(L$ObjectClass;)V")
}
+ case SetAdd(s, e) =>
+ mkExpr(s, ch)
+ mkBoxedExpr(e, ch)
+ ch << InvokeVirtual(SetClass, "plus", s"(L$ObjectClass;)L$SetClass;")
+
case ElementOfSet(e, s) =>
mkExpr(s, ch)
mkBoxedExpr(e, ch)
@@ -573,6 +582,41 @@ trait CodeGeneration {
mkExpr(s2, ch)
ch << InvokeVirtual(SetClass, "minus", s"(L$SetClass;)L$SetClass;")
+ // Bags
+ case FiniteBag(els, _) =>
+ ch << DefaultNew(BagClass)
+ for((k,v) <- els) {
+ ch << DUP
+ mkBoxedExpr(k, ch)
+ mkExpr(v, ch)
+ ch << InvokeVirtual(BagClass, "add", s"(L$ObjectClass;L$BigIntClass;)V")
+ }
+
+ case BagAdd(b, e) =>
+ mkExpr(b, ch)
+ mkBoxedExpr(e, ch)
+ ch << InvokeVirtual(BagClass, "plus", s"(L$ObjectClass;)L$BagClass;")
+
+ case MultiplicityInBag(e, b) =>
+ mkExpr(b, ch)
+ mkBoxedExpr(e, ch)
+ ch << InvokeVirtual(BagClass, "get", s"(L$ObjectClass;)L$BigIntClass;")
+
+ case BagIntersection(b1, b2) =>
+ mkExpr(b1, ch)
+ mkExpr(b2, ch)
+ ch << InvokeVirtual(BagClass, "intersect", s"(L$BagClass;)L$BagClass;")
+
+ case BagUnion(b1, b2) =>
+ mkExpr(b1, ch)
+ mkExpr(b2, ch)
+ ch << InvokeVirtual(BagClass, "union", s"(L$BagClass;)L$BagClass;")
+
+ case BagDifference(b1, b2) =>
+ mkExpr(b1, ch)
+ mkExpr(b2, ch)
+ ch << InvokeVirtual(BagClass, "difference", s"(L$BagClass;)L$BagClass;")
+
// Maps
case FiniteMap(ss, _, _) =>
ch << DefaultNew(MapClass)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index e8bd40eb2302fd9ced5fc44d6c18848c4461b867..366feffafcb9c7b994d6ccefbc1ff2f0269626dd 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -232,6 +232,13 @@ class CompilationUnit(val ctx: LeonContext,
}
s
+ case b @ FiniteBag(els, _) =>
+ val b = new leon.codegen.runtime.Bag()
+ for ((k,v) <- els) {
+ b.add(valueToJVM(k), valueToJVM(v).asInstanceOf[leon.codegen.runtime.BigInt])
+ }
+ b
+
case m @ FiniteMap(els, _, _) =>
val m = new leon.codegen.runtime.Map()
for ((k,v) <- els) {
@@ -362,6 +369,13 @@ class CompilationUnit(val ctx: LeonContext,
case (set: runtime.Set, SetType(b)) =>
FiniteSet(set.getElements.asScala.map(jvmToValue(_, b)).toSet, b)
+ case (bag: runtime.Bag, BagType(b)) =>
+ FiniteBag(bag.getElements.asScala.map { entry =>
+ val k = jvmToValue(entry.getKey, b)
+ val v = jvmToValue(entry.getValue, IntegerType)
+ (k, v)
+ }.toMap, b)
+
case (map: runtime.Map, MapType(from, to)) =>
val pairs = map.getElements.asScala.map { entry =>
val k = jvmToValue(entry.getKey, from)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 0b533e631dee5b0a41181262e0d8c8702b40ea62..6e13cb030ad7df32b6a5ec1543e6d2c80915903d 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -106,6 +106,19 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
constructors += st -> cs
cs
})
+
+ case bt @ BagType(sub) =>
+ constructors.getOrElse(bt, {
+ val cs = for (size <- List(0, 1, 2, 5)) yield {
+ val subs = (1 to size).flatMap(i => List(sub, IntegerType)).toList
+ Constructor[Expr, TypeTree](subs, bt, s => FiniteBag(s.grouped(2).map {
+ case Seq(k, i @ InfiniteIntegerLiteral(v)) =>
+ k -> (if (v > 0) i else InfiniteIntegerLiteral(-v + 1))
+ }.toMap, sub), bt.asString(ctx)+"@"+size)
+ }
+ constructors += bt -> cs
+ cs
+ })
case tt @ TupleType(parts) =>
constructors.getOrElse(tt, {
@@ -117,7 +130,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case mt @ MapType(from, to) =>
constructors.getOrElse(mt, {
val cs = for (size <- List(0, 1, 2, 5)) yield {
- val subs = (1 to size).flatMap(i => List(from, to)).toList
+ val subs = (1 to size).flatMap(i => List(from, to)).toList
Constructor[Expr, TypeTree](subs, mt, s => FiniteMap(s.grouped(2).map(t => (t(0), t(1))).toMap, from, to), mt.asString(ctx)+"@"+size)
}
constructors += mt -> cs
@@ -347,8 +360,9 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
def computeNext(): Option[Seq[Expr]] = {
//return None
- while(total < maxEnumerated && found < maxValid && it.hasNext && !interrupted.get) {
+ while (total < maxEnumerated && found < maxValid && it.hasNext && !interrupted.get) {
val model = it.next()
+ it.hasNext // FIXME: required for some reason by StubGenerator or will return false during loop check
if (model eq null) {
total = maxEnumerated
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 418ac42e62409d18d7ebb39276b9fe40e85b063b..17b44ea45be7bced78fe23712878977633e17840 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -186,6 +186,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(lv,rv) match {
case (FiniteSet(el1, _),FiniteSet(el2, _)) => BooleanLiteral(el1 == el2)
+ case (FiniteBag(el1, _),FiniteBag(el2, _)) => BooleanLiteral(el1 == el2)
case (FiniteMap(el1, _, _),FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
case (FiniteLambda(m1, d1, _), FiniteLambda(m2, d2, _)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
case _ => BooleanLiteral(lv == rv)
@@ -466,40 +467,40 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
+ case SetAdd(s1, elem) =>
+ (e(s1), e(elem)) match {
+ case (FiniteSet(els1, tpe), evElem) => FiniteSet(els1 + evElem, tpe)
+ case (le, re) => throw EvalError(typeErrorMsg(le, s1.getType))
+ }
+
case SetUnion(s1,s2) =>
(e(s1), e(s2)) match {
- case (f@FiniteSet(els1, _),FiniteSet(els2, _)) =>
- val SetType(tpe) = f.getType
- FiniteSet(els1 ++ els2, tpe)
- case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
+ case (FiniteSet(els1, tpe), FiniteSet(els2, _)) => FiniteSet(els1 ++ els2, tpe)
+ 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 intersect els2
- val SetType(tpe) = f.getType
- FiniteSet(newElems, tpe)
+ case (FiniteSet(els1, tpe), FiniteSet(els2, _)) => FiniteSet(els1 intersect els2, tpe)
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case SetDifference(s1,s2) =>
(e(s1), e(s2)) match {
- case (f @ FiniteSet(els1, _),FiniteSet(els2, _)) =>
- val SetType(tpe) = f.getType
- val newElems = els1 -- els2
- FiniteSet(newElems, tpe)
+ case (FiniteSet(els1, tpe), FiniteSet(els2, _)) => FiniteSet(els1 -- els2, tpe)
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case ElementOfSet(el,s) => (e(el), e(s)) match {
- case (e, f @ FiniteSet(els, _)) => BooleanLiteral(els.contains(e))
+ case (e, 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.subsetOf(els2))
+ case (FiniteSet(els1, _),FiniteSet(els2, _)) => BooleanLiteral(els1.subsetOf(els2))
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
+
case SetCardinality(s) =>
val sr = e(s)
sr match {
@@ -510,6 +511,61 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case f @ FiniteSet(els, base) =>
FiniteSet(els.map(e), base)
+ case BagAdd(bag, elem) => (e(bag), e(elem)) match {
+ case (FiniteBag(els, tpe), evElem) => FiniteBag(els + (evElem -> (els.get(evElem) match {
+ case Some(InfiniteIntegerLiteral(i)) => InfiniteIntegerLiteral(i + 1)
+ case Some(i) => throw EvalError(typeErrorMsg(i, IntegerType))
+ case None => InfiniteIntegerLiteral(1)
+ })), tpe)
+
+ case (le, re) => throw EvalError(typeErrorMsg(le, bag.getType))
+ }
+
+ case MultiplicityInBag(elem, bag) => (e(elem), e(bag)) match {
+ case (evElem, FiniteBag(els, tpe)) => els.getOrElse(evElem, InfiniteIntegerLiteral(0))
+ case (le, re) => throw EvalError(typeErrorMsg(re, bag.getType))
+ }
+
+ case BagIntersection(b1, b2) => (e(b1), e(b2)) match {
+ case (FiniteBag(els1, tpe), FiniteBag(els2, _)) => FiniteBag(els1.flatMap { case (k, v) =>
+ val i = (v, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 min i2
+ case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
+
+ if (i <= 0) None else Some(k -> InfiniteIntegerLiteral(i))
+ }, tpe)
+
+ case (le, re) => throw EvalError(typeErrorMsg(le, b1.getType))
+ }
+
+ case BagUnion(b1, b2) => (e(b1), e(b2)) match {
+ case (FiniteBag(els1, tpe), FiniteBag(els2, _)) => FiniteBag((els1.keys ++ els2.keys).toSet.map { (k: Expr) =>
+ k -> ((els1.getOrElse(k, InfiniteIntegerLiteral(0)), els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 + i2)
+ case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ })
+ }.toMap, tpe)
+
+ case (le, re) => throw EvalError(typeErrorMsg(le, b1.getType))
+ }
+
+ case BagDifference(b1, b2) => (e(b1), e(b2)) match {
+ case (FiniteBag(els1, tpe), FiniteBag(els2, _)) => FiniteBag(els1.flatMap { case (k, v) =>
+ val i = (v, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 - i2
+ case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
+
+ if (i <= 0) None else Some(k -> InfiniteIntegerLiteral(i))
+ }, tpe)
+
+ case (le, re) => throw EvalError(typeErrorMsg(le, b1.getType))
+ }
+
+ case FiniteBag(els, base) =>
+ FiniteBag(els.map{ case (k, v) => (e(k), e(v)) }, base)
+
case l @ Lambda(_, _) =>
val mapping = variablesOf(l).map(id => id -> e(Variable(id))).toMap
val newLambda = replaceFromIDs(mapping, l).asInstanceOf[Lambda]
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index d53869f898288ba466b8d79729ba8964dbf06095..d36a4b73951ef113c9fe199676b977693c6c8f31 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -397,6 +397,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
case (Equals(_, _), Seq(lv, rv)) =>
(lv, rv) match {
case (FiniteSet(el1, _), FiniteSet(el2, _)) => BooleanLiteral(el1 == el2)
+ case (FiniteBag(el1, _), FiniteBag(el2, _)) => BooleanLiteral(el1 == el2)
case (FiniteMap(el1, _, _), FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
case (FiniteLambda(m1, d1, _), FiniteLambda(m2, d2, _)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
case _ => BooleanLiteral(lv == rv)
@@ -540,14 +541,23 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
(el, er) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
- case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
+ case (a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) =>
val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
BooleanLiteral(n >= 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
- case (IsTyped(su@SetUnion(s1, s2), tpe), Seq(
+ case (IsTyped(sa @ SetAdd(_, _), tpe), Seq(
+ IsTyped(FiniteSet(els1, _), SetType(tpe1)),
+ IsTyped(elem, tpe2)
+ )) =>
+ FiniteSet(
+ els1 + elem,
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(sa, tpe)))
+ )
+
+ case (IsTyped(su @ SetUnion(s1, s2), tpe), Seq(
IsTyped(FiniteSet(els1, _), SetType(tpe1)),
IsTyped(FiniteSet(els2, _), SetType(tpe2))
)) =>
@@ -556,7 +566,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
)
- case (IsTyped(su@SetIntersection(s1, s2), tpe), Seq(
+ case (IsTyped(su @ SetIntersection(s1, s2), tpe), Seq(
IsTyped(FiniteSet(els1, _), SetType(tpe1)),
IsTyped(FiniteSet(els2, _), SetType(tpe2))
)) =>
@@ -565,7 +575,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
)
- case (IsTyped(su@SetDifference(s1, s2), tpe), Seq(
+ case (IsTyped(su @ SetDifference(s1, s2), tpe), Seq(
IsTyped(FiniteSet(els1, _), SetType(tpe1)),
IsTyped(FiniteSet(els2, _), SetType(tpe2))
)) =>
@@ -586,6 +596,69 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
case (FiniteSet(_, base), els) =>
FiniteSet(els.toSet, base)
+ case (IsTyped(ba @ BagAdd(_, _), tpe), Seq(
+ IsTyped(FiniteBag(els1, _), BagType(tpe1)),
+ IsTyped(e, tpe2)
+ )) =>
+ FiniteBag(
+ els1 + (e -> (els1.getOrElse(e, InfiniteIntegerLiteral(0)) match {
+ case InfiniteIntegerLiteral(i) => InfiniteIntegerLiteral(i + 1)
+ case il => throw EvalError(typeErrorMsg(il, IntegerType))
+ })),
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(ba, tpe)))
+ )
+
+ case (IsTyped(bu @ BagUnion(b1, b2), tpe), Seq(
+ IsTyped(FiniteBag(els1, _), BagType(tpe1)),
+ IsTyped(FiniteBag(els2, _), BagType(tpe2))
+ )) =>
+ FiniteBag(
+ (els1.keys ++ els2.keys).map(k => k -> {
+ ((els1.getOrElse(k, InfiniteIntegerLiteral(0)), els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 + i2)
+ case (l, r) => throw EvalError(typeErrorMsg(l, IntegerType))
+ })
+ }).toMap,
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(bu, tpe)))
+ )
+
+ case (IsTyped(bi @ BagIntersection(s1, s2), tpe), Seq(
+ IsTyped(FiniteBag(els1, _), BagType(tpe1)),
+ IsTyped(FiniteBag(els2, _), BagType(tpe2))
+ )) =>
+ FiniteBag(
+ els1.flatMap { case (k, e) =>
+ val res = (e, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 min i2
+ case (l, r) => throw EvalError(typeErrorMsg(l, IntegerType))
+ }
+ if (res <= 0) None else Some(k -> InfiniteIntegerLiteral(res))
+ },
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(bi, tpe)))
+ )
+
+ case (IsTyped(bd @ BagDifference(s1, s2), tpe), Seq(
+ IsTyped(FiniteBag(els1, _), BagType(tpe1)),
+ IsTyped(FiniteBag(els2, _), BagType(tpe2))
+ )) =>
+ FiniteBag(
+ els1.flatMap { case (k, e) =>
+ val res = (e, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 - i2
+ case (l, r) => throw EvalError(typeErrorMsg(l, IntegerType))
+ }
+ if (res <= 0) None else Some(k -> InfiniteIntegerLiteral(res))
+ },
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(bd, tpe)))
+ )
+
+ case (MultiplicityInBag(_, _), Seq(e, FiniteBag(els, _))) =>
+ els.getOrElse(e, InfiniteIntegerLiteral(0))
+
+ case (fb @ FiniteBag(_, _), els) =>
+ val Operator(_, builder) = fb
+ builder(els)
+
case (ArrayLength(_), Seq(FiniteArray(_, _, IntLiteral(length)))) =>
IntLiteral(length)
@@ -602,15 +675,15 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
.orElse(if (index >= 0 && index < length) default else None)
.getOrElse(throw RuntimeError(s"Array out of bounds error during evaluation:\n array = $fa, index = $index"))
- case (fa@FiniteArray(_, _, _), subs) =>
+ case (fa @ FiniteArray(_, _, _), subs) =>
val Operator(_, builder) = fa
builder(subs)
- case (fm@FiniteMap(_, _, _), subs) =>
+ case (fm @ FiniteMap(_, _, _), subs) =>
val Operator(_, builder) = fm
builder(subs)
- case (g@MapApply(_, _), Seq(FiniteMap(m, _, _), k)) =>
+ case (g @ MapApply(_, _), Seq(FiniteMap(m, _, _), k)) =>
m.getOrElse(k, throw RuntimeError("Key not found: " + k.asString))
case (u@IsTyped(MapUnion(_, _), MapType(kT, vT)), Seq(FiniteMap(m1, _, _), FiniteMap(m2, _, _))) =>
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 7890d7a229da487e8ae8152ae92c7b0b066eb12e..1d107703b1bfe5dff1658bab08b44d0ae84fa2e8 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -44,6 +44,7 @@ trait ASTExtractors {
protected lazy val scalaSetSym = classFromName("scala.collection.immutable.Set")
protected lazy val setSym = classFromName("leon.lang.Set")
protected lazy val mapSym = classFromName("leon.lang.Map")
+ protected lazy val bagSym = classFromName("leon.lang.Bag")
protected lazy val realSym = classFromName("leon.lang.Real")
protected lazy val optionClassSym = classFromName("scala.Option")
protected lazy val arraySym = classFromName("scala.Array")
@@ -80,6 +81,10 @@ trait ASTExtractors {
getResolvedTypeSym(sym) == setSym
}
+ def isBagSym(sym: Symbol) : Boolean = {
+ getResolvedTypeSym(sym) == bagSym
+ }
+
def isRealSym(sym: Symbol) : Boolean = {
getResolvedTypeSym(sym) == realSym
}
@@ -1038,6 +1043,16 @@ trait ASTExtractors {
}
}
+ object ExFiniteBag {
+ def unapply(tree: Apply): Option[(Tree, List[Tree])] = tree match {
+ case Apply(TypeApply(ExSelected("Bag", "apply"), Seq(tpt)), args) =>
+ Some(tpt, args)
+ case Apply(TypeApply(ExSelected("leon", "lang", "Bag", "apply"), Seq(tpt)), args) =>
+ Some(tpt, args)
+ case _ => None
+ }
+ }
+
object ExFiniteMap {
def unapply(tree: Apply): Option[(Tree, Tree, List[Tree])] = tree match {
case Apply(TypeApply(ExSelected("Map", "apply"), Seq(tptFrom, tptTo)), args) =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 993bc4fd0c0f48b56c18eae3b2889f303306027c..0a80b3b53933a6bb6f5c88d8785ea8f3eb1cebaa 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1461,20 +1461,26 @@ trait CodeExtraction extends ASTExtractors {
Forall(vds, exBody)
case ExFiniteMap(tptFrom, tptTo, args) =>
- val singletons = args.collect {
- case ExTuple(tpes, trees) if trees.size == 2 =>
- (extractTree(trees(0)), extractTree(trees(1)))
- }.toMap
-
- if (singletons.size != args.size) {
- outOfSubsetError(tr, "Some map elements could not be extracted as Tuple2")
- }
-
- FiniteMap(singletons, extractType(tptFrom), extractType(tptTo))
+ FiniteMap(args.map {
+ case ExTuple(tpes, Seq(key, value)) =>
+ (extractTree(key), extractTree(value))
+ case tree =>
+ val ex = extractTree(tree)
+ (TupleSelect(ex, 1), TupleSelect(ex, 2))
+ }.toMap, extractType(tptFrom), extractType(tptTo))
case ExFiniteSet(tpt, args) =>
FiniteSet(args.map(extractTree).toSet, extractType(tpt))
+ case ExFiniteBag(tpt, args) =>
+ FiniteBag(args.map {
+ case ExTuple(tpes, Seq(key, value)) =>
+ (extractTree(key), extractTree(value))
+ case tree =>
+ val ex = extractTree(tree)
+ (TupleSelect(ex, 1), TupleSelect(ex, 2))
+ }.toMap, extractType(tpt))
+
case ExCaseClassConstruction(tpt, args) =>
extractType(tpt) match {
case cct: CaseClassType =>
@@ -1669,6 +1675,7 @@ trait CodeExtraction extends ASTExtractors {
val id = cct.classDef.fields.find(_.id.name == name.dropRight(2)).get.id
FieldAssignment(rec, id, e1)
+
//String methods
case (IsTyped(a1, StringType), "toString", List()) =>
a1
@@ -1686,6 +1693,8 @@ trait CodeExtraction extends ASTExtractors {
SubString(a1, start, StringLength(a1))
case (IsTyped(a1, StringType), "substring", List(IsTyped(start, IntegerType | Int32Type), IsTyped(end, IntegerType | Int32Type))) =>
SubString(a1, start, end)
+
+
//BigInt methods
case (IsTyped(a1, IntegerType), "+", List(IsTyped(a2, IntegerType))) =>
Plus(a1, a2)
@@ -1708,6 +1717,7 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, IntegerType), "<=", List(IsTyped(a2, IntegerType))) =>
LessEquals(a1, a2)
+
//Real methods
case (IsTyped(a1, RealType), "+", List(IsTyped(a2, RealType))) =>
RealPlus(a1, a2)
@@ -1726,6 +1736,7 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, RealType), "<=", List(IsTyped(a2, RealType))) =>
LessEquals(a1, a2)
+
// Int methods
case (IsTyped(a1, Int32Type), "+", List(IsTyped(a2, Int32Type))) =>
BVPlus(a1, a2)
@@ -1760,6 +1771,7 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, Int32Type), "<=", List(IsTyped(a2, Int32Type))) =>
LessEquals(a1, a2)
+
// Boolean methods
case (IsTyped(a1, BooleanType), "&&", List(IsTyped(a2, BooleanType))) =>
and(a1, a2)
@@ -1767,6 +1779,7 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, BooleanType), "||", List(IsTyped(a2, BooleanType))) =>
or(a1, a2)
+
// Set methods
case (IsTyped(a1, SetType(b1)), "size", Nil) =>
SetCardinality(a1)
@@ -1777,6 +1790,9 @@ trait CodeExtraction extends ASTExtractors {
//case (IsTyped(a1, SetType(b1)), "max", Nil) =>
// SetMax(a1)
+ case (IsTyped(a1, SetType(b1)), "+", List(a2)) =>
+ SetAdd(a1, a2)
+
case (IsTyped(a1, SetType(b1)), "++", List(IsTyped(a2, SetType(b2)))) if b1 == b2 =>
SetUnion(a1, a2)
@@ -1795,6 +1811,27 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, SetType(b1)), "isEmpty", List()) =>
Equals(a1, FiniteSet(Set(), b1))
+
+ // Bag methods
+ case (IsTyped(a1, BagType(b1)), "+", List(a2)) =>
+ BagAdd(a1, a2)
+
+ case (IsTyped(a1, BagType(b1)), "++", List(IsTyped(a2, BagType(b2)))) if b1 == b2 =>
+ BagUnion(a1, a2)
+
+ case (IsTyped(a1, BagType(b1)), "&", List(IsTyped(a2, BagType(b2)))) if b1 == b2 =>
+ BagIntersection(a1, a2)
+
+ case (IsTyped(a1, BagType(b1)), "--", List(IsTyped(a2, BagType(b2)))) if b1 == b2 =>
+ BagDifference(a1, a2)
+
+ case (IsTyped(a1, BagType(b1)), "get", List(a2)) =>
+ MultiplicityInBag(a2, a1)
+
+ case (IsTyped(a1, BagType(b1)), "isEmpty", List()) =>
+ Equals(a1, FiniteBag(Map(), b1))
+
+
// Array methods
case (IsTyped(a1, ArrayType(vt)), "apply", List(a2)) =>
ArraySelect(a1, a2)
@@ -1926,6 +1963,9 @@ trait CodeExtraction extends ASTExtractors {
case TypeRef(_, sym, btt :: Nil) if isSetSym(sym) =>
SetType(extractType(btt))
+ case TypeRef(_, sym, btt :: Nil) if isBagSym(sym) =>
+ BagType(extractType(btt))
+
case TypeRef(_, sym, List(ftt,ttt)) if isMapSym(sym) =>
MapType(extractType(ftt), extractType(ttt))
diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index 89c5b613b426f8d6c9b6b2eeaa1273da2496ed40..6be2448adf41b1c2962ef458ca838d04c13b9bdb 100644
--- a/src/main/scala/leon/purescala/DefinitionTransformer.scala
+++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala
@@ -97,7 +97,7 @@ class DefinitionTransformer(
for (fd <- requiredFds) {
val nfd = fdMap.toB(fd)
- fd.fullBody = transform(fd.fullBody)((fd.params zip nfd.params).map(p => p._1.id -> p._2.id).toMap)
+ nfd.fullBody = transform(fd.fullBody)((fd.params zip nfd.params).map(p => p._1.id -> p._2.id).toMap)
}
}
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 4f7bc819650c5316ab4dc3ff3bf1cf1203cb9a1d..b917447942ad3996163f5e970e316d0e1aee4b67 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -856,6 +856,7 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
case BooleanType => BooleanLiteral(false)
case UnitType => UnitLiteral()
case SetType(baseType) => FiniteSet(Set(), baseType)
+ case BagType(baseType) => FiniteBag(Map(), baseType)
case MapType(fromType, toType) => FiniteMap(Map(), 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 79172eb7a538c298e5b5eb026eb3e8dfca397f3a..3855813de7e618bc272c6cc845cb24bb3983a5e3 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -821,9 +821,22 @@ object Expressions {
case class FiniteSet(elements: Set[Expr], base: TypeTree) extends Expr {
val getType = SetType(base).unveilUntyped
}
+ /** $encodingof `set + elem` */
+ case class SetAdd(set: Expr, elem: Expr) extends Expr {
+ val getType = {
+ val base = set.getType match {
+ case SetType(base) => base
+ case _ => Untyped
+ }
+ checkParamTypes(Seq(elem.getType), Seq(base), SetType(base).unveilUntyped)
+ }
+ }
/** $encodingof `set.contains(element)` or `set(element)` */
case class ElementOfSet(element: Expr, set: Expr) extends Expr {
- val getType = BooleanType
+ val getType = checkParamTypes(Seq(element.getType), Seq(set.getType match {
+ case SetType(base) => base
+ case _ => Untyped
+ }), BooleanType)
}
/** $encodingof `set.length` */
case class SetCardinality(set: Expr) extends Expr {
@@ -831,9 +844,12 @@ object Expressions {
}
/** $encodingof `set.subsetOf(set2)` */
case class SubsetOf(set1: Expr, set2: Expr) extends Expr {
- val getType = BooleanType
+ val getType = (set1.getType, set2.getType) match {
+ case (SetType(b1), SetType(b2)) if b1 == b2 => BooleanType
+ case _ => Untyped
+ }
}
- /** $encodingof `set.intersect(set2)` */
+ /** $encodingof `set & set2` */
case class SetIntersection(set1: Expr, set2: Expr) extends Expr {
val getType = leastUpperBound(Seq(set1, set2).map(_.getType)).getOrElse(Untyped).unveilUntyped
}
@@ -848,26 +864,27 @@ object Expressions {
/* Bag operations */
/** $encodingof `Bag[base](elements)` */
- case class FiniteBag(elements: Map[Expr, Int], base: TypeTree) extends Expr {
+ case class FiniteBag(elements: Map[Expr, Expr], base: TypeTree) extends Expr {
val getType = BagType(base).unveilUntyped
}
+ /** $encodingof `bag + elem` */
+ case class BagAdd(bag: Expr, elem: Expr) extends Expr {
+ val getType = {
+ val base = bag.getType match {
+ case BagType(base) => base
+ case _ => Untyped
+ }
+ checkParamTypes(Seq(base), Seq(elem.getType), BagType(base).unveilUntyped)
+ }
+ }
/** $encodingof `bag.get(element)` or `bag(element)` */
case class MultiplicityInBag(element: Expr, bag: Expr) extends Expr {
- val getType = IntegerType
- }
- /** $encodingof `bag.length` */
- /*
- case class BagCardinality(bag: Expr) extends Expr {
- val getType = IntegerType
- }
- */
- /** $encodingof `bag1.subsetOf(bag2)` */
- /*
- case class SubbagOf(bag1: Expr, bag2: Expr) extends Expr {
- val getType = BooleanType
+ val getType = checkParamTypes(Seq(element.getType), Seq(bag.getType match {
+ case BagType(base) => base
+ case _ => Untyped
+ }), IntegerType)
}
- */
- /** $encodingof `bag1.intersect(bag2)` */
+ /** $encodingof `bag1 & bag2` */
case class BagIntersection(bag1: Expr, bag2: Expr) extends Expr {
val getType = leastUpperBound(Seq(bag1, bag2).map(_.getType)).getOrElse(Untyped).unveilUntyped
}
@@ -876,12 +893,10 @@ object Expressions {
val getType = leastUpperBound(Seq(bag1, bag2).map(_.getType)).getOrElse(Untyped).unveilUntyped
}
/** $encodingof `bag1 -- bag2` */
- /*
- case class SetDifference(bag1: Expr, bag2: Expr) extends Expr {
- val getType = leastUpperBound(Seq(set1, set2).map(_.getType)).getOrElse(Untyped).unveilUntyped
+ case class BagDifference(bag1: Expr, bag2: Expr) extends Expr {
+ val getType = leastUpperBound(Seq(bag1, bag2).map(_.getType)).getOrElse(Untyped).unveilUntyped
}
- */
-
+
// TODO: Add checks for these expressions too
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 5c09c2d296bcbf7ddeb3518f2c42acdc6a695cb8..ea5b30430005fecbb8eb6c5d8082a415cb1e24e2 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -134,6 +134,8 @@ object Extractors {
Some(Seq(t1, t2), (es: Seq[Expr]) => RealDivision(es(0), es(1)))
case StringConcat(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => StringConcat(es(0), es(1)))
+ case SetAdd(t1, t2) =>
+ Some(Seq(t1, t2), (es: Seq[Expr]) => SetAdd(es(0), es(1)))
case ElementOfSet(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => ElementOfSet(es(0), es(1)))
case SubsetOf(t1, t2) =>
@@ -144,12 +146,16 @@ object Extractors {
Some(Seq(t1, t2), (es: Seq[Expr]) => SetUnion(es(0), es(1)))
case SetDifference(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => SetDifference(es(0), es(1)))
+ case BagAdd(e1, e2) =>
+ Some(Seq(e1, e2), (es: Seq[Expr]) => BagAdd(es(0), es(1)))
case MultiplicityInBag(e1, e2) =>
Some(Seq(e1, e2), (es: Seq[Expr]) => MultiplicityInBag(es(0), es(1)))
case BagIntersection(e1, e2) =>
Some(Seq(e1, e2), (es: Seq[Expr]) => BagIntersection(es(0), es(1)))
case BagUnion(e1, e2) =>
Some(Seq(e1, e2), (es: Seq[Expr]) => BagUnion(es(0), es(1)))
+ case BagDifference(e1, e2) =>
+ Some(Seq(e1, e2), (es: Seq[Expr]) => BagDifference(es(0), es(1)))
case mg @ MapApply(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => MapApply(es(0), es(1)))
case MapUnion(t1, t2) =>
@@ -180,13 +186,22 @@ object Extractors {
case FiniteSet(els, base) =>
Some((els.toSeq, els => FiniteSet(els.toSet, base)))
case FiniteBag(els, base) =>
- val seq = els.toSeq
- Some((seq.map(_._1), els => FiniteBag((els zip seq.map(_._2)).toMap, base)))
+ val subArgs = els.flatMap { case (k, v) => Seq(k, v) }.toSeq
+ val builder = (as: Seq[Expr]) => {
+ def rec(kvs: Seq[Expr]): Map[Expr, Expr] = kvs match {
+ case Seq(k, v, t @ _*) =>
+ Map(k -> v) ++ rec(t)
+ case Seq() => Map()
+ case _ => sys.error("odd number of key/value expressions")
+ }
+ FiniteBag(rec(as), base)
+ }
+ Some((subArgs, builder))
case FiniteMap(args, f, t) => {
val subArgs = args.flatMap { case (k, v) => Seq(k, v) }.toSeq
val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]): Map[Expr, Expr] = kvs match {
- case Seq(k, v, t@_*) =>
+ case Seq(k, v, t @ _*) =>
Map(k -> v) ++ rec(t)
case Seq() => Map()
case _ => sys.error("odd number of key/value expressions")
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index f1b80fd9de6df1996d33fdc7936669be6a997b73..38644fc4a896cb2f84eefac53eb6652dd041e8a1 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -321,16 +321,23 @@ class PrettyPrinter(opts: PrinterOptions,
case RealTimes(l,r) => optP { p"$l * $r" }
case RealDivision(l,r) => optP { p"$l / $r" }
case fs @ FiniteSet(rs, _) => p"{${rs.toSeq}}"
+ case fs @ FiniteBag(rs, _) => p"{$rs}"
case fm @ FiniteMap(rs, _, _) => p"{$rs}"
case Not(ElementOfSet(e,s)) => p"$e \u2209 $s"
case ElementOfSet(e,s) => p"$e \u2208 $s"
case SubsetOf(l,r) => p"$l \u2286 $r"
case Not(SubsetOf(l,r)) => p"$l \u2288 $r"
+ case SetAdd(s,e) => p"$s \u222A {$e}"
case SetUnion(l,r) => p"$l \u222A $r"
+ case BagUnion(l,r) => p"$l \u222A $r"
case MapUnion(l,r) => p"$l \u222A $r"
case SetDifference(l,r) => p"$l \\ $r"
+ case BagDifference(l,r) => p"$l \\ $r"
case SetIntersection(l,r) => p"$l \u2229 $r"
+ case BagIntersection(l,r) => p"$l \u2229 $r"
case SetCardinality(s) => p"$s.size"
+ case BagAdd(b,e) => p"$b + $e"
+ case MultiplicityInBag(e, b) => p"$b($e)"
case MapApply(m,k) => p"$m($k)"
case MapIsDefinedAt(m,k) => p"$m.isDefinedAt($k)"
case ArrayLength(a) => p"$a.length"
@@ -464,6 +471,7 @@ class PrettyPrinter(opts: PrinterOptions,
case StringType => p"String"
case ArrayType(bt) => p"Array[$bt]"
case SetType(bt) => p"Set[$bt]"
+ case BagType(bt) => p"Bag[$bt]"
case MapType(ft,tt) => p"Map[$ft, $tt]"
case TupleType(tpes) => p"($tpes)"
case FunctionType(fts, tt) => p"($fts) => $tt"
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 03c50eb2e752ad0dd3827703eff4fc44542e5b2c..40dcbdab8188f71988d78e58ffb200224de57891 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -28,6 +28,7 @@ class ScalaPrinter(opts: PrinterOptions,
case Choose(pred) => p"choose($pred)"
case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})"
+ case SetAdd(s,e) => optP { p"$s + $e" }
case ElementOfSet(e,s) => p"$s.contains($e)"
case SetUnion(l,r) => optP { p"$l ++ $r" }
case SetDifference(l,r) => optP { p"$l -- $r" }
@@ -35,6 +36,12 @@ class ScalaPrinter(opts: PrinterOptions,
case SetCardinality(s) => p"$s.size"
case SubsetOf(subset,superset) => p"$subset.subsetOf($superset)"
+ case b @ FiniteBag(els, t) => p"Bag[$t]($els)"
+ case BagAdd(s,e) => optP { p"$s + $e" }
+ case BagUnion(l,r) => optP { p"$l ++ $r" }
+ case BagDifference(l,r) => optP { p"$l -- $r" }
+ case BagIntersection(l,r) => optP { p"$l & $r" }
+
case MapUnion(l,r) => optP { p"$l ++ $r" }
case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index e2838104fd704110fbb06e6234ea1ae2599a20e7..1536395e92798360c70b5ad8fcebf3520520768c 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -143,6 +143,7 @@ object Types {
case TupleType(ts) => Some((ts, Constructors.tupleTypeWrap _))
case ArrayType(t) => Some((Seq(t), ts => ArrayType(ts.head)))
case SetType(t) => Some((Seq(t), ts => SetType(ts.head)))
+ case BagType(t) => Some((Seq(t), ts => BagType(ts.head)))
case MapType(from,to) => Some((Seq(from, to), t => MapType(t(0), t(1))))
case FunctionType(fts, tt) => Some((tt +: fts, ts => FunctionType(ts.tail.toList, ts.head)))
/* n-ary operators */
diff --git a/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala b/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
index 3ddfca8d9524f9052dc5e6e49266006e9ffa2e3b..97b5d4dc91a2efcf8c4c6446a7049f4ef28b42fa 100644
--- a/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
@@ -10,4 +10,4 @@ import unrolling._
import theories._
class CVC4UnrollingSolver(context: LeonContext, program: Program, underlying: Solver)
- extends UnrollingSolver(context, program, underlying, theories = new NoEncoder)
+ extends UnrollingSolver(context, program, underlying, theories = new BagEncoder(context, program))
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 5de74510b465d76cfc152c476cff96321c4758e9..8838ae8ffc6443ba2961f51ecce795004dc98233 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -9,7 +9,7 @@ import solvers.theories._
import purescala.Definitions.Program
class SMTLIBCVC4Solver(context: LeonContext, program: Program)
- extends SMTLIBSolver(context, program, new NoEncoder)
+ extends SMTLIBSolver(context, program, new BagEncoder(context, program))
with SMTLIBCVC4Target {
def targetName = "cvc4"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 7418526c9338fce9c558d118fb947af503ee53ec..cd7eae5e8330bac85f5a554b624bf98576655895 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -197,9 +197,15 @@ trait SMTLIBTarget extends Interruptible {
unsupported(r, "Solver returned a co-finite set which is not supported.")
}
require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
-
FiniteSet(r.elems.keySet, base)
+ case BagType(base) =>
+ if (r.default != InfiniteIntegerLiteral(0)) {
+ unsupported(r, "Solver returned an infinite bag which is not supported.")
+ }
+ require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
+ FiniteBag(r.elems, base)
+
case RawArrayType(from, to) =>
r
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 6a58f9f1a294180182595bcb34d35d1a2ffe08a7..43c1643cf89bef425d30fa1c4e6e11eaa02cf3ed 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -16,7 +16,7 @@ import _root_.smtlib.theories.Core.{Equals => _, _}
import theories._
class SMTLIBZ3Solver(context: LeonContext, program: Program)
- extends SMTLIBSolver(context, program, new StringEncoder)
+ extends SMTLIBSolver(context, program, new StringEncoder(context, program))
with SMTLIBZ3Target {
def getProgram: Program = program
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 1be3f7ecf930990749565a1c7ca2181cd2a100dd..00b361323de76d5647a124eb65f449161390a15e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -9,11 +9,12 @@ import purescala.Expressions._
import purescala.Constructors._
import purescala.Types._
-import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
+import _root_.smtlib.common._
+import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Let => SMTLet, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.interpreters.Z3Interpreter
import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
-import _root_.smtlib.theories.ArraysEx
+import _root_.smtlib.theories._
trait SMTLIBZ3Target extends SMTLIBTarget {
@@ -44,6 +45,8 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case SetType(base) =>
super.declareSort(BooleanType)
declareSetSort(base)
+ case BagType(base) =>
+ declareSort(RawArrayType(base, IntegerType))
case _ =>
super.declareSort(t)
}
@@ -112,6 +115,9 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
SMTEquals(ArrayMap(SSymbol("implies"), toSMT(ss), toSMT(s)), allTrue)
+ case SetAdd(s, e) =>
+ ArraysEx.Store(toSMT(s), toSMT(e), True())
+
case ElementOfSet(e, s) =>
ArraysEx.Select(toSMT(s), toSMT(e))
@@ -128,6 +134,39 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case SetIntersection(l, r) =>
ArrayMap(SSymbol("and"), toSMT(l), toSMT(r))
+ case fb @ FiniteBag(elems, base) =>
+ declareSort(fb.getType)
+
+ toSMT(RawArrayValue(base, elems, InfiniteIntegerLiteral(0)))
+
+ case BagAdd(b, e) =>
+ val bid = FreshIdentifier("b", b.getType, true)
+ val eid = FreshIdentifier("e", e.getType, true)
+ val (bSym, eSym) = (id2sym(bid), id2sym(eid))
+ SMTLet(VarBinding(bSym, toSMT(b)), Seq(VarBinding(eSym, toSMT(e))), ArraysEx.Store(bSym, eSym,
+ Ints.Add(ArraysEx.Select(bSym, eSym), Ints.NumeralLit(1))))
+
+ case MultiplicityInBag(e, b) =>
+ ArraysEx.Select(toSMT(b), toSMT(e))
+
+ case BagUnion(b1, b2) =>
+ val plus = SortedSymbol("+", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
+ ArrayMap(plus, toSMT(b1), toSMT(b2))
+
+ case BagIntersection(b1, b2) =>
+ val abs = SortedSymbol("abs", List(IntegerType).map(declareSort), declareSort(IntegerType))
+ val plus = SortedSymbol("+", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
+ val minus = SortedSymbol("-", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
+ val div = SortedSymbol("/", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
+
+ val did = FreshIdentifier("d", b1.getType, true)
+ val dSym = id2sym(did)
+
+ val all2 = ArrayConst(declareSort(IntegerType), Ints.NumeralLit(2))
+
+ SMTLet(VarBinding(dSym, ArrayMap(minus, toSMT(b1), toSMT(b2))), Seq(),
+ ArrayMap(div, ArrayMap(plus, dSym, ArrayMap(abs, dSym)), all2))
+
case _ =>
super.toSMT(e)
}
@@ -159,8 +198,16 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
throw LeonFatalError("Unable to extract "+s)
}
+ protected object SortedSymbol {
+ def apply(op: String, from: List[Sort], to: Sort) = {
+ def simpleSort(s: Sort): Boolean = s.subSorts.isEmpty && !s.id.isIndexed
+ assert(from.forall(simpleSort) && simpleSort(to), "SortedSymbol is only defined for simple sorts")
+ SList(SSymbol(op), SList(from.map(_.id.symbol): _*), to.id.symbol)
+ }
+ }
+
protected object ArrayMap {
- def apply(op: SSymbol, arrs: Term*) = {
+ def apply(op: SExpr, arrs: Term*) = {
FunctionApplication(
QualifiedIdentifier(SMTIdentifier(SSymbol("map"), List(op))),
arrs
diff --git a/src/main/scala/leon/solvers/theories/BagEncoder.scala b/src/main/scala/leon/solvers/theories/BagEncoder.scala
index 4ba7fcaa42307ae9c1b65bd3b81c4da03ab62b22..2ae7f2ac8a59b0cc2e96a2cec06b22d1983b79da 100644
--- a/src/main/scala/leon/solvers/theories/BagEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/BagEncoder.scala
@@ -6,9 +6,113 @@ package theories
import purescala.Common._
import purescala.Expressions._
+import purescala.Definitions._
import purescala.Types._
-class BagEncoder(val context: LeonContext) extends TheoryEncoder {
- val encoder = new Encoder
- val decoder = new Decoder
+class BagEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
+ val Bag = p.library.lookupUnique[CaseClassDef]("leon.theories.Bag")
+
+ val Get = p.library.lookupUnique[FunDef]("leon.theories.Bag.get")
+ val Add = p.library.lookupUnique[FunDef]("leon.theories.Bag.add")
+ val Union = p.library.lookupUnique[FunDef]("leon.theories.Bag.union")
+ val Difference = p.library.lookupUnique[FunDef]("leon.theories.Bag.difference")
+ val Intersect = p.library.lookupUnique[FunDef]("leon.theories.Bag.intersect")
+ val BagEquals = p.library.lookupUnique[FunDef]("leon.theories.Bag.equals")
+
+ val encoder = new Encoder {
+ override def transform(e: Expr)(implicit binders: Map[Identifier, Identifier]): Expr = e match {
+ case FiniteBag(elems, tpe) =>
+ val newTpe = transform(tpe)
+ val id = FreshIdentifier("x", newTpe, true)
+ CaseClass(Bag.typed(Seq(newTpe)), Seq(Lambda(Seq(ValDef(id)),
+ elems.foldRight[Expr](InfiniteIntegerLiteral(0).copiedFrom(e)) { case ((k, v), ite) =>
+ IfExpr(Equals(Variable(id), transform(k)), transform(v), ite).copiedFrom(e)
+ }))).copiedFrom(e)
+
+ case BagAdd(bag, elem) =>
+ val BagType(base) = bag.getType
+ FunctionInvocation(Add.typed(Seq(transform(base))), Seq(transform(bag), transform(elem))).copiedFrom(e)
+
+ case MultiplicityInBag(elem, bag) =>
+ val BagType(base) = bag.getType
+ FunctionInvocation(Get.typed(Seq(transform(base))), Seq(transform(bag), transform(elem))).copiedFrom(e)
+
+ case BagIntersection(b1, b2) =>
+ val BagType(base) = b1.getType
+ FunctionInvocation(Intersect.typed(Seq(transform(base))), Seq(transform(b1), transform(b2))).copiedFrom(e)
+
+ case BagUnion(b1, b2) =>
+ val BagType(base) = b1.getType
+ FunctionInvocation(Union.typed(Seq(transform(base))), Seq(transform(b1), transform(b2))).copiedFrom(e)
+
+ case BagDifference(b1, b2) =>
+ val BagType(base) = b1.getType
+ FunctionInvocation(Difference.typed(Seq(transform(base))), Seq(transform(b1), transform(b2))).copiedFrom(e)
+
+ case Equals(b1, b2) if b1.getType.isInstanceOf[BagType] =>
+ val BagType(base) = b1.getType
+ FunctionInvocation(BagEquals.typed(Seq(transform(base))), Seq(transform(b1), transform(b2))).copiedFrom(e)
+
+ case _ => super.transform(e)
+ }
+
+ override def transform(tpe: TypeTree): TypeTree = tpe match {
+ case BagType(base) => Bag.typed(Seq(transform(base))).copiedFrom(tpe)
+ case _ => super.transform(tpe)
+ }
+ }
+
+ val decoder = new Decoder {
+ override def transform(e: Expr)(implicit binders: Map[Identifier, Identifier]): Expr = e match {
+ case cc @ CaseClass(CaseClassType(Bag, Seq(tpe)), args) =>
+ FiniteBag(args(0) match {
+ case FiniteLambda(mapping, dflt, tpe) =>
+ if (dflt != InfiniteIntegerLiteral(0))
+ throw new Unsupported(cc, "Bags can't have default value " + dflt.asString(ctx))(ctx)
+ mapping.map { case (ks, v) => transform(ks.head) -> transform(v) }.toMap
+
+ case Lambda(Seq(ValDef(id)), body) =>
+ def rec(expr: Expr): Map[Expr, Expr] = expr match {
+ case IfExpr(Equals(`id`, k), v, elze) => rec(elze) + (transform(k) -> transform(v))
+ case InfiniteIntegerLiteral(v) if v == 0 => Map.empty
+ case _ => throw new Unsupported(expr, "Bags can't have default value " + expr.asString(ctx))(ctx)
+ }
+
+ rec(body)
+
+ case f => scala.sys.error("Unexpected function " + f.asString(ctx))
+ }, transform(tpe)).copiedFrom(e)
+
+ case FunctionInvocation(TypedFunDef(Add, Seq(_)), Seq(bag, elem)) =>
+ BagAdd(transform(bag), transform(elem)).copiedFrom(e)
+
+ case FunctionInvocation(TypedFunDef(Get, Seq(_)), Seq(bag, elem)) =>
+ MultiplicityInBag(transform(elem), transform(bag)).copiedFrom(e)
+
+ case FunctionInvocation(TypedFunDef(Intersect, Seq(_)), Seq(b1, b2)) =>
+ BagIntersection(transform(b1), transform(b2)).copiedFrom(e)
+
+ case FunctionInvocation(TypedFunDef(Union, Seq(_)), Seq(b1, b2)) =>
+ BagUnion(transform(b1), transform(b2)).copiedFrom(e)
+
+ case FunctionInvocation(TypedFunDef(Difference, Seq(_)), Seq(b1, b2)) =>
+ BagDifference(transform(b1), transform(b2)).copiedFrom(e)
+
+ case FunctionInvocation(TypedFunDef(BagEquals, Seq(_)), Seq(b1, b2)) =>
+ Equals(transform(b1), transform(b2)).copiedFrom(e)
+
+ case _ => super.transform(e)
+ }
+
+ override def transform(tpe: TypeTree): TypeTree = tpe match {
+ case CaseClassType(Bag, Seq(base)) => BagType(transform(base)).copiedFrom(tpe)
+ case _ => super.transform(tpe)
+ }
+
+ override def transform(pat: Pattern): (Pattern, Map[Identifier, Identifier]) = pat match {
+ case CaseClassPattern(b, CaseClassType(Bag, Seq(tpe)), Seq(sub)) =>
+ throw new Unsupported(pat, "Can't translate Bag case class pattern")(ctx)
+ case _ => super.transform(pat)
+ }
+ }
}
diff --git a/src/main/scala/leon/solvers/theories/StringEncoder.scala b/src/main/scala/leon/solvers/theories/StringEncoder.scala
index 8f33513a64898c17a7a4b2dfda13a037b2d93f5d..5af13c1c0e52e29d3f79654a6cbe30f009630d5d 100644
--- a/src/main/scala/leon/solvers/theories/StringEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/StringEncoder.scala
@@ -10,114 +10,18 @@ import purescala.Constructors._
import purescala.Types._
import purescala.Definitions._
import leon.utils.Bijection
-import leon.purescala.DefOps
import leon.purescala.TypeOps
-import leon.purescala.Extractors.Operator
-import leon.evaluators.EvaluationResults
-object StringEcoSystem {
- private def withIdentifier[T](name: String, tpe: TypeTree = Untyped)(f: Identifier => T): T = {
- val id = FreshIdentifier(name, tpe)
- f(id)
- }
-
- private def withIdentifiers[T](name: String, tpe: TypeTree, name2: String, tpe2: TypeTree = Untyped)(f: (Identifier, Identifier) => T): T = {
- withIdentifier(name, tpe)(id => withIdentifier(name2, tpe2)(id2 => f(id, id2)))
- }
-
- val StringList = new AbstractClassDef(FreshIdentifier("StringList"), Seq(), None)
- val StringListTyped = StringList.typed
- val StringCons = withIdentifiers("head", CharType, "tail", StringListTyped){ (head, tail) =>
- val d = new CaseClassDef(FreshIdentifier("StringCons"), Seq(), Some(StringListTyped), false)
- d.setFields(Seq(ValDef(head), ValDef(tail)))
- d
- }
-
- StringList.registerChild(StringCons)
- val StringConsTyped = StringCons.typed
- val StringNil = new CaseClassDef(FreshIdentifier("StringNil"), Seq(), Some(StringListTyped), false)
- val StringNilTyped = StringNil.typed
- StringList.registerChild(StringNil)
-
- val StringSize = withIdentifiers("l", StringListTyped, "StringSize"){ (lengthArg, id) =>
- val fd = new FunDef(id, Seq(), Seq(ValDef(lengthArg)), IntegerType)
- fd.body = Some(withIdentifiers("h", CharType, "t", StringListTyped){ (h, t) =>
- MatchExpr(Variable(lengthArg), Seq(
- MatchCase(CaseClassPattern(None, StringNilTyped, Seq()), None, InfiniteIntegerLiteral(BigInt(0))),
- MatchCase(CaseClassPattern(None, StringConsTyped, Seq(WildcardPattern(Some(h)), WildcardPattern(Some(t)))), None,
- Plus(InfiniteIntegerLiteral(BigInt(1)), FunctionInvocation(fd.typed, Seq(Variable(t)))))
- ))
- })
- fd
- }
-
- val StringListConcat = withIdentifiers("x", StringListTyped, "y", StringListTyped) { (x, y) =>
- val fd = new FunDef(FreshIdentifier("StringListConcat"), Seq(), Seq(ValDef(x), ValDef(y)), StringListTyped)
- fd.body = Some(
- withIdentifiers("h", CharType, "t", StringListTyped){ (h, t) =>
- MatchExpr(Variable(x), Seq(
- MatchCase(CaseClassPattern(None, StringNilTyped, Seq()), None, Variable(y)),
- MatchCase(CaseClassPattern(None, StringConsTyped, Seq(WildcardPattern(Some(h)), WildcardPattern(Some(t)))), None,
- CaseClass(StringConsTyped, Seq(Variable(h), FunctionInvocation(fd.typed, Seq(Variable(t), Variable(y)))))
- )))
- }
- )
- fd
- }
-
- val StringTake = withIdentifiers("tt", StringListTyped, "it", StringListTyped) { (tt, it) =>
- val fd = new FunDef(FreshIdentifier("StringTake"), Seq(), Seq(ValDef(tt), ValDef(it)), StringListTyped)
- fd.body = Some{
- withIdentifiers("h", CharType, "t", StringListTyped) { (h, t) =>
- withIdentifier("i", IntegerType){ i =>
- MatchExpr(Tuple(Seq(Variable(tt), Variable(it))), Seq(
- MatchCase(TuplePattern(None, Seq(CaseClassPattern(None, StringNilTyped, Seq()), WildcardPattern(None))), None,
- InfiniteIntegerLiteral(BigInt(0))),
- MatchCase(TuplePattern(None, Seq(CaseClassPattern(None, StringConsTyped, Seq(WildcardPattern(Some(h)), WildcardPattern(Some(t)))), WildcardPattern(Some(i)))), None,
- IfExpr(LessThan(Variable(i), InfiniteIntegerLiteral(BigInt(0))),
- CaseClass(StringNilTyped, Seq()),
- CaseClass(StringConsTyped, Seq(Variable(h),
- FunctionInvocation(fd.typed, Seq(Variable(t), Minus(Variable(i), InfiniteIntegerLiteral(BigInt(1)))))))
- ))))
- }
- }
- }
- fd
- }
-
- val StringDrop = withIdentifiers("td", StringListTyped, "id", IntegerType) { (td, id) =>
- val fd = new FunDef(FreshIdentifier("StringDrop"), Seq(), Seq(ValDef(td), ValDef(id)), StringListTyped)
- fd.body = Some(
- withIdentifiers("h", CharType, "t", StringListTyped) { (h, t) =>
- withIdentifier("i", IntegerType){ i =>
- MatchExpr(Tuple(Seq(Variable(td), Variable(id))), Seq(
- MatchCase(TuplePattern(None, Seq(CaseClassPattern(None, StringNilTyped, Seq()), WildcardPattern(None))), None,
- InfiniteIntegerLiteral(BigInt(0))),
- MatchCase(TuplePattern(None, Seq(CaseClassPattern(None, StringConsTyped, Seq(WildcardPattern(Some(h)), WildcardPattern(Some(t)))), WildcardPattern(Some(i)))), None,
- IfExpr(LessThan(Variable(i), InfiniteIntegerLiteral(BigInt(0))),
- CaseClass(StringConsTyped, Seq(Variable(h), Variable(t))),
- FunctionInvocation(fd.typed, Seq(Variable(t), Minus(Variable(i), InfiniteIntegerLiteral(BigInt(1)))))
- ))))
- }}
- )
- fd
- }
-
- val StringSlice = withIdentifier("s", StringListTyped) { s => withIdentifiers("from", IntegerType, "to", IntegerType) { (from, to) =>
- val fd = new FunDef(FreshIdentifier("StringSlice"), Seq(), Seq(ValDef(s), ValDef(from), ValDef(to)), StringListTyped)
- fd.body = Some(
- FunctionInvocation(StringTake.typed,
- Seq(FunctionInvocation(StringDrop.typed, Seq(Variable(s), Variable(from))),
- Minus(Variable(to), Variable(from)))))
- fd
- } }
-
- val classDefs = Seq(StringList, StringCons, StringNil)
- val funDefs = Seq(StringSize, StringListConcat, StringTake, StringDrop, StringSlice)
-}
+class StringEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
+ val String = p.library.lookupUnique[ClassDef]("leon.theories.String").typed
+ val StringCons = p.library.lookupUnique[CaseClassDef]("leon.theories.StringCons").typed
+ val StringNil = p.library.lookupUnique[CaseClassDef]("leon.theories.StringNil").typed
-class StringEncoder extends TheoryEncoder {
- import StringEcoSystem._
+ val Size = p.library.lookupUnique[FunDef]("leon.theories.String.size").typed
+ val Take = p.library.lookupUnique[FunDef]("leon.theories.String.take").typed
+ val Drop = p.library.lookupUnique[FunDef]("leon.theories.String.drop").typed
+ val Slice = p.library.lookupUnique[FunDef]("leon.theories.String.slice").typed
+ val Concat = p.library.lookupUnique[FunDef]("leon.theories.String.concat").typed
private val stringBijection = new Bijection[String, Expr]()
@@ -127,8 +31,8 @@ class StringEncoder extends TheoryEncoder {
})
private def convertFromString(v: String): Expr = stringBijection.cachedB(v) {
- v.toList.foldRight(CaseClass(StringNilTyped, Seq())){
- case (char, l) => CaseClass(StringConsTyped, Seq(CharLiteral(char), l))
+ v.toList.foldRight(CaseClass(StringNil, Seq())){
+ case (char, l) => CaseClass(StringCons, Seq(CharLiteral(char), l))
}
}
@@ -137,26 +41,26 @@ class StringEncoder extends TheoryEncoder {
case StringLiteral(v) =>
convertFromString(v)
case StringLength(a) =>
- FunctionInvocation(StringSize.typed, Seq(transform(a))).copiedFrom(e)
+ FunctionInvocation(Size, Seq(transform(a))).copiedFrom(e)
case StringConcat(a, b) =>
- FunctionInvocation(StringListConcat.typed, Seq(transform(a), transform(b))).copiedFrom(e)
+ FunctionInvocation(Concat, Seq(transform(a), transform(b))).copiedFrom(e)
case SubString(a, start, Plus(start2, length)) if start == start2 =>
- FunctionInvocation(StringTake.typed, Seq(FunctionInvocation(StringDrop.typed, Seq(transform(a), transform(start))), transform(length))).copiedFrom(e)
+ FunctionInvocation(Take, Seq(FunctionInvocation(Drop, Seq(transform(a), transform(start))), transform(length))).copiedFrom(e)
case SubString(a, start, end) =>
- FunctionInvocation(StringSlice.typed, Seq(transform(a), transform(start), transform(end))).copiedFrom(e)
+ FunctionInvocation(Slice, Seq(transform(a), transform(start), transform(end))).copiedFrom(e)
case _ => super.transform(e)
}
override def transform(tpe: TypeTree): TypeTree = tpe match {
- case StringType => StringListTyped
+ case StringType => String
case _ => super.transform(tpe)
}
override def transform(pat: Pattern): (Pattern, Map[Identifier, Identifier]) = pat match {
case LiteralPattern(binder, StringLiteral(s)) =>
val newBinder = binder map transform
- val newPattern = s.foldRight(CaseClassPattern(None, StringNilTyped, Seq())) {
- case (elem, pattern) => CaseClassPattern(None, StringConsTyped, Seq(LiteralPattern(None, CharLiteral(elem)), pattern))
+ val newPattern = s.foldRight(CaseClassPattern(None, StringNil, Seq())) {
+ case (elem, pattern) => CaseClassPattern(None, StringCons, Seq(LiteralPattern(None, CharLiteral(elem)), pattern))
}
(newPattern.copy(binder = newBinder), (binder zip newBinder).filter(p => p._1 != p._2).toMap)
case _ => super.transform(pat)
@@ -165,35 +69,42 @@ class StringEncoder extends TheoryEncoder {
val decoder = new Decoder {
override def transform(e: Expr)(implicit binders: Map[Identifier, Identifier]): Expr = e match {
- case cc @ CaseClass(cct, args) if TypeOps.isSubtypeOf(cct, StringListTyped)=>
+ case cc @ CaseClass(cct, args) if TypeOps.isSubtypeOf(cct, String)=>
StringLiteral(convertToString(cc)).copiedFrom(cc)
- case FunctionInvocation(StringSize, Seq(a)) =>
+ case FunctionInvocation(Size, Seq(a)) =>
StringLength(transform(a)).copiedFrom(e)
- case FunctionInvocation(StringListConcat, Seq(a, b)) =>
+ case FunctionInvocation(Concat, Seq(a, b)) =>
StringConcat(transform(a), transform(b)).copiedFrom(e)
- case FunctionInvocation(StringTake, Seq(FunctionInvocation(StringDrop, Seq(a, start)), length)) =>
+ case FunctionInvocation(Slice, Seq(a, from, to)) =>
+ SubString(transform(a), transform(from), transform(to)).copiedFrom(e)
+ case FunctionInvocation(Take, Seq(FunctionInvocation(Drop, Seq(a, start)), length)) =>
val rstart = transform(start)
SubString(transform(a), rstart, plus(rstart, transform(length))).copiedFrom(e)
+ case FunctionInvocation(Take, Seq(a, length)) =>
+ SubString(transform(a), InfiniteIntegerLiteral(0), transform(length)).copiedFrom(e)
+ case FunctionInvocation(Drop, Seq(a, count)) =>
+ val ra = transform(a)
+ SubString(ra, transform(count), StringLength(ra)).copiedFrom(e)
case _ => super.transform(e)
}
override def transform(tpe: TypeTree): TypeTree = tpe match {
- case StringListTyped | StringConsTyped | StringNilTyped => StringType
+ case String | StringCons | StringNil => StringType
case _ => super.transform(tpe)
}
override def transform(pat: Pattern): (Pattern, Map[Identifier, Identifier]) = pat match {
- case CaseClassPattern(b, StringNilTyped, Seq()) =>
+ case CaseClassPattern(b, StringNil, Seq()) =>
val newBinder = b map transform
(LiteralPattern(newBinder , StringLiteral("")), (b zip newBinder).filter(p => p._1 != p._2).toMap)
- case CaseClassPattern(b, StringConsTyped, Seq(LiteralPattern(_, CharLiteral(elem)), sub)) => transform(sub) match {
+ case CaseClassPattern(b, StringCons, Seq(LiteralPattern(_, CharLiteral(elem)), sub)) => transform(sub) match {
case (LiteralPattern(_, StringLiteral(s)), binders) =>
val newBinder = b map transform
(LiteralPattern(newBinder, StringLiteral(elem + s)), (b zip newBinder).filter(p => p._1 != p._2).toMap ++ binders)
case (e, binders) =>
- (LiteralPattern(None, StringLiteral("Failed to parse pattern back as string:" + e)), binders)
+ throw new Unsupported(pat, "Failed to parse pattern back as string: " + e)(ctx)
}
case _ => super.transform(pat)
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 852e125ed88db4327b18cfabc329d31e1366a2f6..403fb08fd20c9297b91cd6294cfc4a707e7ad40a 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -172,8 +172,12 @@ trait AbstractUnrollingSolver[T]
trait ModelWrapper {
def modelEval(elem: T, tpe: TypeTree): Option[Expr]
- def eval(elem: T, tpe: TypeTree): Option[Expr] = modelEval(elem, theoryEncoder.encode(tpe)).map {
- expr => theoryEncoder.decode(expr)(Map.empty)
+ def eval(elem: T, tpe: TypeTree): Option[Expr] = modelEval(elem, theoryEncoder.encode(tpe)).flatMap {
+ expr => try {
+ Some(theoryEncoder.decode(expr)(Map.empty))
+ } catch {
+ case u: Unsupported => None
+ }
}
def get(id: Identifier): Option[Expr] = eval(freeVars(id), theoryEncoder.encode(id.getType)).filter {
@@ -259,7 +263,9 @@ trait AbstractUnrollingSolver[T]
var quantify = false
def check[R](clauses: Seq[T])(block: Option[Boolean] => R) =
- if (partialModels) solverCheckAssumptions(clauses)(block) else solverCheck(clauses)(block)
+ if (partialModels || templateGenerator.manager.quantifications.isEmpty)
+ solverCheckAssumptions(clauses)(block)
+ else solverCheck(clauses)(block)
val timer = context.timers.solvers.check.start()
check(encodedAssumptions.toSeq ++ unrollingBank.satisfactionAssumptions) { res =>
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index f8237a4885fdc459efe261bb4333afc36944b500..abf4c63d3d2c019a3a33e62fee88a5d663c4d1e8 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -103,7 +103,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
def asString(implicit ctx: LeonContext) = z3.toString
}
- val theoryEncoder = new StringEncoder
+ val theoryEncoder = new StringEncoder(context, program) >> new BagEncoder(context, program)
val templateEncoder = new TemplateEncoder[Z3AST] {
def encodeId(id: Identifier): Z3AST = {
diff --git a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
index 99c75199a7d96b64ce42ba9039dd648032e60888..a1ed39dfe442044be38be88dac287cfd34aca391 100644
--- a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
@@ -10,4 +10,4 @@ import unrolling._
import theories._
class Z3UnrollingSolver(context: LeonContext, program: Program, underlying: Solver)
- extends UnrollingSolver(context, program, underlying, theories = new StringEncoder)
+ extends UnrollingSolver(context, program, underlying, new StringEncoder(context, program))
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 77b15659c3e2e7be97d36d9e5645af5daf9cfb58..daab94567d4ef6cb27f79d074ab58ea37d10a0b3 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -33,7 +33,7 @@ final case class Chain(relations: List[Relation]) {
def rec(list: List[Relation], funDef: TypedFunDef, args: Seq[Expr]): Seq[(Seq[ValDef], Expr)] = list match {
case Relation(_, _, fi @ FunctionInvocation(fitfd, nextArgs), _) :: xs =>
val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
- val subst = tfd.paramSubst(args)
+ val subst = funDef.paramSubst(args)
val expr = replaceFromIDs(subst, hoistIte(expandLets(matchToIfThenElse(tfd.body.get))))
val mappedArgs = nextArgs.map(e => replaceFromIDs(subst, tfd.translated(e)))
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index e075c374e8d4796680c940f3cf6e4d3ec455df79..e4b7d42139f5a921c23012c202c7d877422b1803 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -78,21 +78,25 @@ trait StructuralSize {
}).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus)
case IntegerType =>
FunctionInvocation(typedAbsBigIntFun, Seq(expr))
+/*
+ case Int32Type =>
+ FunctionInvocation(typedAbsIntFun, Seq(expr))
+*/
case _ => InfiniteIntegerLiteral(0)
}
}
def lexicographicDecreasing(s1: Seq[Expr], s2: Seq[Expr], strict: Boolean, sizeOfOneExpr: Expr => Expr): Expr = {
// Note: The Equal and GreaterThan ASTs work for both BigInt and Bitvector
-
+
val sameSizeExprs = for ((arg1, arg2) <- s1 zip s2) yield Equals(sizeOfOneExpr(arg1), sizeOfOneExpr(arg2))
-
+
val greaterBecauseGreaterAtFirstDifferentPos =
orJoin(for (firstDifferent <- 0 until scala.math.min(s1.length, s2.length)) yield and(
andJoin(sameSizeExprs.take(firstDifferent)),
GreaterThan(sizeOfOneExpr(s1(firstDifferent)), sizeOfOneExpr(s2(firstDifferent)))
))
-
+
if (s1.length > s2.length || (s1.length == s2.length && !strict)) {
or(andJoin(sameSizeExprs), greaterBecauseGreaterAtFirstDifferentPos)
} else {
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 18dc12938bd2dd55ff51e568e5af4bcd79cd245a..6bff50527120342bd5610c7e3ba9576a4bf2af95 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -7,6 +7,8 @@ import purescala.Definitions._
import purescala.Types._
import purescala.DefOps._
+import scala.reflect._
+
case class Library(pgm: Program) {
lazy val List = lookup("leon.collection.List").collectFirst { case acd : AbstractClassDef => acd }
lazy val Cons = lookup("leon.collection.Cons").collectFirst { case ccd : CaseClassDef => ccd }
@@ -28,6 +30,13 @@ case class Library(pgm: Program) {
pgm.lookupAll(name)
}
+ def lookupUnique[D <: Definition : ClassTag](name: String): D = {
+ val ct = classTag[D]
+ val all = pgm.lookupAll(name).filter(d => ct.runtimeClass.isInstance(d))
+ assert(all.size == 1, "lookupUnique(\"name\") returned results " + all.map(_.id.uniqueName))
+ all.head.asInstanceOf[D]
+ }
+
def optionType(tp: TypeTree) = AbstractClassType(Option.get, Seq(tp))
def someType(tp: TypeTree) = CaseClassType(Some.get, Seq(tp))
def noneType(tp: TypeTree) = CaseClassType(None.get, Seq(tp))
diff --git a/src/test/resources/regression/verification/purescala/valid/MergeSort2.scala b/src/test/resources/regression/verification/purescala/valid/MergeSort2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0bd0ab35ecaef991f618c0938f8446051eabf00e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MergeSort2.scala
@@ -0,0 +1,43 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.collection._
+import leon.lang._
+
+object MergeSort2 {
+
+ def bag[T](list: List[T]): Bag[T] = list match {
+ case Nil() => Bag.empty[T]
+ case Cons(x, xs) => bag(xs) + x
+ }
+
+ def isSorted(list: List[BigInt]): Boolean = list match {
+ case Cons(x1, tail @ Cons(x2, _)) => x1 <= x2 && isSorted(tail)
+ case _ => true
+ }
+
+ def merge(l1: List[BigInt], l2: List[BigInt]): List[BigInt] = {
+ require(isSorted(l1) && isSorted(l2))
+
+ (l1, l2) match {
+ case (Cons(x, xs), Cons(y, ys)) =>
+ if (x <= y) Cons(x, merge(xs, l2))
+ else Cons(y, merge(l1, ys))
+ case _ => l1 ++ l2
+ }
+ } ensuring (res => isSorted(res) && bag(res) == bag(l1) ++ bag(l2))
+
+ def split(list: List[BigInt]): (List[BigInt], List[BigInt]) = (list match {
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1, s2) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ case _ => (list, Nil[BigInt]())
+ }) ensuring (res => bag(res._1) ++ bag(res._2) == bag(list))
+
+ def mergeSort(list: List[BigInt]): List[BigInt] = (list match {
+ case Cons(_, Cons(_, _)) =>
+ val (s1, s2) = split(list)
+ merge(mergeSort(s1), mergeSort(s2))
+ case _ => list
+ }) ensuring (res => isSorted(res) && bag(res) == bag(list))
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Nested14.scala b/src/test/resources/regression/verification/purescala/valid/Nested14.scala
index 82f4fd1b965dc06c2458d237c84eb96d23ba8349..39e668aa208f1eeefd8257b359b3b5a5be51b39f 100644
--- a/src/test/resources/regression/verification/purescala/valid/Nested14.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Nested14.scala
@@ -4,7 +4,11 @@ object Nested14 {
def foo(i: Int): Int = {
def rec1(j: Int): Int = {
- def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1)
+ require(j >= 0)
+ def rec2(k: Int): Int = {
+ require(j > 0 || j == k)
+ if(k == 0) 0 else rec1(j-1)
+ }
rec2(j)
}
rec1(3)
diff --git a/src/test/resources/regression/verification/purescala/valid/Nested16.scala b/src/test/resources/regression/verification/purescala/valid/Nested16.scala
new file mode 100644
index 0000000000000000000000000000000000000000..411e4a27f0fb918eba1cd5b8d31131f734d0142b
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Nested16.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+object Nested16 {
+
+ def foo(i: BigInt): BigInt = {
+ def rec1(j: BigInt): BigInt = {
+ require(j >= 0)
+ def rec2(k: BigInt): BigInt = {
+ require(j > 0 || j == k)
+ if(k == 0) 0 else rec1(j-1)
+ }
+ rec2(j)
+ }
+ rec1(3)
+ } ensuring(0 == _)
+
+}
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index 5245c00c2b8147d62217d5d5bcecd89399427efe..bf828a9fb07ae255ad78c7ab71f3e76eb7cee02e 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -49,11 +49,30 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
|
| def finite() : Set[Int] = Set(1, 2, 3)
| def build(x : Int, y : Int, z : Int) : Set[Int] = Set(x, y, z)
+ | def add(s1 : Set[Int], e: Int) : Set[Int] = s1 + e
| def union(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 ++ s2
| def inter(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 & s2
| def diff(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 -- s2
|}""".stripMargin,
+ """|import leon.lang._
+ |object Bags {
+ | sealed abstract class List
+ | case class Nil() extends List
+ | case class Cons(head : Int, tail : List) extends List
+ |
+ | def content(l : List) : Bag[Int] = l match {
+ | case Nil() => Bag.empty[Int]
+ | case Cons(x, xs) => content(xs) + x
+ | }
+ |
+ | def finite() : Bag[Int] = Bag((1, 1), (2, 2), (3, 3))
+ | def add(s1 : Bag[Int], e: Int) : Bag[Int] = s1 + e
+ | def union(s1 : Bag[Int], s2 : Bag[Int]) : Bag[Int] = s1 ++ s2
+ | def inter(s1 : Bag[Int], s2 : Bag[Int]) : Bag[Int] = s1 & s2
+ | def diff(s1 : Bag[Int], s2 : Bag[Int]) : Bag[Int] = s1 -- s2
+ |}""".stripMargin,
+
"""|import leon.lang._
|object Maps {
| sealed abstract class PList
@@ -295,6 +314,8 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
eval(e, fcall("Sets.content")(cons12)) === s12
eval(e, fcall("Sets.build")(i(1), i(2), i(3))) === s123
eval(e, fcall("Sets.build")(i(1), i(2), i(2))) === s12
+ eval(e, fcall("Sets.add")(s12, i(2))) === s12
+ eval(e, fcall("Sets.add")(s12, i(3))) === s123
eval(e, fcall("Sets.union")(s123, s246)) === s12346
eval(e, fcall("Sets.union")(s246, s123)) === s12346
eval(e, fcall("Sets.inter")(s123, s246)) === s2
@@ -308,6 +329,39 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
}
}
+ test("Bags") { implicit fix =>
+ val nil = cc("Bags.Nil")()
+ def cons(es: Expr*) = cc("Bags.Cons")(es: _*)
+
+ val cons12 = cons(i(1), cons(i(2), nil))
+ val cons122 = cons(i(1), cons(i(2), cons(i(2), nil)))
+
+ def fb(is: (Int, Int)*) = FiniteBag(is.map(p => i(p._1) -> bi(p._2)).toMap, Int32Type)
+
+ val b12 = fb(1 -> 1, 2 -> 1)
+ val b123 = fb(1 -> 1, 2 -> 1, 3 -> 1)
+ val b246 = fb(2 -> 1, 4 -> 1, 6 -> 1)
+ val b1223 = fb(1 -> 1, 2 -> 2, 3 -> 1)
+
+ for(e <- allEvaluators) {
+ eval(e, fcall("Bags.finite")()) === fb(1 -> 1, 2 -> 2, 3 -> 3)
+ eval(e, fcall("Bags.content")(nil)) === fb()
+ eval(e, fcall("Bags.content")(cons12)) === fb(1 -> 1, 2 -> 1)
+ eval(e, fcall("Bags.content")(cons122)) === fb(1 -> 1, 2 -> 2)
+ eval(e, fcall("Bags.add")(b12, i(2))) === fb(1 -> 1, 2 -> 2)
+ eval(e, fcall("Bags.add")(b12, i(3))) === fb(1 -> 1, 2 -> 1, 3 -> 1)
+ eval(e, fcall("Bags.union")(b123, b246)) === fb(1 -> 1, 2 -> 2, 3 -> 1, 4 -> 1, 6 -> 1)
+ eval(e, fcall("Bags.union")(b246, b123)) === fb(1 -> 1, 2 -> 2, 3 -> 1, 4 -> 1, 6 -> 1)
+ eval(e, fcall("Bags.inter")(b123, b246)) === fb(2 -> 1)
+ eval(e, fcall("Bags.inter")(b246, b123)) === fb(2 -> 1)
+ eval(e, fcall("Bags.inter")(b1223, b123)) === b123
+ eval(e, fcall("Bags.diff")(b123, b246)) === fb(1 -> 1, 3 -> 1)
+ eval(e, fcall("Bags.diff")(b246, b123)) === fb(4 -> 1, 6 -> 1)
+ eval(e, fcall("Bags.diff")(b1223, b123)) === fb(2 -> 1)
+ eval(e, fcall("Bags.diff")(b123, b1223)) === fb()
+ }
+ }
+
test("Maps") { implicit fix =>
val cons1223 = cc("Maps.PCons")(i(1), i(2), cc("Maps.PCons")(i(2), i(3), cc("Maps.PNil")()))
diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala
index 8b0d8026e1540a170df577b3952140e4ef8fa910..f47f3c9b9e58f9eb44c601716d363cbeedc6b3d3 100644
--- a/src/test/scala/leon/integration/solvers/SolversSuite.scala
+++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala
@@ -41,6 +41,7 @@ class SolversSuite extends LeonTestSuiteWithProgram {
StringType,
TypeParameter.fresh("T"),
SetType(IntegerType),
+ BagType(IntegerType),
MapType(IntegerType, IntegerType),
FunctionType(Seq(IntegerType), IntegerType),
TupleType(Seq(IntegerType, BooleanType, Int32Type))
@@ -54,6 +55,8 @@ class SolversSuite extends LeonTestSuiteWithProgram {
Equals(v, simplestValue(v.getType))
case SetType(base) =>
Not(ElementOfSet(simplestValue(base), v))
+ case BagType(base) =>
+ Not(Equals(MultiplicityInBag(simplestValue(base), v), simplestValue(IntegerType)))
case MapType(from, to) =>
Not(Equals(MapApply(v, simplestValue(from)), simplestValue(to)))
case FunctionType(froms, to) =>
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 52984ac7a781fd1c8b4e058bbadd094337260f87..876ad77bde182b5fd380300a69b3963929eaee31 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -35,7 +35,8 @@ class TerminationSuite extends LeonRegressionSuite {
val ignored = List(
"termination/valid/NNF.scala",
//"verification/purescala/valid/MergeSort.scala",
- "verification/purescala/valid/Nested14.scala"
+ "verification/purescala/valid/Nested14.scala",
+ "verification/purescala/valid/MergeSort2.scala"
)
val t = if (ignored.exists(displayName.replaceAll("\\\\","/").endsWith)) {