diff --git a/testcases/synthesis/repair/DaysToYears/DaysToYears.scala b/testcases/repair/DaysToYears/DaysToYears.scala
similarity index 100%
rename from testcases/synthesis/repair/DaysToYears/DaysToYears.scala
rename to testcases/repair/DaysToYears/DaysToYears.scala
diff --git a/testcases/synthesis/repair/DaysToYears/DaysToYears1.scala b/testcases/repair/DaysToYears/DaysToYears1.scala
similarity index 100%
rename from testcases/synthesis/repair/DaysToYears/DaysToYears1.scala
rename to testcases/repair/DaysToYears/DaysToYears1.scala
diff --git a/testcases/synthesis/repair/DaysToYears/DaysToYears2.scala b/testcases/repair/DaysToYears/DaysToYears2.scala
similarity index 100%
rename from testcases/synthesis/repair/DaysToYears/DaysToYears2.scala
rename to testcases/repair/DaysToYears/DaysToYears2.scala
diff --git a/testcases/synthesis/repair/Desugar/Desugar.scala b/testcases/repair/Desugar/Desugar.scala
similarity index 100%
rename from testcases/synthesis/repair/Desugar/Desugar.scala
rename to testcases/repair/Desugar/Desugar.scala
diff --git a/testcases/synthesis/repair/Desugar/Desugar1.scala b/testcases/repair/Desugar/Desugar1.scala
similarity index 100%
rename from testcases/synthesis/repair/Desugar/Desugar1.scala
rename to testcases/repair/Desugar/Desugar1.scala
diff --git a/testcases/synthesis/repair/Desugar/Desugar2.scala b/testcases/repair/Desugar/Desugar2.scala
similarity index 100%
rename from testcases/synthesis/repair/Desugar/Desugar2.scala
rename to testcases/repair/Desugar/Desugar2.scala
diff --git a/testcases/synthesis/repair/Desugar/Desugar3.scala b/testcases/repair/Desugar/Desugar3.scala
similarity index 100%
rename from testcases/synthesis/repair/Desugar/Desugar3.scala
rename to testcases/repair/Desugar/Desugar3.scala
diff --git a/testcases/synthesis/repair/Desugar/Desugar4.scala b/testcases/repair/Desugar/Desugar4.scala
similarity index 100%
rename from testcases/synthesis/repair/Desugar/Desugar4.scala
rename to testcases/repair/Desugar/Desugar4.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort.scala b/testcases/repair/HeapSort/HeapSort.scala
similarity index 100%
rename from testcases/synthesis/repair/HeapSort/HeapSort.scala
rename to testcases/repair/HeapSort/HeapSort.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort1.scala b/testcases/repair/HeapSort/HeapSort1.scala
similarity index 100%
rename from testcases/synthesis/repair/HeapSort/HeapSort1.scala
rename to testcases/repair/HeapSort/HeapSort1.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort2.scala b/testcases/repair/HeapSort/HeapSort2.scala
similarity index 100%
rename from testcases/synthesis/repair/HeapSort/HeapSort2.scala
rename to testcases/repair/HeapSort/HeapSort2.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort3.scala b/testcases/repair/HeapSort/HeapSort3.scala
similarity index 100%
rename from testcases/synthesis/repair/HeapSort/HeapSort3.scala
rename to testcases/repair/HeapSort/HeapSort3.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort4.scala b/testcases/repair/HeapSort/HeapSort4.scala
similarity index 100%
rename from testcases/synthesis/repair/HeapSort/HeapSort4.scala
rename to testcases/repair/HeapSort/HeapSort4.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort5.scala b/testcases/repair/HeapSort/HeapSort5.scala
similarity index 100%
rename from testcases/synthesis/repair/HeapSort/HeapSort5.scala
rename to testcases/repair/HeapSort/HeapSort5.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort6.scala b/testcases/repair/HeapSort/HeapSort6.scala
similarity index 100%
rename from testcases/synthesis/repair/HeapSort/HeapSort6.scala
rename to testcases/repair/HeapSort/HeapSort6.scala
diff --git a/testcases/repair/HeapSort/HeapSort7.scala b/testcases/repair/HeapSort/HeapSort7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d4de52fe4dde4a0af4562b2bd047c5ee0a794c9c
--- /dev/null
+++ b/testcases/repair/HeapSort/HeapSort7.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.collection._
+import leon._
+
+object HeapSort {
+
+ sealed abstract class Heap {
+ val rank : Int = this match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ 1 + max(l.rank, r.rank)
+ }
+ def content : Set[Int] = this match {
+ case Leaf() => Set[Int]()
+ case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+ case class Leaf() extends Heap
+ case class Node(value:Int, left: Heap, right: Heap) extends Heap
+
+ def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
+
+ def hasHeapProperty(h : Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(v, l, r) =>
+ ( l match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ }) &&
+ ( r match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ })
+ }
+
+ def hasLeftistProperty(h: Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(_,l,r) =>
+ hasLeftistProperty(l) &&
+ hasLeftistProperty(r) &&
+ l.rank >= r.rank
+ }
+
+ def heapSize(t: Heap): Int = { t match {
+ case Leaf() => 0
+ case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+ }} ensuring(_ >= 0)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 + v2 > 0) // FIXME: Nonsense, should be v1 >= v2
+ makeN(v1, l1, merge(r1, h2))
+ else
+ makeN(v2, l2, merge(h1, r2))
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+ }
+
+ private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
+ require(
+ hasLeftistProperty(left) && hasLeftistProperty(right)
+ )
+ if(left.rank >= right.rank)
+ Node(value, left, right)
+ else
+ Node(value, right, left)
+ } ensuring { res =>
+ hasLeftistProperty(res) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1 &&
+ res.content == heap.content ++ Set(element)
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h) && hasHeapProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res)
+ }
+
+}
diff --git a/testcases/repair/HeapSort/HeapSort8.scala b/testcases/repair/HeapSort/HeapSort8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..33a3ff5aac56c67109ecd2f9a242c27e41fc69fa
--- /dev/null
+++ b/testcases/repair/HeapSort/HeapSort8.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.collection._
+import leon._
+
+object HeapSort {
+
+ sealed abstract class Heap {
+ val rank : Int = this match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ 1 + max(l.rank, r.rank)
+ }
+ def content : Set[Int] = this match {
+ case Leaf() => Set[Int]()
+ case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+ case class Leaf() extends Heap
+ case class Node(value:Int, left: Heap, right: Heap) extends Heap
+
+ def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
+
+ def hasHeapProperty(h : Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(v, l, r) =>
+ ( l match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ }) &&
+ ( r match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ })
+ }
+
+ def hasLeftistProperty(h: Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(_,l,r) =>
+ hasLeftistProperty(l) &&
+ hasLeftistProperty(r) &&
+ l.rank >= r.rank
+ }
+
+ def heapSize(t: Heap): Int = { t match {
+ case Leaf() => 0
+ case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+ }} ensuring(_ >= 0)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 <= v2) // FIXME should be >=
+ makeN(v1, l1, merge(r1, h2))
+ else
+ makeN(v2, l2, merge(h1, r2))
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+ }
+
+ private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
+ require(
+ hasLeftistProperty(left) && hasLeftistProperty(right)
+ )
+ if(left.rank >= right.rank)
+ Node(value, left, right)
+ else
+ Node(value, right, left)
+ } ensuring { res =>
+ hasLeftistProperty(res) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1 &&
+ res.content == heap.content ++ Set(element)
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h) && hasHeapProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res)
+ }
+
+}
diff --git a/testcases/repair/HeapSort/HeapSort9.scala b/testcases/repair/HeapSort/HeapSort9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6846a9cae6fd0f37f2601c118fb6a502abe61c37
--- /dev/null
+++ b/testcases/repair/HeapSort/HeapSort9.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.collection._
+import leon._
+
+object HeapSort {
+
+ sealed abstract class Heap {
+ val rank : Int = this match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ 1 + max(l.rank, r.rank)
+ }
+ def content : Set[Int] = this match {
+ case Leaf() => Set[Int]()
+ case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+ case class Leaf() extends Heap
+ case class Node(value:Int, left: Heap, right: Heap) extends Heap
+
+ def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
+
+ def hasHeapProperty(h : Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(v, l, r) =>
+ ( l match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ }) &&
+ ( r match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ })
+ }
+
+ def hasLeftistProperty(h: Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(_,l,r) =>
+ hasLeftistProperty(l) &&
+ hasLeftistProperty(r) &&
+ l.rank >= r.rank
+ }
+
+ def heapSize(t: Heap): Int = { t match {
+ case Leaf() => 0
+ case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+ }} ensuring(_ >= 0)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 >= v2)
+ makeN(v1, l1, merge(r1, h2))
+ else
+ makeN(v2, l2, merge(h1, r2))
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+ }
+
+ private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
+ require(
+ hasLeftistProperty(left) && hasLeftistProperty(right)
+ )
+ if(left.rank >= right.rank + 42) // FIXME delete +42
+ Node(value, left, right)
+ else
+ Node(value, right, left)
+ } ensuring { res =>
+ hasLeftistProperty(res) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1 &&
+ res.content == heap.content ++ Set(element)
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h) && hasHeapProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/OffByOne/FirstIndexOf.scala b/testcases/repair/List/FirstIndexOf.scala
similarity index 100%
rename from testcases/synthesis/repair/OffByOne/FirstIndexOf.scala
rename to testcases/repair/List/FirstIndexOf.scala
diff --git a/testcases/synthesis/repair/OffByOne/FirstIndexOf1.scala b/testcases/repair/List/FirstIndexOf1.scala
similarity index 100%
rename from testcases/synthesis/repair/OffByOne/FirstIndexOf1.scala
rename to testcases/repair/List/FirstIndexOf1.scala
diff --git a/testcases/synthesis/repair/OffByOne/FirstIndexOf2.scala b/testcases/repair/List/FirstIndexOf2.scala
similarity index 100%
rename from testcases/synthesis/repair/OffByOne/FirstIndexOf2.scala
rename to testcases/repair/List/FirstIndexOf2.scala
diff --git a/testcases/repair/List/FirstIndexOf3.scala b/testcases/repair/List/FirstIndexOf3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9904ef80485403e37676e5898fd70ddcba510e5d
--- /dev/null
+++ b/testcases/repair/List/FirstIndexOf3.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+
+object FirstIndexOf {
+ def firstIndexOf(l: List[Int], v: Int): Int = {
+ l match {
+ case Cons(h, t) if v == h => 0
+ case Cons(h, t) =>
+ if (firstIndexOf(t, v) > 0) { // FIXME: Should be >=
+ firstIndexOf(t, v)+1
+ } else {
+ -1
+ }
+ case Nil() =>
+ -1
+ }
+ } ensuring { (res: Int) =>
+ (if (l.content contains v) {
+ l.size > res && l.apply(res) == v
+ } else {
+ res == -1
+ }) && (((l,v), res) passes {
+ case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
+ case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
+ })
+ }
+}
diff --git a/testcases/repair/List/FirstIndexOf4.scala b/testcases/repair/List/FirstIndexOf4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..df3c90f7862fa22a6254903b1bee5bd3e4a39db6
--- /dev/null
+++ b/testcases/repair/List/FirstIndexOf4.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+
+object FirstIndexOf {
+ def firstIndexOf(l: List[Int], v: Int): Int = {
+ l match {
+ case Cons(h, t) if v == h => 0
+ case Cons(h, t) =>
+ if (firstIndexOf(t,v) <= 0) { // FIXME: should be >= 0
+ firstIndexOf(t, v)+1
+ } else {
+ -1
+ }
+ case Nil() =>
+ -1
+ }
+ } ensuring { (res: Int) =>
+ (if (l.content contains v) {
+ l.size > res && l.apply(res) == v
+ } else {
+ res == -1
+ }) && (((l,v), res) passes {
+ case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
+ case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
+ })
+ }
+}
diff --git a/testcases/repair/List/Size.scala b/testcases/repair/List/Size.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8e36fc6ab7139fa7dfa64ad10b6cc5832efdd7d8
--- /dev/null
+++ b/testcases/repair/List/Size.scala
@@ -0,0 +1,19 @@
+import leon._
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object List {
+ def size(l: List[Int]): Int = (l match {
+ case Nil() => 1
+ case Cons(h, t) => 1 + size(t)
+ }) ensuring {
+ (res: Int) =>
+ ((l, res) passes {
+ case Cons(a, Nil()) => 1
+ case Cons(a, Cons(b, Nil())) => 2
+ case Cons(a, Cons(b, Cons(c, Nil()))) => 3
+ case Nil() => 0
+ })
+ }
+}
diff --git a/testcases/repair/List/Size1.scala b/testcases/repair/List/Size1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e6aa4e37d1241c1b19b48588846a019641092480
--- /dev/null
+++ b/testcases/repair/List/Size1.scala
@@ -0,0 +1,17 @@
+import leon._
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object List {
+ def size(l: List[Int]): Int = (l match {
+ case Cons(h, t) => 3 + size(t) // FIXME: 1 + ...
+ }) ensuring {
+ (res: Int) =>
+ ((l, res) passes {
+ case Cons(a, Nil()) => 1
+ case Nil() => 0
+ })
+ }
+
+}
diff --git a/testcases/repair/List/Sum.scala b/testcases/repair/List/Sum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..df8ea2e2558c1881c53a7f344a2b1635ed99bd72
--- /dev/null
+++ b/testcases/repair/List/Sum.scala
@@ -0,0 +1,19 @@
+import leon._
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object List {
+ def sum(l: List[Int]): Int = (l match {
+ case Nil() => 0
+ case Cons(h, t) => h + sum(t)
+ }) ensuring {
+ (res: Int) =>
+ ((l, res) passes {
+ case Cons(a, Nil()) => a
+ case Cons(a, Cons(b, Nil())) => a+b
+ case Cons(a, Cons(b, Cons(c, Nil()))) => a+b+c
+ case Nil() => 0
+ })
+ }
+}
diff --git a/testcases/repair/List/Sum1.scala b/testcases/repair/List/Sum1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b809f5c714817615a57aba3a43027e262f83ff10
--- /dev/null
+++ b/testcases/repair/List/Sum1.scala
@@ -0,0 +1,19 @@
+import leon._
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object List {
+ def sum(l: List[Int]): Int = (l match {
+ case Nil() => 0
+ case Cons(h, t) => 1 + sum(t) // FIXME: 1 instead of h
+ }) ensuring {
+ (res: Int) =>
+ ((l, res) passes {
+ case Cons(a, Nil()) => a
+ case Cons(a, Cons(b, Nil())) => a+b
+ case Cons(a, Cons(b, Cons(c, Nil()))) => a+b+c
+ case Nil() => 0
+ })
+ }
+}
diff --git a/testcases/synthesis/repair/Naturals/Naturals.scala b/testcases/repair/Naturals/Naturals.scala
similarity index 100%
rename from testcases/synthesis/repair/Naturals/Naturals.scala
rename to testcases/repair/Naturals/Naturals.scala
diff --git a/testcases/synthesis/repair/Parser/Parser.scala b/testcases/repair/Parser/Parser.scala
similarity index 100%
rename from testcases/synthesis/repair/Parser/Parser.scala
rename to testcases/repair/Parser/Parser.scala
diff --git a/testcases/synthesis/repair/Parser/Parser1.scala b/testcases/repair/Parser/Parser1.scala
similarity index 100%
rename from testcases/synthesis/repair/Parser/Parser1.scala
rename to testcases/repair/Parser/Parser1.scala
diff --git a/testcases/synthesis/repair/Parser/Parser2.scala b/testcases/repair/Parser/Parser2.scala
similarity index 100%
rename from testcases/synthesis/repair/Parser/Parser2.scala
rename to testcases/repair/Parser/Parser2.scala
diff --git a/testcases/synthesis/repair/Parser/Parser3.scala b/testcases/repair/Parser/Parser3.scala
similarity index 100%
rename from testcases/synthesis/repair/Parser/Parser3.scala
rename to testcases/repair/Parser/Parser3.scala
diff --git a/testcases/synthesis/repair/Parser/Parser4.scala b/testcases/repair/Parser/Parser4.scala
similarity index 100%
rename from testcases/synthesis/repair/Parser/Parser4.scala
rename to testcases/repair/Parser/Parser4.scala
diff --git a/testcases/synthesis/repair/Parser/Parser5.scala b/testcases/repair/Parser/Parser5.scala
similarity index 100%
rename from testcases/synthesis/repair/Parser/Parser5.scala
rename to testcases/repair/Parser/Parser5.scala
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic.scala b/testcases/repair/PropLogic/PropLogic.scala
similarity index 100%
rename from testcases/synthesis/repair/PropLogic/PropLogic.scala
rename to testcases/repair/PropLogic/PropLogic.scala
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic1.scala b/testcases/repair/PropLogic/PropLogic1.scala
similarity index 100%
rename from testcases/synthesis/repair/PropLogic/PropLogic1.scala
rename to testcases/repair/PropLogic/PropLogic1.scala
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic2.scala b/testcases/repair/PropLogic/PropLogic2.scala
similarity index 71%
rename from testcases/synthesis/repair/PropLogic/PropLogic2.scala
rename to testcases/repair/PropLogic/PropLogic2.scala
index 192f7e3e776ff59c9e20986ba66ea19cae88ca2e..2799b20788010fc952e51de8d2c0a69421c303cb 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic2.scala
+++ b/testcases/repair/PropLogic/PropLogic2.scala
@@ -47,24 +47,5 @@ object SemanticsPreservation {
case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case _ => true
}
-
- def partEval(formula : Formula) : Formula = { formula match {
- case And(Const(false), _ ) => Const(false)
- case And(_, Const(false)) => Const(false)
- case And(Const(true), e) => partEval(e)
- case And(e, Const(true)) => partEval(e)
- case Or(Const(true), _ ) => Const(true)
- case Or(_, Const(true)) => Const(true)
- case Or(Const(false), e) => partEval(e)
- case Or(e, Const(false)) => partEval(e)
- case Not(Const(c)) => Const(!c)
- case other => other
- }} ensuring { size(_) <= size(formula) }
-
-
- @induct
- def partEvalSound (f : Formula, env : Set[Int]) = {
- eval(partEval(f))(env) == eval(f)(env)
- }.holds
}
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic3.scala b/testcases/repair/PropLogic/PropLogic3.scala
similarity index 100%
rename from testcases/synthesis/repair/PropLogic/PropLogic3.scala
rename to testcases/repair/PropLogic/PropLogic3.scala
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic4.scala b/testcases/repair/PropLogic/PropLogic4.scala
similarity index 100%
rename from testcases/synthesis/repair/PropLogic/PropLogic4.scala
rename to testcases/repair/PropLogic/PropLogic4.scala
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic5.scala b/testcases/repair/PropLogic/PropLogic5.scala
similarity index 100%
rename from testcases/synthesis/repair/PropLogic/PropLogic5.scala
rename to testcases/repair/PropLogic/PropLogic5.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree.scala b/testcases/repair/RedBlackTree/RedBlackTree.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree.scala
rename to testcases/repair/RedBlackTree/RedBlackTree.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala b/testcases/repair/RedBlackTree/RedBlackTree1.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
rename to testcases/repair/RedBlackTree/RedBlackTree1.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala b/testcases/repair/RedBlackTree/RedBlackTree2.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
rename to testcases/repair/RedBlackTree/RedBlackTree2.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala b/testcases/repair/RedBlackTree/RedBlackTree3.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
rename to testcases/repair/RedBlackTree/RedBlackTree3.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree4.scala b/testcases/repair/RedBlackTree/RedBlackTree4.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree4.scala
rename to testcases/repair/RedBlackTree/RedBlackTree4.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala b/testcases/repair/RedBlackTree/RedBlackTree5.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala
rename to testcases/repair/RedBlackTree/RedBlackTree5.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala b/testcases/repair/RedBlackTree/RedBlackTree6.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
rename to testcases/repair/RedBlackTree/RedBlackTree6.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala b/testcases/repair/RedBlackTree/RedBlackTree7.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala
rename to testcases/repair/RedBlackTree/RedBlackTree7.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime.scala b/testcases/repair/SecondsToTime/SecondsToTime.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTime.scala
rename to testcases/repair/SecondsToTime/SecondsToTime.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime1.scala b/testcases/repair/SecondsToTime/SecondsToTime1.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTime1.scala
rename to testcases/repair/SecondsToTime/SecondsToTime1.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime2.scala b/testcases/repair/SecondsToTime/SecondsToTime2.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTime2.scala
rename to testcases/repair/SecondsToTime/SecondsToTime2.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime3.scala b/testcases/repair/SecondsToTime/SecondsToTime3.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTime3.scala
rename to testcases/repair/SecondsToTime/SecondsToTime3.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime4.scala b/testcases/repair/SecondsToTime/SecondsToTime4.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTime4.scala
rename to testcases/repair/SecondsToTime/SecondsToTime4.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod.scala b/testcases/repair/SecondsToTime/SecondsToTimeMod.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod.scala
rename to testcases/repair/SecondsToTime/SecondsToTimeMod.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod1.scala b/testcases/repair/SecondsToTime/SecondsToTimeMod1.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod1.scala
rename to testcases/repair/SecondsToTime/SecondsToTimeMod1.scala
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod2.scala b/testcases/repair/SecondsToTime/SecondsToTimeMod2.scala
similarity index 100%
rename from testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod2.scala
rename to testcases/repair/SecondsToTime/SecondsToTimeMod2.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList.scala b/testcases/repair/SortedList/SortedList.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList.scala
rename to testcases/repair/SortedList/SortedList.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList1.scala b/testcases/repair/SortedList/SortedList1.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList1.scala
rename to testcases/repair/SortedList/SortedList1.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList2.scala b/testcases/repair/SortedList/SortedList2.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList2.scala
rename to testcases/repair/SortedList/SortedList2.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList3.scala b/testcases/repair/SortedList/SortedList3.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList3.scala
rename to testcases/repair/SortedList/SortedList3.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList4.scala b/testcases/repair/SortedList/SortedList4.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList4.scala
rename to testcases/repair/SortedList/SortedList4.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList5.scala b/testcases/repair/SortedList/SortedList5.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList5.scala
rename to testcases/repair/SortedList/SortedList5.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList6.scala b/testcases/repair/SortedList/SortedList6.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList6.scala
rename to testcases/repair/SortedList/SortedList6.scala
diff --git a/testcases/synthesis/repair/SortedList/SortedList7.scala b/testcases/repair/SortedList/SortedList7.scala
similarity index 100%
rename from testcases/synthesis/repair/SortedList/SortedList7.scala
rename to testcases/repair/SortedList/SortedList7.scala
diff --git a/testcases/repair/inria/Desugar-io b/testcases/repair/inria/Desugar-io
new file mode 100644
index 0000000000000000000000000000000000000000..21dd7bc39bcddca22dedf6ec1179dc6700fcbce7
--- /dev/null
+++ b/testcases/repair/inria/Desugar-io
@@ -0,0 +1,69 @@
+INPUT:
+def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), desugar(rhs)) // FIXME forgot Neg
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+}} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e) && ((e,res) passes {
+ case Trees.Minus(Trees.IntLiteral(42), Trees.IntLiteral(i)) =>
+ Plus(Literal(42), Neg(Literal(i)))
+ })
+}
+
+
+COMMAND:
+leon Desugar2.scala --repair --functions=desugar --solvers=fairz3:enum --timeout=5
+
+
+OUTPUT:
+(Focused Problem:)
+[ Info ] ⟦ e;lhs;rhs, ↓ desugar(e) && ⊙ {Plus(desugar(lhs), desugar(rhs))} && ¬e.isInstanceOf[Plus] && e.isInstanceOf[Minus] && lhs == e.lhs && rhs == e.rhs ≺ ⟨ sem(res) == semUntyped(e) && (e, res) passes {
+ case Minus(IntLiteral(42), IntLiteral(i)) =>
+ Plus(Literal(42), Neg(Literal(i)))
+ } ⟩ res ⟧
+...
+(Solution:)
+[ Info ] Found trusted solution!
+[ Info ] ============================== Repair successful: ==============================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] Plus(desugar(lhs), Neg(desugar(rhs)))
+[ Info ] ================================= In context: =================================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] @induct
+ def desugar(e : Trees.Expr): SimpleE = {
+ e match {
+ case Trees.Plus(lhs, rhs) =>
+ Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) =>
+ Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) =>
+ LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And(lhs, rhs) =>
+ Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or(lhs, rhs) =>
+ Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) =>
+ Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) =>
+ Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) =>
+ Literal(v)
+ case Trees.BoolLiteral(b) =>
+ Literal(b2i(b))
+ }
+ } ensuring {
+ (res : SimpleE) => sem(res) == semUntyped(e) && (e, res) passes {
+ case Trees.Minus(Trees.IntLiteral(42), Trees.IntLiteral(i)) =>
+ Plus(Literal(42), Neg(Literal(i)))
+ }
+ }
diff --git a/testcases/repair/inria/Desugar.scala b/testcases/repair/inria/Desugar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..19cd3305ab3e7a63fbb4f35c924819a143838aa3
--- /dev/null
+++ b/testcases/repair/inria/Desugar.scala
@@ -0,0 +1,172 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/inria/Desugar2-io b/testcases/repair/inria/Desugar2-io
new file mode 100644
index 0000000000000000000000000000000000000000..18580e316b68a67798d20da42d073c880709c53e
--- /dev/null
+++ b/testcases/repair/inria/Desugar2-io
@@ -0,0 +1,62 @@
+INPUT:
+def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(1)) // FIXME 1 instead of 0
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+}} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e) && ((e,res) passes {
+ case Trees.Minus(Trees.IntLiteral(42), Trees.IntLiteral(i)) =>
+ Plus(Literal(42), Neg(Literal(i)))
+ })
+}
+
+
+COMMAND:
+leon --repair --timeout=5 Desugar5.scala --functions=desugar
+
+OUTPUT:
+(Focused Problem:)
+[ Info ] ⟦ e;lhs;rhs, ↓ desugar(e) && ⊙ {Ite(desugar(lhs), desugar(rhs), Literal(1))} && ¬e.isInstanceOf[Plus] && ¬e.isInstanceOf[Minus] && ¬e.isInstanceOf[LessThan] && e.isInstanceOf[And] && lhs == e.lhs && rhs == e.rhs ≺ ⟨ sem(res) == semUntyped(e) ⟩ res ⟧
+
+(Solution:)
+[ Info ] Found trusted solution!
+[ Info ] ============================== Repair successful: ==============================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] Ite(desugar(lhs), desugar(rhs), Literal(0))
+[ Info ] ================================= In context: =================================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] @induct
+ def desugar(e : Trees.Expr): SimpleE = {
+ e match {
+ case Trees.Plus(lhs, rhs) =>
+ Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) =>
+ Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) =>
+ LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And(lhs, rhs) =>
+ Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or(lhs, rhs) =>
+ Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) =>
+ Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) =>
+ Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) =>
+ Literal(v)
+ case Trees.BoolLiteral(b) =>
+ Literal(b2i(b))
+ }
+ } ensuring {
+ (res : SimpleE) => sem(res) == semUntyped(e)
+ }
diff --git a/testcases/repair/inria/FirstIndexOf-io b/testcases/repair/inria/FirstIndexOf-io
new file mode 100644
index 0000000000000000000000000000000000000000..587199f2bd7457045b83e74931c949f8d5008628
--- /dev/null
+++ b/testcases/repair/inria/FirstIndexOf-io
@@ -0,0 +1,87 @@
+INPUT:
+
+def firstIndexOf(l: List[Int], v: Int): Int = {
+ l match {
+ case Cons(h, t) if v == h => 0
+ case Cons(h, t) =>
+ if (firstIndexOf(t, v) >= 0) {
+ firstIndexOf(t, v) // Should be +1 (Solves with CEGIS)
+ } else {
+ -1
+ }
+ case Nil() =>
+ -1
+ }
+} ensuring {
+ (res: Int) => (if (l.content contains v) {
+ l.size > res && l.apply(res) == v
+ } else {
+ res == -1
+ }) && (((l,v), res) passes {
+ case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
+ case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
+ })
+}
+
+
+COMMAND:
+leon FirstIndexOf1.scala --repair --solvers=fairz3:enum --timeout=5
+
+OUTPUT:
+(Focused problem:)
+
+[ Info ] ⟦ v;l;t;h, ↓ firstIndexOf(l, v) && ⊙ {firstIndexOf(t, v)} && ¬(l.isInstanceOf[Cons[Int]] && v == l.h) && l.isInstanceOf[Cons[Int]] && h == l.h && t == l.t && firstIndexOf(t, v) >= 0 ≺ ⟨ (if (v ∈ l.content()) {
+ l.size() > res && l.apply(res) == v
+ } else {
+ res == -1
+ }) && ((l, v), res) passes {
+ case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) =>
+ 3
+ case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) =>
+ 3
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) =>
+ 1
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) =>
+ -1
+ } ⟩ res ⟧
+
+
+(Solution)
+[ Info ] Found trusted solution!
+[ Info ] ============================== Repair successful: ==============================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] firstIndexOf(t, v) + 1
+[ Info ] ================================= In context: =================================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] def firstIndexOf(l : List[Int], v : Int): Int = {
+ l match {
+ case Cons(h, t) if v == h =>
+ 0
+ case Cons(h, t) =>
+ if (firstIndexOf(t, v) >= 0) {
+ firstIndexOf(t, v) + 1
+ } else {
+ -1
+ }
+ case Nil() =>
+ -1
+ }
+ } ensuring {
+ (res : Int) => (if (l.content().contains(e)) {
+ l.size() > res && l.apply(res) == v
+ } else {
+ res == -1
+ }) && ((l, v), res) passes {
+ case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) =>
+ 3
+ case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) =>
+ 3
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) =>
+ 1
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) =>
+ -1
+ }
+ }
+
diff --git a/testcases/repair/inria/FirstIndexOf.scala b/testcases/repair/inria/FirstIndexOf.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d591315063d90c26b2adfbe7bdd36b03d4871a99
--- /dev/null
+++ b/testcases/repair/inria/FirstIndexOf.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+
+object FirstIndexOf {
+ def firstIndexOf(l: List[Int], v: Int): Int = {
+ l match {
+ case Cons(h, t) if v == h => 0
+ case Cons(h, t) =>
+ if (firstIndexOf(t, v) >= 0) {
+ firstIndexOf(t, v)+1
+ } else {
+ -1
+ }
+ case Nil() =>
+ -1
+ }
+ } ensuring {
+ (res: Int) => (if (l.content contains v) {
+ l.size > res && l.apply(res) == v
+ } else {
+ res == -1
+ }) && (((l,v), res) passes {
+ case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
+ case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
+ case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
+ })
+ }
+}
diff --git a/testcases/repair/inria/HeapSort-io b/testcases/repair/inria/HeapSort-io
new file mode 100644
index 0000000000000000000000000000000000000000..af9f8b12419c89b56d040f62a87e613dc8f735f1
--- /dev/null
+++ b/testcases/repair/inria/HeapSort-io
@@ -0,0 +1,61 @@
+INPUT:
+
+private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 + v2 > 0) // FIXME: Nonsense, should be v1 >= v2
+ makeN(v1, l1, merge(r1, h2))
+ else
+ makeN(v2, l2, merge(h1, r2))
+ }
+} ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+}
+
+
+COMMAND:
+leon HeapSort7.scala --repair --functions=merge
+
+OUTPUT:
+
+(focused problem/ condition fails)
+[ Info ] ⟦ l1;r2;v1;l2;h1;v2;h2;r1, ↓ merge(h1, h2) && ⊙ {(v1 + v2 > 0)} && hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2) && ¬h1.isInstanceOf[Leaf] && ¬h2.isInstanceOf[Leaf] && h1.isInstanceOf[Node] && v1 == h1.value && l1 == h1.left && r1 == h1.right && h2.isInstanceOf[Node] && v2 == h2.value && l2 == h2.left && r2 == h2.right ≺ ⟨ val res = if (cond) {
+ makeN(v1, l1, merge(r1, h2))
+ } else {
+ makeN(v2, l2, merge(h1, r2))
+ };
+ hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ∪ h2.content() == res.content() ⟩ cond ⟧
+
+(solution)
+[ Info ] Found trusted solution!
+[ Info ] ============================== Repair successful: ==============================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] v2 <= v1
+[ Info ] ================================= In context: =================================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] def merge(h1 : Heap, h2 : Heap): Heap = {
+ require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2))
+ (h1, h2) match {
+ case (Leaf(), _) =>
+ h2
+ case (_, Leaf()) =>
+ h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if (v2 <= v1) {
+ makeN(v1, l1, merge(r1, h2))
+ } else {
+ makeN(v2, l2, merge(h1, r2))
+ }
+ }
+ } ensuring {
+ (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content()
+ }
+
diff --git a/testcases/repair/inria/HeapSort.scala b/testcases/repair/inria/HeapSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5ceed2228715ceb2ea9bb7270c81c3608698a6a9
--- /dev/null
+++ b/testcases/repair/inria/HeapSort.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.collection._
+import leon._
+
+object HeapSort {
+
+ sealed abstract class Heap {
+ val rank : Int = this match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ 1 + max(l.rank, r.rank)
+ }
+ def content : Set[Int] = this match {
+ case Leaf() => Set[Int]()
+ case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+ case class Leaf() extends Heap
+ case class Node(value:Int, left: Heap, right: Heap) extends Heap
+
+ def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
+
+ def hasHeapProperty(h : Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(v, l, r) =>
+ ( l match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ }) &&
+ ( r match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ })
+ }
+
+ def hasLeftistProperty(h: Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(_,l,r) =>
+ hasLeftistProperty(l) &&
+ hasLeftistProperty(r) &&
+ l.rank >= r.rank
+ }
+
+ def heapSize(t: Heap): Int = { t match {
+ case Leaf() => 0
+ case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+ }} ensuring(_ >= 0)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 >= v2)
+ makeN(v1, l1, merge(r1, h2))
+ else
+ makeN(v2, l2, merge(h1, r2))
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+ }
+
+ private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
+ require(
+ hasLeftistProperty(left) && hasLeftistProperty(right)
+ )
+ if(left.rank >= right.rank)
+ Node(value, left, right)
+ else
+ Node(value, right, left)
+ } ensuring { res =>
+ hasLeftistProperty(res) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1 &&
+ res.content == heap.content ++ Set(element)
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h) && hasHeapProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res)
+ }
+
+}
diff --git a/testcases/repair/inria/PropLogic-io b/testcases/repair/inria/PropLogic-io
new file mode 100644
index 0000000000000000000000000000000000000000..517099269c80202dcc521cec11cc7d704a530bc3
--- /dev/null
+++ b/testcases/repair/inria/PropLogic-io
@@ -0,0 +1,84 @@
+INPUT:
+
+def nnf(formula : Formula) : Formula = { formula match {
+ case Not(And(lhs,rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs,rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Const(v)) => Const(!v)
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ // FIXME: forgot to handle the Not(Not(_)) case
+ case other => other
+}} ensuring { res =>
+ isNNF(res) && ((formula, res) passes {
+ case Not(Not(Not(Const(a)))) => Const(!a)
+ })
+}
+
+COMMAND:
+leon PropLogic2.scala --repair --functions=nnf --solvers=fairz3:enum
+
+
+OUTPUT:
+(Focused Problem:)
+(Comment:
+ There is something here that is not legal Scala, namely formula.f
+ The path condition makes sure formula is indeed a Not so it has the f field, but Scala would require a typecast here.
+)
+[ Info ] ⟦ formula;other, ↓ nnf(formula) && ⊙ {other} && ¬(formula.isInstanceOf[Not] && formula.f.isInstanceOf[And]) && ¬(formula.isInstanceOf[Not] && formula.f.isInstanceOf[Or]) && ¬(formula.isInstanceOf[Not] && formula.f.isInstanceOf[Const]) && ¬formula.isInstanceOf[And] && ¬formula.isInstanceOf[Or] && other == formula ≺ ⟨ isNNF(res) && (formula, res) passes {
+ case Not(Not(Not(Const(a)))) =>
+ Const(¬a)
+ } ⟩ res ⟧
+
+(Solution:)
+[ Info ] Found trusted solution!
+[ Info ] ============================== Repair successful: ==============================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] formula match {
+ case Const(v) =>
+ other
+ case Literal(id) =>
+ other
+ case Not(f) =>
+ f match {
+ case Literal(id) =>
+ nnf(Literal(id))
+ case Not(f1) =>
+ nnf(f1)
+ }
+ }
+[ Info ] ================================= In context: =================================
+[ Info ] --------------------------------- Solution 1: ---------------------------------
+[ Info ] def nnf(formula : Formula): Formula = {
+ formula match {
+ case Not(And(lhs, rhs)) =>
+ Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) =>
+ And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Const(v)) =>
+ Const(!v)
+ case And(lhs, rhs) =>
+ And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) =>
+ Or(nnf(lhs), nnf(rhs))
+ case other =>
+ formula match {
+ case Const(v) =>
+ other
+ case Literal(id) =>
+ other
+ case Not(f) =>
+ f match {
+ case Literal(id) =>
+ nnf(Literal(id))
+ case Not(f1) =>
+ nnf(f1)
+ }
+ }
+ }
+ } ensuring {
+ (res : Formula) => isNNF(res) && (formula, res) passes {
+ case Not(Not(Not(Const(a)))) =>
+ Const(!a)
+ }
+ }
+
diff --git a/testcases/repair/inria/PropLogic.scala b/testcases/repair/inria/PropLogic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..718a36e89b1fb70e7eb1c4cfc0a35520f7f953c4
--- /dev/null
+++ b/testcases/repair/inria/PropLogic.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+
+object SemanticsPreservation {
+
+ sealed abstract class Formula
+ case class And(lhs : Formula, rhs : Formula) extends Formula
+ case class Or(lhs : Formula, rhs : Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Const(v: Boolean) extends Formula
+ case class Literal(id: Int) extends Formula
+
+ def size(f : Formula) : Int = { f match {
+ case And(l,r) => 1 + size(l) + size(r)
+ case Or(l,r) => 1 + size(l) + size(r)
+ case Not(e) => 1 + size(e)
+ case _ => 1
+ }} ensuring { _ >= 0 }
+
+ def eval(formula: Formula)(implicit trueVars : Set[Int]): Boolean = formula match {
+ case And(lhs, rhs) => eval(lhs) && eval(rhs)
+ case Or(lhs, rhs) => eval(lhs) || eval(rhs)
+ case Not(f) => !eval(f)
+ case Const(v) => v
+ case Literal(id) => trueVars contains id
+ }
+
+ def nnf(formula : Formula) : Formula = { formula match {
+ case Not(And(lhs,rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs,rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Const(v)) => Const(!v)
+ case Not(Not(e)) => nnf(e)
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case other => other
+ }} ensuring { res =>
+ isNNF(res)
+ }
+
+ def isNNF(f : Formula) : Boolean = f match {
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case _ => true
+ }
+
+
+}