From bea947055cbd2db3783465595ae77691612ed1d1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 9 Jan 2013 11:20:02 +0100
Subject: [PATCH] Add List-related benchmarks, with various invariants (none,
 isSorted, isStrictlySorted), with common operations

---
 testcases/synthesis/cav2013/List.scala        | 45 +++++-------------
 testcases/synthesis/cav2013/SortedList.scala  | 45 ++++++++++++++++++
 .../cav2013/StrictlySortedList.scala          | 47 +++++++++++++++++++
 3 files changed, 103 insertions(+), 34 deletions(-)
 create mode 100644 testcases/synthesis/cav2013/SortedList.scala
 create mode 100644 testcases/synthesis/cav2013/StrictlySortedList.scala

diff --git a/testcases/synthesis/cav2013/List.scala b/testcases/synthesis/cav2013/List.scala
index ce9c60f4e..b76682401 100644
--- a/testcases/synthesis/cav2013/List.scala
+++ b/testcases/synthesis/cav2013/List.scala
@@ -7,6 +7,8 @@ object List {
   case class Cons(head: Int, tail: List) extends List
   case class Nil() extends List
 
+  def inv(l: List): Boolean = true
+
   def size(l: List) : Int = (l match {
       case Nil() => 0
       case Cons(_, t) => 1 + size(t)
@@ -17,48 +19,23 @@ object List {
     case Cons(i, t) => Set(i) ++ content(t)
   }
 
-  def isSorted(l: List): Boolean = l match {
-    case Nil() => true
-    case Cons(x, Nil()) => true
-    case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
-  }
-
-  def isStrictSorted(l: List): Boolean = l match {
-    case Nil() => true
-    case Cons(x, Nil()) => true
-    case Cons(x, Cons(y, ys)) => x < y && isSorted(Cons(y, ys))
-  }
 
-  def deleteSynth(in: List, v: Int) = choose {
-    (out: List) => (content(out) == (content(in) -- Set(v)))
-  }
+  // To Synthesize:
 
-  def deleteSortedSynth(in: List, v: Int) = choose {
-    (out: List) => isSorted(in) && (content(out) == (content(in) -- Set(v))) && isSorted(out)
-  }
 
-  def insertSynth(in: List, v: Int) = choose {
-    (out: List) => (content(out) == (content(in) ++ Set(v)))
+  def insert(in: List, v: Int) = choose {
+    (out: List) => inv(in) && (content(out) == (content(in) ++ Set(v))) && inv(out)
   }
 
-  def insertSortedSynth(in: List, v: Int) = choose {
-    (out: List) => isSorted(in) && (content(out) == (content(in) ++ Set(v))) && isSorted(out)
+  def delete(in: List, v: Int) = choose {
+    (out: List) => inv(in) && (content(out) == (content(in) -- Set(v))) && inv(out)
   }
 
-  def insertStrictSortedSynth(in: List, v: Int) = choose {
-    (out: List) => isStrictSorted(in) && (content(out) == (content(in) ++ Set(v))) && isStrictSorted(out)
+  def union(in1: List, in2: List) = choose {
+    (out: List) => inv(in1) && inv(in2) && (content(out) == (content(in1) ++ content(in2))) && inv(out)
   }
 
-  def concatSynth(in1: List, in2: List) = choose {
-    (out : List) => content(out) == content(in1) ++ content(in2)
+  def intersection(in1: List, in2: List) = choose {
+    (out: List) => inv(in1) && inv(in2) && (content(out) == (content(in1) & content(in2))) && inv(out)
   }
-
-  def mergeSynth(in1: List, in2: List) = choose {
-    (out : List) => isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
-  }
-
-  def mergeStrictSynth(in1: List, in2: List) = choose {
-    (out : List) => isStrictSorted(in1) && isStrictSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isStrictSorted(out)
-  }
-
 }
diff --git a/testcases/synthesis/cav2013/SortedList.scala b/testcases/synthesis/cav2013/SortedList.scala
new file mode 100644
index 000000000..e07619bff
--- /dev/null
+++ b/testcases/synthesis/cav2013/SortedList.scala
@@ -0,0 +1,45 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object SortedList {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  def isSorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x, Nil()) => true
+    case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+  }
+
+  def inv(l: List): Boolean = isSorted(l)
+
+  def size(l: List) : Int = (l match {
+      case Nil() => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil() => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  // To Synthesize:
+
+  def insert(in: List, v: Int) = choose {
+    (out: List) => inv(in) && (content(out) == (content(in) ++ Set(v))) && inv(out)
+  }
+
+  def delete(in: List, v: Int) = choose {
+    (out: List) => inv(in) && (content(out) == (content(in) -- Set(v))) && inv(out)
+  }
+
+  def union(in1: List, in2: List) = choose {
+    (out: List) => inv(in1) && inv(in2) && (content(out) == (content(in1) ++ content(in2))) && inv(out)
+  }
+
+  def intersection(in1: List, in2: List) = choose {
+    (out: List) => inv(in1) && inv(in2) && (content(out) == (content(in1) & content(in2))) && inv(out)
+  }
+}
diff --git a/testcases/synthesis/cav2013/StrictlySortedList.scala b/testcases/synthesis/cav2013/StrictlySortedList.scala
new file mode 100644
index 000000000..9570df701
--- /dev/null
+++ b/testcases/synthesis/cav2013/StrictlySortedList.scala
@@ -0,0 +1,47 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object SortedList {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  def isStrictSorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x, Nil()) => true
+    case Cons(x, Cons(y, ys)) => x < y && isStrictSorted(Cons(y, ys))
+  }
+
+  def inv(l: List): Boolean = isStrictSorted(l)
+
+  def size(l: List) : Int = (l match {
+      case Nil() => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil() => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+
+  // To Synthesize:
+
+
+  def insert(in: List, v: Int) = choose {
+    (out: List) => inv(in) && (content(out) == (content(in) ++ Set(v))) && inv(out)
+  }
+
+  def delete(in: List, v: Int) = choose {
+    (out: List) => inv(in) && (content(out) == (content(in) -- Set(v))) && inv(out)
+  }
+
+  def union(in1: List, in2: List) = choose {
+    (out: List) => inv(in1) && inv(in2) && (content(out) == (content(in1) ++ content(in2))) && inv(out)
+  }
+
+  def intersection(in1: List, in2: List) = choose {
+    (out: List) => inv(in1) && inv(in2) && (content(out) == (content(in1) & content(in2))) && inv(out)
+  }
+}
-- 
GitLab