From 9ef0ded5cf54e5696b3dd952b48c5c1997b698e8 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Sun, 6 Mar 2016 17:51:53 +0100
Subject: [PATCH] Add run-lenght encoding benchmark
---
.../current/RunLength/RunLength.scala | 60 +++++++++++++++++++
testcases/synthesis/current/run.sh | 3 +
2 files changed, 63 insertions(+)
create mode 100644 testcases/synthesis/current/RunLength/RunLength.scala
diff --git a/testcases/synthesis/current/RunLength/RunLength.scala b/testcases/synthesis/current/RunLength/RunLength.scala
new file mode 100644
index 000000000..fd886180e
--- /dev/null
+++ b/testcases/synthesis/current/RunLength/RunLength.scala
@@ -0,0 +1,60 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+import leon.collection._
+
+object RunLength {
+
+
+ def decode[A](l: List[(BigInt, A)]): List[A] = {
+ def fill[A](i: BigInt, a: A): List[A] = {
+ if (i > 0) a :: fill(i - 1, a)
+ else Nil[A]()
+ }
+ l match {
+ case Nil() => Nil[A]()
+ case Cons((i, x), xs) =>
+ fill(i, x) ++ decode(xs)
+ }
+ }
+
+
+ def legal[A](l: List[(BigInt, A)]): Boolean = l match {
+ case Cons((i, x), tl) =>
+ i > 0 && (tl match {
+ case Cons((_, y), _) => x != y
+ case _ => true
+ }) && legal(tl)
+ case _ => true
+ }
+
+ /*def unique[A](l1: List[A], l2: List[A]) => {
+ require(encode(l1) == encode(l2))
+ l1 == l2
+ }.holds*/
+
+ // Solvable with --manual=2,0,0,1,0,0,3,0,1,1,0,0,1,0,0,0,1,1,1
+ def encode[A](l: List[A]): List[(BigInt, A)] = {
+ // Solution
+ /*l match {
+ case Nil() => Nil[(BigInt, A)]()
+ case Cons(x, xs) =>
+ val rec = encode(xs)
+ rec match {
+ case Nil() =>
+ Cons( (BigInt(1), x), Nil[(BigInt,A)]())
+ case Cons( (recC, recEl), recTl) =>
+ if (x == recEl) {
+ Cons( (1+recC, x), recTl)
+ } else {
+ Cons( (BigInt(1), x), rec )
+ }
+ }
+ }*/
+ ???[List[(BigInt, A)]]
+ } ensuring {
+ (res: List[(BigInt, A)]) =>
+ legal(res) && decode(res) == l
+ }
+
+}
diff --git a/testcases/synthesis/current/run.sh b/testcases/synthesis/current/run.sh
index d16431ec7..907198b0b 100755
--- a/testcases/synthesis/current/run.sh
+++ b/testcases/synthesis/current/run.sh
@@ -41,3 +41,6 @@ run testcases/synthesis/current/BatchedQueue/Dequeue.scala
# AddressBook
run testcases/synthesis/current/AddressBook/Make.scala
run testcases/synthesis/current/AddressBook/Merge.scala
+
+# RunLength
+run testcases/synthesis/current/RunLength/RunLength.scala
--
GitLab