started to rewrite the CADE07 formulas as FunCheck functions. So far they all work :)

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)

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 {

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?")
   }

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 

vmcai2011-testcases/CADE07.scala

+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)
+}