Remove code generating table for benchmarks

src/main/scala/leon/repair/RepairPhase.scala

@@ -49,19 +49,8 @@ object RepairPhase extends LeonPhase[Program, Program] {
     if (toRepair.isEmpty) reporter.warning("No functions found with the given names")
     
     for (fd <- toRepair) {
-      val res = new Repairman(ctx, program, fd, verifTimeoutMs, verifTimeoutMs).repair()
-      val fw = new FileWriter("repairs.last", true)
-      try {
-        fw.write(res.toLine)
-      } finally {
-        fw.close
-      }
-      val fw2 = new FileWriter("repairs.table", true)
-      try {
-        fw2.write(res.toTableLine)
-      } finally {
-        fw2.close
-      }
+      val rep = new Repairman(ctx, program, fd, verifTimeoutMs, verifTimeoutMs)
+      rep.repair()
     }
 
     program

src/main/scala/leon/repair/RepairResult.scala

-package leon
-package repair
-
-import java.io.File
-
-case class RepairResult(f: File,
-                        psize: Int,
-                        fsize: Int = -1,
-                        name: String = "?",
-                        initTime: Option[Long] = None,
-                        focusTime: Option[Long] = None,
-                        focusSize: Option[Int] = None,
-                        repairTime: Option[Long] = None,
-                        repairSize: Option[Int] = None,
-                        repairTrusted: Option[Boolean] = None) {
-
-  def toLine = {
-    val benchCat  = f.getAbsoluteFile().getParentFile().getName()
-    val benchName = f.getName()
-    val benchFun  = name
-
-    f"$benchCat%20s, $benchName%20s, $benchFun%20s, $psize%3s, $fsize%3s, ${focusSize.getOrElse("")}%3s, ${initTime.getOrElse("")}%5s, ${focusTime.getOrElse("")}%5s, ${repairTime.getOrElse("")}%5s, ${repairTrusted.getOrElse("")}%5s\n"
-  }
-
-  def toTableLine = {
-    val benchCat  = f.getAbsoluteFile().getParentFile().getName()
-    val benchName = f.getName()
-    val benchFun  = name
-
-    def ts(ot: Option[Long]): String = {
-      val s = ot.map{
-        ms => 
-          val t: Double = Math.round(ms/100.0)/10.0
-          f"$t%.1f"
-      }.getOrElse("")
-
-      f"$s%5s"
-    }
-
-    val verified = repairTrusted.map(if (_) "\\chmark" else "").getOrElse("")
-
-    val repairTime2 = (focusTime, repairTime) match {
-      case (Some(t), Some(t2)) => Some(t + t2)
-      case _ => None
-    }
-
-    f"$benchCat%20s &  $benchName%20s & $benchFun%20s & $psize%4s & $fsize%3s & ${focusSize.getOrElse("")}%3s & ${repairSize.getOrElse("")}%3s & ${ts(initTime)} & ${ts(repairTime2)} & $verified%7s \\\\ \n"
-  }
-}
-

src/main/scala/leon/repair/Repairman.scala

@@ -44,11 +44,9 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
     }
   }
 
-  var result = RepairResult(ctx.files.head, programSize(initProgram));
-
   import VRes._
-  
-  def repair(): RepairResult = {
+
+  def repair(): Unit = {
     val to = new TimeoutFor(ctx.interruptManager)
 
     to.interruptAfter(repairTimeoutMs) {
@@ -95,7 +93,6 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
           reporter.info(f" - Minimal Failing Set Size: ${minimalFailingTests.size}%3d")
           
           val initTime = t1.stop
-          result = result.copy(initTime = Some(initTime))
           reporter.info("Finished in "+initTime+"ms")
       
           reporter.ifDebug { printer =>
@@ -110,8 +107,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
       
           var solutions = List[Solution]()
           val focusTime = t2.stop
-          result = result.copy(focusTime = Some(focusTime))
-      
+
           reporter.info("Finished in "+focusTime+"ms")
           reporter.info(ASCIIHelpers.title("3. Synthesizing"))
           reporter.info(p)
@@ -120,7 +116,6 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
           val t3    = new Timer().start
           synth.synthesize() match {
             case (search, sols) =>
-              result = result.copy(repairTime = Some(t3.stop))
               for (sol <- sols) {
       
                 // Validate solution if not trusted
@@ -135,17 +130,14 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
                     case NotValid(_, _) =>
                       solutions ::= sol
                       reporter.warning("Solution is not trusted!")
-                      result = result.copy(repairTrusted = Some(false))
 
                     case Valid =>
                       solutions ::= sol
                       reporter.info("Solution was not trusted but post-validation passed!")
-                      result = result.copy(repairTrusted = Some(true))
                   }
                 } else {
                   reporter.info("Found trusted solution!")
                   solutions ::= sol
-                  result = result.copy(repairTrusted = Some(true))
                 }
               }
       
@@ -162,7 +154,6 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
                 for ((sol, i) <- solutions.reverse.zipWithIndex) {
                   reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
                   val expr = sol.toSimplifiedExpr(ctx, program)
-                  result = result.copy(repairSize = Some(formulaSize(expr)))
                   reporter.info(ScalaPrinter(expr));
                 }
                 reporter.info(ASCIIHelpers.title("In context:"))
@@ -184,8 +175,6 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
             }
       }
     }
-
-    result
   }
 
   def getSynthesizer(failingTests: List[Example]): Synthesizer = {
@@ -195,12 +184,11 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
     val (newBody, replacedExpr) = focusRepair(program, fd, failingTests)
     fd.body = Some(newBody)
 
+    val psize     = programSize(initProgram)
     val size      = formulaSize(body)
     val focusSize = formulaSize(replacedExpr)
 
-    result = result.copy(name = fd.id.name, fsize = size, focusSize = Some(focusSize))
-
-    reporter.info("Program size      : "+result.psize)
+    reporter.info("Program size      : "+psize)
     reporter.info("Original body size: "+size)
     reporter.info("Focused expr size : "+focusSize)