Include times, fix testcases

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)
 

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)))
     })
   }
 

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))) => 

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) && 

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(