From b1408d30baf31afb4e4b2d434511801c3de412d8 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Sun, 2 Nov 2014 20:09:41 +0100
Subject: [PATCH] Repair benchmarks
---
.../synthesis/repair/HeapSort/HeapSort.scala | 86 +++++++++++
.../synthesis/repair/HeapSort/HeapSort1.scala | 86 +++++++++++
.../synthesis/repair/HeapSort/HeapSort2.scala | 87 +++++++++++
.../synthesis/repair/HeapSort/HeapSort5.scala | 86 +++++++++++
.../repair/PropLogic/PropLogic.scala | 66 ++++++++
.../repair/PropLogic/PropLogic1.scala | 66 ++++++++
.../repair/PropLogic/PropLogic3.scala | 66 ++++++++
.../repair/PropLogic/PropLogic4.scala | 67 ++++++++
.../repair/PropLogic/PropLogic5.scala | 66 ++++++++
.../repair/PropLogic/PropLogic6.scala | 68 +++++++++
.../repair/RedBlackTree/RedBlackTree.scala | 143 +++++++++++++++++
.../repair/RedBlackTree/RedBlackTree1.scala | 143 +++++++++++++++++
.../repair/RedBlackTree/RedBlackTree2.scala | 143 +++++++++++++++++
.../repair/RedBlackTree/RedBlackTree3.scala | 144 ++++++++++++++++++
.../repair/RedBlackTree/RedBlackTree5.scala | 144 ++++++++++++++++++
.../repair/RedBlackTree/RedBlackTree6.scala | 144 ++++++++++++++++++
.../repair/RedBlackTree/RedBlackTree7.scala | 143 +++++++++++++++++
.../repair/SecondsToTime/SecondsToTime.scala | 38 +++++
.../repair/SecondsToTime/SecondsToTime1.scala | 38 +++++
.../repair/SecondsToTime/SecondsToTime2.scala | 38 +++++
.../repair/SecondsToTime/SecondsToTime3.scala | 38 +++++
.../repair/SecondsToTime/SecondsToTime4.scala | 38 +++++
.../SecondsToTime/SecondsToTimeMod.scala | 22 +++
.../SecondsToTime/SecondsToTimeMod1.scala | 22 +++
.../SecondsToTime/SecondsToTimeMod2.scala | 22 +++
.../repair/SortedList/SortedList.scala | 51 +++++++
.../repair/SortedList/SortedList1.scala | 51 +++++++
.../repair/SortedList/SortedList2.scala | 51 +++++++
.../repair/SortedList/SortedList3.scala | 51 +++++++
.../repair/SortedList/SortedList4.scala | 52 +++++++
.../repair/SortedList/SortedList5.scala | 51 +++++++
.../repair/SortedList/SortedList6.scala | 51 +++++++
.../repair/SortedList/SortedList7.scala | 52 +++++++
33 files changed, 2414 insertions(+)
create mode 100644 testcases/synthesis/repair/HeapSort/HeapSort.scala
create mode 100644 testcases/synthesis/repair/HeapSort/HeapSort1.scala
create mode 100644 testcases/synthesis/repair/HeapSort/HeapSort2.scala
create mode 100644 testcases/synthesis/repair/HeapSort/HeapSort5.scala
create mode 100644 testcases/synthesis/repair/PropLogic/PropLogic.scala
create mode 100644 testcases/synthesis/repair/PropLogic/PropLogic1.scala
create mode 100644 testcases/synthesis/repair/PropLogic/PropLogic3.scala
create mode 100644 testcases/synthesis/repair/PropLogic/PropLogic4.scala
create mode 100644 testcases/synthesis/repair/PropLogic/PropLogic5.scala
create mode 100644 testcases/synthesis/repair/PropLogic/PropLogic6.scala
create mode 100644 testcases/synthesis/repair/RedBlackTree/RedBlackTree.scala
create mode 100644 testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
create mode 100644 testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
create mode 100644 testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
create mode 100644 testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala
create mode 100644 testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
create mode 100644 testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTime.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTime1.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTime2.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTime3.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTime4.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod1.scala
create mode 100644 testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod2.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList1.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList2.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList3.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList4.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList5.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList6.scala
create mode 100644 testcases/synthesis/repair/SortedList/SortedList7.scala
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort.scala b/testcases/synthesis/repair/HeapSort/HeapSort.scala
new file mode 100644
index 000000000..8cd6b51fa
--- /dev/null
+++ b/testcases/synthesis/repair/HeapSort/HeapSort.scala
@@ -0,0 +1,86 @@
+/* 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)
+ }
+ }
+ 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 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))
+ (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) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res)
+ }
+
+ 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 { hasLeftistProperty(_) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ }
+
+}
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort1.scala b/testcases/synthesis/repair/HeapSort/HeapSort1.scala
new file mode 100644
index 000000000..c9976e2dd
--- /dev/null
+++ b/testcases/synthesis/repair/HeapSort/HeapSort1.scala
@@ -0,0 +1,86 @@
+/* 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)
+ }
+ }
+ 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 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))
+ (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, r2, merge(h1, l2)) // FIXME: swap l2 and r2
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res)
+ }
+
+ 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 { hasLeftistProperty(_) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ }
+
+}
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort2.scala b/testcases/synthesis/repair/HeapSort/HeapSort2.scala
new file mode 100644
index 000000000..c33921bee
--- /dev/null
+++ b/testcases/synthesis/repair/HeapSort/HeapSort2.scala
@@ -0,0 +1,87 @@
+/* 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)
+ }
+ }
+ 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 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))
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 > v2)
+ Node(v1, l1, merge(r1, h2)) // FIXME: Forgot to put the heap of lowest rank on the left
+ // (failed to use makeN)
+ else
+ Node(v2, l2, merge(h1, r2)) // FIXME: Same as above
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res)
+ }
+/*
+ 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 { hasLeftistProperty(_) }
+*/
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ }
+
+}
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort5.scala b/testcases/synthesis/repair/HeapSort/HeapSort5.scala
new file mode 100644
index 000000000..e601a6225
--- /dev/null
+++ b/testcases/synthesis/repair/HeapSort/HeapSort5.scala
@@ -0,0 +1,86 @@
+/* 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)
+ }
+ }
+ 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 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))
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h2 // FIXME: h2 instead of 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) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res)
+ }
+
+ 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 { hasLeftistProperty(_) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ }
+
+}
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic.scala b/testcases/synthesis/repair/PropLogic/PropLogic.scala
new file mode 100644
index 000000000..c33b0500e
--- /dev/null
+++ b/testcases/synthesis/repair/PropLogic/PropLogic.scala
@@ -0,0 +1,66 @@
+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 { isNNF(_) }
+
+ 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
+ }
+
+ 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/PropLogic1.scala b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
new file mode 100644
index 000000000..9668ca1a1
--- /dev/null
+++ b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
@@ -0,0 +1,66 @@
+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)) => e // FIXME: should be nnf(e)
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case other => other
+ }} ensuring { isNNF(_) }
+
+ 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
+ }
+
+ 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/synthesis/repair/PropLogic/PropLogic3.scala
new file mode 100644
index 000000000..b905ed40f
--- /dev/null
+++ b/testcases/synthesis/repair/PropLogic/PropLogic3.scala
@@ -0,0 +1,66 @@
+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 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 { isNNF(_) }
+
+ 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
+ }
+
+ 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/PropLogic4.scala b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
new file mode 100644
index 000000000..549b91c45
--- /dev/null
+++ b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
@@ -0,0 +1,67 @@
+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 { isNNF(_) }
+
+ 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
+ }
+
+ 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)
+ // FIXME (hard!) : treats Or as And
+ case Or(Const(false), _ ) => Const(false)
+ case Or(_, Const(false)) => Const(false)
+ case Or(Const(true), e) => partEval(e)
+ case Or(e, Const(true)) => 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/PropLogic5.scala b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
new file mode 100644
index 000000000..4b8a2149a
--- /dev/null
+++ b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
@@ -0,0 +1,66 @@
+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 { isNNF(_) }
+
+ 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
+ }
+
+ 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) // FIXME should be !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/PropLogic6.scala b/testcases/synthesis/repair/PropLogic/PropLogic6.scala
new file mode 100644
index 000000000..12791f753
--- /dev/null
+++ b/testcases/synthesis/repair/PropLogic/PropLogic6.scala
@@ -0,0 +1,68 @@
+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 { isNNF(_) }
+
+ 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
+ }
+
+ 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) }
+ // FIXME: should be <=
+ // Can you realize you cannot fix this without breaking partEvalSound?
+
+
+ @induct
+ def partEvalSound (f : Formula, env : Set[Int]) = {
+ eval(partEval(f))(env) == eval(f)(env)
+ }.holds
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree.scala
new file mode 100644
index 000000000..a63a70ce7
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree.scala
@@ -0,0 +1,143 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black,_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty => 1
+ case Node(Black, l, _, _) => blackHeight(l) + 1
+ case Node(Red, l, _, _) => blackHeight(l)
+ }
+
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty => Node(Red,Empty,x,Empty)
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) &&
+ size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren(res) &&
+ blackBalanced(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ n match {
+ case Node(Red,l,v,r) => Node(Black,l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+// def buggyAdd(x: Int, t: Tree): Tree = {
+// require(redNodesHaveBlackChildren(t))
+// // makeBlack(ins(x, t))
+// ins(x, t)
+// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+
+ // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
new file mode 100644
index 000000000..9480a1686
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
@@ -0,0 +1,143 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black,_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty => 1
+ case Node(Black, l, _, _) => blackHeight(l) + 1
+ case Node(Red, l, _, _) => blackHeight(l)
+ }
+
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty => Node(Red,Empty,x,Empty)
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) &&
+ size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren(res) &&
+ blackBalanced(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ n match {
+ case Node(Red,l,v,r) => Node(Black,l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+// def buggyAdd(x: Int, t: Tree): Tree = {
+// require(redNodesHaveBlackChildren(t))
+// // makeBlack(ins(x, t))
+// ins(x, t)
+// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Red,c,zV,d)) // FIXME: Last Red should be Black
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Red,c,zV,d)) // FIXME: as above
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+
+ // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
new file mode 100644
index 000000000..6aa63cefd
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
@@ -0,0 +1,143 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black,_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty => 1
+ case Node(Black, l, _, _) => blackHeight(l) + 1
+ case Node(Red, l, _, _) => blackHeight(l)
+ }
+
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty => Node(Red,Empty,x,Empty)
+ case Node(c,a,y,b) =>
+ if (x < y) Node(c, ins(x, a), y, b) // FIXME : forgot to balance
+ else if (x == y) Node(c,a,y,b)
+ else Node(c,a,y,ins(x, b)) // FIXME : as above
+ }
+ } ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) &&
+ size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren(res) &&
+ blackBalanced(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ n match {
+ case Node(Red,l,v,r) => Node(Black,l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+// def buggyAdd(x: Int, t: Tree): Tree = {
+// require(redNodesHaveBlackChildren(t))
+// // makeBlack(ins(x, t))
+// ins(x, t)
+// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+
+ // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
new file mode 100644
index 000000000..1bad0be29
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
@@ -0,0 +1,144 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black,_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty => 1
+ case Node(Black, l, _, _) => blackHeight(l) + 1
+ case Node(Red, l, _, _) => blackHeight(l)
+ }
+
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty => Node(Red,Empty,x,Empty)
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) &&
+ size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren(res) &&
+ blackBalanced(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ n match {
+ case Node(Red,l,v,r) => Node(Black,l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+// def buggyAdd(x: Int, t: Tree): Tree = {
+// require(redNodesHaveBlackChildren(t))
+// // makeBlack(ins(x, t))
+// ins(x, t)
+// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+
+ // FIXME : says buggy, so I uncommented it!
+ def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala
new file mode 100644
index 000000000..bea0f7bbc
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala
@@ -0,0 +1,144 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black,_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty => 1
+ case Node(Black, l, _, _) => blackHeight(l) + 1
+ case Node(Red, l, _, _) => blackHeight(l)
+ }
+
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty => Node(Red,Empty,x,Empty)
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) &&
+ size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren(res) &&
+ blackBalanced(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ n match {
+ case Node(Red,l,v,r) => Node(Black,l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+// def buggyAdd(x: Int, t: Tree): Tree = {
+// require(redNodesHaveBlackChildren(t))
+// // makeBlack(ins(x, t))
+// ins(x, t)
+// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // FIXME: forgot this case
+ //case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+
+ // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
new file mode 100644
index 000000000..865c320ab
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
@@ -0,0 +1,144 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black,_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty => 1
+ case Node(Black, l, _, _) => blackHeight(l) + 1
+ case Node(Red, l, _, _) => blackHeight(l)
+ }
+
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty => Node(Red,Empty,x,Empty)
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) &&
+ size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren(res) &&
+ blackBalanced(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ n match {
+ case Node(Red,l,v,r) => Node(Black,l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ // FIXME: uncommented this
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ // makeBlack(ins(x, t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+
+ // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala
new file mode 100644
index 000000000..ff1284dae
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala
@@ -0,0 +1,143 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black,_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty => 1
+ case Node(Black, l, _, _) => blackHeight(l) + 1
+ case Node(Red, l, _, _) => blackHeight(l)
+ }
+
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty => Node(Red,Empty,x,Empty)
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) &&
+ size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren(res) &&
+ blackBalanced(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ n match {
+ case Node(Red,l,v,r) => Node(Black,l,v,r)
+ case Node(Black,l,v,r) => Node(Red,l,v,r) // FIXME : Red instead of Black
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+// def buggyAdd(x: Int, t: Tree): Tree = {
+// require(redNodesHaveBlackChildren(t))
+// // makeBlack(ins(x, t))
+// ins(x, t)
+// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ Node(c,a,x,b) match {
+ case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+
+ // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) =>
+ // Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTime.scala
new file mode 100644
index 000000000..151b6c51a
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTime.scala
@@ -0,0 +1,38 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ rec(total, total, 0, 0)
+ } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) })
+
+ def rec(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+ require(
+ total == toSecs(h, m, r) &&
+ m >= 0 && m < 60 &&
+ h >= 0 && r >= 0 &&
+ (m == 0 || r + m * 60 < 3600)
+ )
+
+ if(r >= 3600) {
+ rec(total, r - 3600, h + 1, m)
+ } else if(r >= 60) {
+ rec(total, r - 60, h, m + 1)
+ } else {
+ (h, m, r)
+ }
+ } ensuring { res =>
+ val (h,m,s) = res
+ prop(total, h, m, s)
+ }
+
+
+
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime1.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTime1.scala
new file mode 100644
index 000000000..8396cece5
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTime1.scala
@@ -0,0 +1,38 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ rec(total, total, 0, 0)
+ } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) })
+
+ def rec(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+ require(
+ total == toSecs(h, m, r) &&
+ m >= 0 && m < 60 &&
+ h >= 0 && r >= 0 &&
+ (m == 0 || r + m * 60 < 3600)
+ )
+
+ if(r >= 3600) {
+ rec(total, r - 3600, h , m) // FIXME: Should be h+1
+ } else if(r >= 60) {
+ rec(total, r - 60, h, m + 1)
+ } else {
+ (h, m, r)
+ }
+ } ensuring { res =>
+ val (h,m,s) = res
+ prop(total, h, m, s)
+ }
+
+
+
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime2.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTime2.scala
new file mode 100644
index 000000000..9a9aa90fc
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTime2.scala
@@ -0,0 +1,38 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ rec(total, total, 0, 0)
+ } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) })
+
+ def rec(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+ require(
+ total == toSecs(h, m, r) &&
+ m >= 0 && m < 60 &&
+ h >= 0 && r >= 0 &&
+ (m == 0 || r + m * 60 < 3600)
+ )
+
+ if(r >= 3600) {
+ rec(total, r - 3600, h + 1, m)
+ } else if(r >= 60) {
+ rec(total, r - 60, h, m )// FIXME : Should be m + 1
+ } else {
+ (h, m, r)
+ }
+ } ensuring { res =>
+ val (h,m,s) = res
+ prop(total, h, m, s)
+ }
+
+
+
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime3.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTime3.scala
new file mode 100644
index 000000000..3b23952e8
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTime3.scala
@@ -0,0 +1,38 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ rec(total, total, 0, 0)
+ } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) })
+
+ def rec(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+ require(
+ total == toSecs(h, m, r) &&
+ m >= 0 && m < 60 &&
+ h >= 0 && r >= 0 &&
+ (m == 0 || r + m * 60 < 3600)
+ )
+
+ if(r >= 3600) {
+ rec(total, r - 3600, h + 1, m)
+ } else if(r > 60) { // FIXME (hard!) condition should be >=
+ rec(total, r - 60, h, m + 1)
+ } else {
+ (h, m, r)
+ }
+ } ensuring { res =>
+ val (h,m,s) = res
+ prop(total, h, m, s)
+ }
+
+
+
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTime4.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTime4.scala
new file mode 100644
index 000000000..31843a58c
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTime4.scala
@@ -0,0 +1,38 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ rec(total, total, 0, 0)
+ } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) })
+
+ def rec(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+ require(
+ total == toSecs(h, m, r) &&
+ m >= 0 && m < 60 &&
+ h >= 0 && r >= 0 &&
+ (m == 0 || r + m * 60 < 3600)
+ )
+
+ if(r >= 3600) {
+ rec(total, r - 3600, h + 1, m)
+ } else if(r >= 60) {
+ rec(total, r - 60, h, m + 1)
+ } else {
+ (r, m, h) // FIXME: flipped the order in the tuple
+ }
+ } ensuring { res =>
+ val (h,m,s) = res
+ prop(total, h, m, s)
+ }
+
+
+
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod.scala
new file mode 100644
index 000000000..32e486119
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod.scala
@@ -0,0 +1,22 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ val h = total / 3600
+ val rest = total % 3600
+ val m = rest / 60
+ val s = rest % 60
+ (h,m,s)
+ } ensuring { _ match { case (h,m,s) =>
+ prop(total, h, m, s)
+ }}
+
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod1.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod1.scala
new file mode 100644
index 000000000..7df923d6b
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod1.scala
@@ -0,0 +1,22 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ val h = total / 3600
+ val rest = total % 3600
+ val m = rest / 60
+ val s = rest / 60 // FIXME : / instead of %
+ (h,m,s)
+ } ensuring { _ match { case (h,m,s) =>
+ prop(total, h, m, s)
+ }}
+
+
+}
diff --git a/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod2.scala b/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod2.scala
new file mode 100644
index 000000000..d54d58666
--- /dev/null
+++ b/testcases/synthesis/repair/SecondsToTime/SecondsToTimeMod2.scala
@@ -0,0 +1,22 @@
+
+object SecondsToTime {
+
+ def toSecs(h: Int, m: Int, s: Int) = h * 3600 + m * 60 + s
+ def prop(t: Int, h: Int, m: Int, s: Int) : Boolean =
+ toSecs(h, m, s) == t &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60
+
+ def secondsToTime(total : Int) = {
+ require(total >= 0)
+ val h = total / 3600
+ val rest = total % 3600
+ val m = rest / 60
+ val s = total % 60 // FIXME: total instead of rest
+ (h,m,s)
+ } ensuring { _ match { case (h,m,s) =>
+ prop(total, h, m, s)
+ }}
+
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList.scala b/testcases/synthesis/repair/SortedList/SortedList.scala
new file mode 100644
index 000000000..1b79edd82
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList.scala
@@ -0,0 +1,51 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ Cons(h1, merge(t1,l2))
+ else
+ Cons(h2, merge(l1,t2))
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, Cons(h2, tl)) =>
+ val (t1,t2) = split(tl)
+ ( Cons(h1,t1), Cons(h2,t2) )
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1),mergeSort(l2))
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList1.scala b/testcases/synthesis/repair/SortedList/SortedList1.scala
new file mode 100644
index 000000000..39ca45d49
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList1.scala
@@ -0,0 +1,51 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ Cons(h1, merge(t1,l2))
+ else
+ Cons(h2, merge(l1,t2))
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, Cons(h2, tl)) =>
+ val (t1,t2) = split(tl)
+ ( Cons(h1,t1), Cons(h2,t2) )
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(l1,l2) // FIXME: Forgot to mergeSort l1 and l2
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList2.scala b/testcases/synthesis/repair/SortedList/SortedList2.scala
new file mode 100644
index 000000000..0219d16f3
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList2.scala
@@ -0,0 +1,51 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ Cons(h1, merge(t1,l2))
+ else
+ Cons(h1, merge(l1,t2)) // FIXME: h1 instead of h2
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, Cons(h2, tl)) =>
+ val (t1,t2) = split(tl)
+ ( Cons(h1,t1), Cons(h2,t2) )
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1),mergeSort(l2))
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList3.scala b/testcases/synthesis/repair/SortedList/SortedList3.scala
new file mode 100644
index 000000000..175683215
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList3.scala
@@ -0,0 +1,51 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ //if (h1 <= h2) // FIXME : didn't EqSplit here
+ Cons(h1, merge(t1,l2))
+ //else
+ //Cons(h2, merge(l1,t2))
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, Cons(h2, tl)) =>
+ val (t1,t2) = split(tl)
+ ( Cons(h1,t1), Cons(h2,t2) )
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1),mergeSort(l2))
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList4.scala b/testcases/synthesis/repair/SortedList/SortedList4.scala
new file mode 100644
index 000000000..4a2ba301c
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList4.scala
@@ -0,0 +1,52 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ Cons(h1, merge(t1,l2))
+ else
+ Cons(h2, merge(l1,t2))
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, tl) =>
+ val (t1,t2) = split(tl)
+ ( Cons(h1,t1), t2 )
+ // FIXME (hard) : this is nonsense, just places everything on the first list
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1),mergeSort(l2))
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList5.scala b/testcases/synthesis/repair/SortedList/SortedList5.scala
new file mode 100644
index 000000000..b0310ae8c
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList5.scala
@@ -0,0 +1,51 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ Cons(h1, merge(t1,l2))
+ else
+ Cons(h2, merge(l1,t2))
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, Cons(h2, tl)) =>
+ val (t1,t2) = split(tl)
+ ( t1, Cons(h2,t2) ) // FIXME: t1 should be h1 :: t1
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1),mergeSort(l2))
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList6.scala b/testcases/synthesis/repair/SortedList/SortedList6.scala
new file mode 100644
index 000000000..523cee08c
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList6.scala
@@ -0,0 +1,51 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ Cons(h1, merge(t1,l2))
+ else
+ Cons(h2, merge(t1,t2)) // FIXME : t1 instead l1
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, Cons(h2, tl)) =>
+ val (t1,t2) = split(tl)
+ ( Cons(h1,t1), Cons(h2,t2) )
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1),mergeSort(l2))
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
diff --git a/testcases/synthesis/repair/SortedList/SortedList7.scala b/testcases/synthesis/repair/SortedList/SortedList7.scala
new file mode 100644
index 000000000..fbd78cf8e
--- /dev/null
+++ b/testcases/synthesis/repair/SortedList/SortedList7.scala
@@ -0,0 +1,52 @@
+import leon.collection._
+import leon.lang.synthesis._
+
+object SortedList {
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(h1, tl@Cons(h2, _)) => h1 <= h2 && isSorted(tl)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ // FIXME : swap the branches
+ Cons(h2, merge(l1,t2))
+ else
+ Cons(h1, merge(t1,l2))
+ }
+ } ensuring { res =>
+ isSorted(res) && (res.content == l1.content ++ l2.content)
+ }
+
+
+ def split(l : List[Int]) : (List[Int], List[Int]) = { l match {
+ case Cons(h1, Cons(h2, tl)) =>
+ val (t1,t2) = split(tl)
+ ( Cons(h1,t1), Cons(h2,t2) )
+ case _ => (l, Nil[Int]())
+ }} ensuring { res =>
+ val (res1,res2) = res
+ res1.content ++ res2.content == l.content &&
+ res1.size + res2.size == l.size &&
+ res1.size <= res2.size + 1 &&
+ res1.size >= res2.size - 1
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case _ =>
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1),mergeSort(l2))
+ }} ensuring { res =>
+ res.content == l.content &&
+ isSorted(res)
+ }
+
+}
--
GitLab