Add listOfSize benchmark

synthesis-collective.txt

@@ -13,6 +13,7 @@ List.delete                 |   61 |    0 | ✓ | 4.5  | F | 30.1 | ✓ | 3.2  |
 List.union                  |   75 |   11 | ✓ | 7.1  | ✓ | 12.5 | ✓ | 3.5  | ✓ | 1.7  | ✓ | 1.9  | ✓ | 1.9  | ✓ | 1.9  |
 List.diff                   |  106 |    0 | ✓ | 6.1  | F | 31.8 | ✓ | 11.2 | ✓ | 9.1  | ✓ | 10.1 | ✓ | 10.8 | ✓ | 10.8 |
 List.split*(easier for O-O) |   96 |   24 | ✓ | 3.6  | ✓ | 5.3  | ✓ | 2.6  | ✓ | 2.2  | ✓ | 2.3  | ✓ | 2.6  | ✓ | 2.6  |
+List.listOfSize             |   54 |   11 |   |      |   |      |   |      |   |      |   |      |   |      | ✓ | 1.5  |
 SortedList.insert           |   91 |    0 | ? | 16.5 | F | 30.0 | ? | 23.6 | ? | 11.8 | ? | 11.8 | ? | 10.6 | ? | 11.0 |
 SortedList.insertAlways     |  105 |    0 | ✓ | 20.5 | F | 30.0 | ✓ | 40.8 | ✓ | 22.2 | ✓ | 23.2 | ✓ | 21.9 | ✓ | 21.2 |
 SortedList.delete           |   91 |    0 | ? | 7.9  | F | 30.0 | ? | 5.7  | ? | 9.5  | ? | 9.6  | ? | 10.2 | ? | 9.5  |

testcases/synthesis/current/List/ListOfSize.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object ListOfSize {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def listOfSize(s: BigInt) = {
+    require(s >= 0)
+    choose((l: List) => size(l) == s)
+  }
+}

testcases/synthesis/current/run.sh

@@ -15,6 +15,7 @@ run testcases/synthesis/current/List/Delete.scala
 run testcases/synthesis/current/List/Union.scala
 run testcases/synthesis/current/List/Diff.scala
 run testcases/synthesis/current/List/Split.scala
+run testcases/synthesis/current/List/ListOfSize.scala
 
 # SortedList
 run testcases/synthesis/current/SortedList/Insert.scala