diff --git a/src/main/java/leon/codegen/runtime/Bag.java b/src/main/java/leon/codegen/runtime/Bag.java
index 8276935f780c3bb74b2d1a18213a5121d86dcd85..e7404f522b8170523ff70e2a8e94059d05c1317b 100644
--- a/src/main/java/leon/codegen/runtime/Bag.java
+++ b/src/main/java/leon/codegen/runtime/Bag.java
@@ -2,56 +2,55 @@
package leon.codegen.runtime;
-import java.util.Arrays;
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, Integer> _underlying;
+ private final HashMap<Object, BigInt> _underlying;
- protected final HashMap<Object, Integer> underlying() {
+ protected final HashMap<Object, BigInt> underlying() {
return _underlying;
}
public Bag() {
- _underlying = new HashMap<Object, Integer>();
+ _underlying = new HashMap<Object, BigInt>();
}
- private Bag(HashMap<Object, Integer> u) {
+ private Bag(HashMap<Object, BigInt> u) {
_underlying = u;
}
// Uses mutation! Useful at building time.
public void add(Object e) {
- add(e, 1);
+ add(e, BigInt.ONE);
}
// Uses mutation! Useful at building time.
- private void add(Object e, int count) {
- _underlying.put(e, get(e) + count);
+ public void add(Object e, BigInt count) {
+ _underlying.put(e, get(e).add(count));
}
- public Iterator<java.util.Map.Entry<Object, Integer>> getElements() {
+ public Iterator<java.util.Map.Entry<Object, BigInt>> getElements() {
return _underlying.entrySet().iterator();
}
- public int get(Object element) {
- Integer r = _underlying.get(element);
- if (r == null) return 0;
- else return r.intValue();
+ 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, Integer>(_underlying));
+ 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, Integer>(_underlying));
- for (java.util.Map.Entry<Object, Integer> entry : b.underlying().entrySet()) {
+ 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;
@@ -59,18 +58,19 @@ public final class Bag {
public Bag intersect(Bag b) {
Bag n = new Bag();
- for (java.util.Map.Entry<Object, Integer> entry : _underlying.entrySet()) {
- int m = Math.min(entry.getValue(), b.get(entry.getKey()));
- if (m > 0) n.add(entry.getKey(), m);
+ 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, Integer> entry : _underlying.entrySet()) {
- int m = entry.getValue() - b.get(entry.getKey());
- if (m > 0) n.add(entry.getKey(), m);
+ 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;
}
@@ -82,11 +82,11 @@ public final class Bag {
Bag other = (Bag) that;
for (Object key : _underlying.keySet()) {
- if (get(key) != other.get(key)) return false;
+ if (!get(key).equals(other.get(key))) return false;
}
for (Object key : other.underlying().keySet()) {
- if (get(key) != other.get(key)) return false;
+ if (!get(key).equals(other.get(key))) return false;
}
return true;
@@ -97,7 +97,7 @@ public final class Bag {
StringBuilder sb = new StringBuilder();
sb.append("Bag(");
boolean first = true;
- for (java.util.Map.Entry<Object, Integer> entry : _underlying.entrySet()) {
+ for (java.util.Map.Entry<Object, BigInt> entry : _underlying.entrySet()) {
if(!first) {
sb.append(", ");
first = false;
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/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index d615c4a7e0d2e58420a64097442458ceb006207c..d7a3b12c13c9ebdf55e2217b32022e4901643d54 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -589,7 +589,7 @@ trait CodeGeneration {
ch << DUP
mkBoxedExpr(k, ch)
mkExpr(v, ch)
- ch << InvokeVirtual(BagClass, "add", s"(L$ObjectClass;I)V")
+ ch << InvokeVirtual(BagClass, "add", s"(L$ObjectClass;L$BigIntClass;)V")
}
case BagAdd(b, e) =>
@@ -600,7 +600,7 @@ trait CodeGeneration {
case MultiplicityInBag(e, b) =>
mkExpr(b, ch)
mkBoxedExpr(e, ch)
- ch << InvokeVirtual(BagClass, "get", s"(L$ObjectClass;)I")
+ ch << InvokeVirtual(BagClass, "get", s"(L$ObjectClass;)L$BigIntClass;")
case BagIntersection(b1, b2) =>
mkExpr(b1, ch)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index bde7a7649541ade3c1ea989b4e4a8936e52edb45..366feffafcb9c7b994d6ccefbc1ff2f0269626dd 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -235,7 +235,7 @@ class CompilationUnit(val ctx: LeonContext,
case b @ FiniteBag(els, _) =>
val b = new leon.codegen.runtime.Bag()
for ((k,v) <- els) {
- b.add(valueToJVM(k), valueToJVM(v))
+ b.add(valueToJVM(k), valueToJVM(v).asInstanceOf[leon.codegen.runtime.BigInt])
}
b
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 0c5ad1ac7be71076ff013e43b7f1a6df9b92d846..6e13cb030ad7df32b6a5ec1543e6d2c80915903d 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -112,7 +112,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
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 List(k, i @ InfiniteIntegerLiteral(v)) =>
+ case Seq(k, i @ InfiniteIntegerLiteral(v)) =>
k -> (if (v > 0) i else InfiniteIntegerLiteral(-v + 1))
}.toMap, sub), bt.asString(ctx)+"@"+size)
}
@@ -360,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 cc1acc3bcc8c12883275ce10825d59989062a21d..17b44ea45be7bced78fe23712878977633e17840 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -515,7 +515,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
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(0)
+ case None => InfiniteIntegerLiteral(1)
})), tpe)
case (le, re) => throw EvalError(typeErrorMsg(le, bag.getType))
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/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index dfc48fffed88eadfc3cfb6587819ca2bdce16567..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 {
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")()))