diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index 0305faf6e65f158bacd6cba907789b1ee3baf1dd..c6e1e4466677fd7ee37c17c9a2aef5625e74970b 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/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
diff --git a/src/main/scala/leon/repair/RepairResult.scala b/src/main/scala/leon/repair/RepairResult.scala
deleted file mode 100644
index 463bdae3187bcc810e03eb296e210f5f65370fe5..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/repair/RepairResult.scala
+++ /dev/null
@@ -1,50 +0,0 @@
-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"
- }
-}
-
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 8f50da0117c9b09005b544ac4ebd5fb9dc61bdd8..20caf3bb3ad43ad1cde0cba9e42e6fdce2c46703 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/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)