diff --git a/testcases/synthesis/repair/DaysToYears/DaysToYears1.scala b/testcases/synthesis/repair/DaysToYears/DaysToYears1.scala
index c8d475de3da55421a1abe7a9860197b212e634fb..13eec09ae4ee1a611fc5a7d916ed92e061086112 100644
--- a/testcases/synthesis/repair/DaysToYears/DaysToYears1.scala
+++ b/testcases/synthesis/repair/DaysToYears/DaysToYears1.scala
@@ -24,7 +24,7 @@ object DaysToYears {
(((year,days), res) passes {
case (1999, 14 ) => (1999, 14)
case (1980, 366) => (1980, 366)
- case (1981, 634) => (1982, 269)
+ case (1981, 366) => (1982, 1)
})
}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
index e705ff4fabf095941f594200ef0e3f01ba2db833..93d5b61e9288be38928b9a01dfd3092889bfeef3 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
@@ -118,14 +118,14 @@ object RedBlackTree {
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(Red,c,zV,d)) // FIXME: Last Red should be Black
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,xV,d)) // FIXME: xV instead of zV in right node
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))
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,xV,d)) // FIXME: xV instead of zV in right node
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))
+ } 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 {
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree10.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree10.scala
deleted file mode 100644
index 93d5b61e9288be38928b9a01dfd3092889bfeef3..0000000000000000000000000000000000000000
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree10.scala
+++ /dev/null
@@ -1,143 +0,0 @@
-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,xV,d)) // FIXME: xV instead of zV in right node
- 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,xV,d)) // FIXME: xV instead of zV in right node
- 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
index 8ceec4415eefa3fe4e9e2f694b30e90b0c3457e4..4d8e1f39d07d8c667a0fa733d6d09fce2569f1a4 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
@@ -88,7 +88,7 @@ object RedBlackTree {
// ins(x, t)
// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
- /*def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ 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) =>
@@ -118,28 +118,26 @@ object RedBlackTree {
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))
+ Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,xV,d)) // FIXME: xV instead of zV in right node
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))
- */
+ } 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))
+ // 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/RedBlackTree8.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree4.scala
similarity index 100%
rename from testcases/synthesis/repair/RedBlackTree/RedBlackTree8.scala
rename to testcases/synthesis/repair/RedBlackTree/RedBlackTree4.scala
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
index eb5dc7248a6690ff0114307f42d043a81b6509f2..36cfb692b4a9efb218be24eee6bb78dc0c680851 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
@@ -84,7 +84,7 @@ object RedBlackTree {
def add(x: Int, t: Tree): Tree = {
require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
- ins(x, t) // FIX: makeBlack(ins(x, t))
+ ins(x, t) // FIXME: makeBlack(ins(x, t))
} ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree9.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree9.scala
deleted file mode 100644
index 4d8e1f39d07d8c667a0fa733d6d09fce2569f1a4..0000000000000000000000000000000000000000
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree9.scala
+++ /dev/null
@@ -1,143 +0,0 @@
-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,xV,d)) // FIXME: xV instead of zV in right node
- 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))
-
-}