From b50c56179d63f8a9801536574d7cc462996570c4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 9 Mar 2016 15:32:35 +0100
Subject: [PATCH] Add list differences benchmark
---
synthesis-collective.txt | 3 ++-
testcases/synthesis/current/Diffs/Diffs.scala | 16 ++++++++++++++++
testcases/synthesis/current/run.sh | 4 ++++
3 files changed, 22 insertions(+), 1 deletion(-)
create mode 100644 testcases/synthesis/current/Diffs/Diffs.scala
diff --git a/synthesis-collective.txt b/synthesis-collective.txt
index acf809699..2be829c86 100644
--- a/synthesis-collective.txt
+++ b/synthesis-collective.txt
@@ -6,7 +6,7 @@ F = Timeout/failed to synth.
====================================================================================================================================================================
-Name | FDefs| Size | O-O-5 | O-O-7 | 6cf54fc | e710631 | 1d71892 | 1588205 | 7c6ca79 | 904b6ce | 79fd5c5 | 93fda91 | |
+Name | FDefs| Size | O-O-5 | O-O-7 | 6cf54fc | e710631 | 1d71892 | 1588205 | 7c6ca79 | 904b6ce | 79fd5c5 | 93fda91 |<current> |
====================================================================================================================================================================
List.insert | 59 | 3 | ✓ | 0.8 | ✓ | 1.0 | ✓ | 0.8 | ✓ | 0.8 | ✓ | 0.8 | ✓ | 0.8 | ✓ | 0.8 | ✓ | 0.9 | ✓ | 0.8 | ✓ | 0.6 | ✓ | 0.7 |
List.delete | 61 | 0 | ✓ | 4.5 | F | 30.1 | ✓ | 9.8 | ✓ | 4.3 | ✓ | 4.3 | ✓ | 4.2 | ✓ | 4.3 | ✓ | 4.0 | ✓ | 3.5 | ✓ | 3.6 | ✓ | 3.2 |
@@ -30,4 +30,5 @@ BatchedQueue.dequeue | 65 | 9 | ? | 14.3 | ? | 11.4 | ? | 8.4 | ? |
AddressBook.makeAddressBook | 42 | 0 | F | 14.3 | F | 30.0 | ✓ | 7.5 | ✓ | 25.2 | ✓ | 6.9 | ✓ | 7.2 | ✓ | 6.7 | ✓ | 5.6 | ✓ | 6.3 | ✓ | 6.6 | ✓ | 6.7 |
AddressBook.merge | 99 | 11 | ? | 6.9 | ? | 9.5 | ? | 7.6 | ? | 8.1 | ? | 6.1 | ? | 6.3 | ? | 6.1 | ? | 5.6 | ? | 5.5 | ? | 9.6 | ? | 9.9 |
RunLength.encode | 110 | 38 | | | | | | | | | | | | | | | | | | | ✓ | 50.9 | ✓ | 54.0 |
+Diffs.diffs | 63 | 22 | | | | | | | | | | | | | | | | | | | | | ✓ | 20.0 |
====================================================================================================================================================================
diff --git a/testcases/synthesis/current/Diffs/Diffs.scala b/testcases/synthesis/current/Diffs/Diffs.scala
new file mode 100644
index 000000000..fb0e01afb
--- /dev/null
+++ b/testcases/synthesis/current/Diffs/Diffs.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object Diffs {
+
+ def diffs(l: List[BigInt]): List[BigInt] =
+ choose((res: List[BigInt]) =>
+ res.size == l.size && undiff(res) == l
+ )
+
+ def undiff(l: List[BigInt]) = {
+ l.scanLeft(BigInt(0))(_ + _).tail
+ }
+}
+
diff --git a/testcases/synthesis/current/run.sh b/testcases/synthesis/current/run.sh
index 907198b0b..2768ce261 100755
--- a/testcases/synthesis/current/run.sh
+++ b/testcases/synthesis/current/run.sh
@@ -44,3 +44,7 @@ run testcases/synthesis/current/AddressBook/Merge.scala
# RunLength
run testcases/synthesis/current/RunLength/RunLength.scala
+
+# Diffs
+run testcases/synthesis/current/Diffs/Diffs.scala
+
--
GitLab