Add list differences benchmark

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 |
 ====================================================================================================================================================================

testcases/synthesis/current/Diffs/Diffs.scala

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

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
+