Produce a table

runTests.sh

@@ -4,6 +4,7 @@ summaryLog=repairs.log
 fullLog=fullLog.log
 
 echo -n "" > $log;
+echo -n "" > "repairs.table";
 
 
 echo "################################" >> $summaryLog

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

@@ -56,6 +56,12 @@ object RepairPhase extends LeonPhase[Program, Program] {
       } finally {
         fw.close
       }
+      val fw2 = new FileWriter("repairs.table", true)
+      try {
+        fw2.write(res.toTableLine)
+      } finally {
+        fw2.close
+      }
     }
 
     program

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

@@ -11,6 +11,7 @@ case class RepairResult(f: File,
                         focusTime: Option[Long] = None,
                         focusSize: Option[Int] = None,
                         repairTime: Option[Long] = None,
+                        repairSize: Option[Int] = None,
                         repairTrusted: Option[Boolean] = None) {
 
   def toLine = {
@@ -21,5 +22,24 @@ case class RepairResult(f: File,
     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.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("")
+
+    f"$benchCat%20s &  $benchName%20s & $benchFun%20s & $psize%4s & $fsize%3s & ${focusSize.getOrElse("")}%3s & ${repairSize.getOrElse("")}%3s & ${ts(initTime)} & ${ts(focusTime)} & ${ts(repairTime)} & $verified%7s \\\\ \n"
+  }
 }
 

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

@@ -37,9 +37,14 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
     case class NotValid(passing : List[Example], failing : List[Example]) extends VerificationResult
   }
 
-  var result = RepairResult(ctx.files.head, visibleFunDefsFromMain(initProgram).foldLeft(0) {
-    case (s, f) => formulaSize(f.fullBody) + s
-  });
+  def programSize(pgm: Program): Int = {
+    visibleFunDefsFromMain(pgm).foldLeft(0) {
+      case (s, f) => 
+        1 + f.params.size + formulaSize(f.fullBody) + s
+    }
+  }
+
+  var result = RepairResult(ctx.files.head, programSize(initProgram));
 
   import VRes._
   
@@ -121,6 +126,7 @@ 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:"))