diff --git a/lib/z3.jar b/lib/z3.jar
index 37ffb232df24c3b5aa8e35181a736edf576ed751..e40a8c348760944735605957c8a5d45f5dada7db 100644
Binary files a/lib/z3.jar and b/lib/z3.jar differ
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index b60cab38f4301e87e58f2df860387e67b9ddbd1d..c6caa595e6f44ce2b888f3db449ca08397eafbaf 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -422,7 +422,29 @@ trait CodeExtraction extends Extractors {
throw ImpureCodeEncounteredException(tree)
}
}
- }
+ }
+ case ExSetContains(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => ElementOfSet(rr, rl)
+ case _ => {
+ if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
+ case ExSetSubset(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SubsetOf(rl, rr)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Subset on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
case ExSetMinus(t1,t2) => {
val rl = rec(t1)
val rr = rec(t2)
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 62f4b0dae2882a4ab03d263c45adbf099bcf31b4..110efa6753799a6bab9a14f7fffe9bfdce8bcab6 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -409,6 +409,20 @@ trait Extractors {
case _ => None
}
}
+
+ object ExSetContains {
+ def unapply(tree: Apply) : Option[(Tree,Tree)] = tree match {
+ case Apply(Select(lhs, n), List(rhs)) if (n.toString == "contains") => Some((lhs,rhs))
+ case _ => None
+ }
+ }
+
+ object ExSetSubset {
+ def unapply(tree: Apply) : Option[(Tree,Tree)] = tree match {
+ case Apply(Select(lhs, n), List(rhs)) if (n.toString == "subsetOf") => Some((lhs,rhs))
+ case _ => None
+ }
+ }
object ExSetMinus {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 11daf5ebabc033fad337f7cd894daf7c53525fab..4b82075624e281e3b6b8718fdfade14b8928864d 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -73,7 +73,6 @@ object PrettyPrinter {
case And(exprs) => ppNary(sb, exprs, "(", " \u2227 ", ")", lvl) // \land
case Or(exprs) => ppNary(sb, exprs, "(", " \u2228 ", ")", lvl) // \lor
case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ", lvl) // \neq
- case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
case Iff(l,r) => ppBinary(sb, l, r, " <=> ", lvl)
case Implies(l,r) => ppBinary(sb, l, r, " ==> ", lvl)
case UMinus(expr) => ppUnary(sb, expr, "-(", ")", lvl)
@@ -106,6 +105,10 @@ object PrettyPrinter {
case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", lvl)
case EmptySet(_) => sb.append("\u2205") // Ø
case EmptyMultiset(_) => sb.append("\u2205") // Ø
+ case Not(ElementOfSet(s,e)) => ppBinary(sb, s, e, " \u2209 ", lvl) // \notin
+ case ElementOfSet(s,e) => ppBinary(sb, s, e, " \u2208 ", lvl) // \in
+ case SubsetOf(l,r) => ppBinary(sb, l, r, " \u2286 ", lvl) // \subseteq
+ case Not(SubsetOf(l,r)) => ppBinary(sb, l, r, " \u2288 ", lvl) // \notsubseteq
case SetMin(s) => pp(s, sb, lvl).append(".min")
case SetMax(s) => pp(s, sb, lvl).append(".max")
case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl) // \cup
@@ -181,7 +184,7 @@ object PrettyPrinter {
}
case ResultVariable() => sb.append("#res")
-
+ case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
case _ => sb.append("Expr?")
}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 66fa89e4272ac82f02e0c755277c377699ea7a1c..cafc43db50c49ca75a8e517c37f49bd819778376 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -249,11 +249,15 @@ object Trees {
/* Set expressions */
case class EmptySet(baseType: TypeTree) extends Expr with Terminal
case class FiniteSet(elements: Seq[Expr]) extends Expr
- case class ElementOfSet(element: Expr, set: Expr) extends Expr
+ case class ElementOfSet(element: Expr, set: Expr) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
case class SetCardinality(set: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class SubsetOf(set1: Expr, set2: Expr) extends Expr
+ case class SubsetOf(set1: Expr, set2: Expr) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
case class SetIntersection(set1: Expr, set2: Expr) extends Expr
case class SetUnion(set1: Expr, set2: Expr) extends Expr
case class SetDifference(set1: Expr, set2: Expr) extends Expr
diff --git a/vmcai2011-testcases/CADE07.scala b/vmcai2011-testcases/CADE07.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1453c45340aaa6f1b890dd43611e9272958a704b
--- /dev/null
+++ b/vmcai2011-testcases/CADE07.scala
@@ -0,0 +1,72 @@
+import scala.collection.immutable.Set
+
+object CADE07 {
+ def vc1(listContent: Set[Int]) : Boolean = {
+ (listContent.size == 0) == (listContent == Set.empty[Int])
+ } ensuring(_ == true)
+
+ def vc2(x: Int, listContent: Set[Int]) : Set[Int] = {
+ require(!listContent.contains(x))
+ listContent ++ Set(x)
+ } // ensuring(_.size == listContent.size + 1)
+
+ def vc2r(x: Set[Int], listContent: Set[Int]) : Set[Int] = {
+ require(x.size == 1 && !x.subsetOf(listContent))
+ listContent ++ x
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc2a(listRoot: Int, list: Set[Int], x: Int, listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ list.contains(listRoot)
+ && !listContent.contains(x)
+ && listContent.subsetOf(objectAlloc)
+ && objct.contains(x)
+ && objectAlloc.contains(x))
+
+ listContent ++ Set(x)
+ } // ensuring(_.size == listContent.size + 1)
+
+ def vc2ar(listRoot: Set[Int], list: Set[Int], x: Set[Int], listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ listRoot.size == 1
+ && listRoot.subsetOf(list)
+ && x.size == 1
+ && !x.subsetOf(listContent)
+ && listContent.subsetOf(objectAlloc)
+ && x.subsetOf(objct)
+ && x.subsetOf(objectAlloc))
+
+ listContent ++ x
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc2b(listRoot: Int, list: Set[Int], x: Int, listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ list.contains(listRoot)
+ && listContent.subsetOf(objectAlloc)
+ && objct.contains(x)
+ && objectAlloc.contains(x))
+
+ listContent ++ Set(x)
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc2br(listRoot: Set[Int], list: Set[Int], x: Set[Int], listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ listRoot.size == 1
+ && listRoot.subsetOf(list)
+ && x.size == 1
+ && listContent.subsetOf(objectAlloc)
+ && x.subsetOf(objct)
+ && x.subsetOf(objectAlloc))
+
+ listContent ++ x
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc3(x: Int, listContent: Set[Int]) : Set[Int] = {
+ listContent ++ Set(x)
+ } //ensuring(_.size <= listContent.size + 1)
+
+ def vc3r(x: Set[Int], listContent: Set[Int]) : Set[Int] = {
+ require(x.size == 1)
+ listContent ++ x
+ } ensuring(_.size <= listContent.size + 1)
+}