From 58e50f675d913191802c97ef4de93794412a2e74 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 17 Mar 2016 19:50:02 +0100
Subject: [PATCH] Add listOfSize benchmark
---
synthesis-collective.txt | 1 +
.../synthesis/current/List/ListOfSize.scala | 24 +++++++++++++++++++
testcases/synthesis/current/run.sh | 1 +
3 files changed, 26 insertions(+)
create mode 100644 testcases/synthesis/current/List/ListOfSize.scala
diff --git a/synthesis-collective.txt b/synthesis-collective.txt
index b8b35afce..8220967f2 100644
--- a/synthesis-collective.txt
+++ b/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 |
diff --git a/testcases/synthesis/current/List/ListOfSize.scala b/testcases/synthesis/current/List/ListOfSize.scala
new file mode 100644
index 000000000..12a95b590
--- /dev/null
+++ b/testcases/synthesis/current/List/ListOfSize.scala
@@ -0,0 +1,24 @@
+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)
+ }
+}
diff --git a/testcases/synthesis/current/run.sh b/testcases/synthesis/current/run.sh
index 2768ce261..85b2c0f3b 100755
--- a/testcases/synthesis/current/run.sh
+++ b/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
--
GitLab