From 5e347618f13c093979f3be5831efd54f718182fb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 15 Dec 2014 19:44:45 +0100
Subject: [PATCH] Include times, fix testcases
---
src/main/scala/leon/repair/Repairman.scala | 6 ++++++
.../synthesis/repair/PropLogic/PropLogic4.scala | 2 +-
.../repair/RedBlackTree/RedBlackTree1.scala | 4 ++--
.../repair/RedBlackTree/RedBlackTree2.scala | 2 +-
.../repair/RedBlackTree/RedBlackTree6.scala | 14 ++++++--------
5 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index c88913162..e5b257f07 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -32,17 +32,23 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
def repair() = {
reporter.info(ASCIIHelpers.title("1. Discovering tests for "+fd.id))
+ val t1 = new Timer().start
val (passingTests, failingTests) = discoverTests
reporter.info(f" - Passing: ${passingTests.size}%3d")
reporter.info(f" - Failing: ${failingTests.size}%3d")
+ reporter.info("Finished in "+t1.stop+"ms")
+
+
reporter.info(ASCIIHelpers.title("2. Locating/Focusing synthesis problem"))
+ val t2 = new Timer().start
val synth = getSynthesizer(passingTests, failingTests)
val p = synth.problem
var solutions = List[Solution]()
+ reporter.info("Finished in "+t2.stop+"ms")
reporter.info(ASCIIHelpers.title("3. Synthesizing"))
reporter.info(p)
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic4.scala b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
index 20e44fe92..025c0a8b5 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic4.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
@@ -37,7 +37,7 @@ object SemanticsPreservation {
case other => other
}} ensuring { res =>
isNNF(res) && ((formula, res) passes {
- case Or(Not(Const(c)), Not(Literal(l))) => Or(Const(c), Not(Literal(l)))
+ case Or(Not(Const(c)), Not(Literal(l))) => Or(Const(!c), Not(Literal(l)))
})
}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
index 9480a1686..e705ff4fa 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
@@ -116,9 +116,9 @@ object RedBlackTree {
// )
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
+ 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: as above
+ Node(Red,Node(Black,a,xV,b),yV,Node(Red,c,zV,d)) // FIXME: Last Red should be Black
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))) =>
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
index 6aa63cefd..d4675cadb 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
@@ -59,7 +59,7 @@ object RedBlackTree {
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
+ else balance(c,a,y,ins(x, b))
}
} ensuring (res =>
content(res) == content(t) ++ Set(x) &&
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
index 865c320ab..eb5dc7248 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
@@ -77,17 +77,15 @@ object RedBlackTree {
}
} 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 add(x: Int, t: Tree): Tree = {
require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
- makeBlack(ins(x, t))
+ ins(x, t) // FIX: 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(
--
GitLab