Skip to content
Snippets Groups Projects
Commit 5dba7016 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Clean up Repairman a little

parent 24b99cba
No related branches found
No related tags found
No related merge requests found
...@@ -3,7 +3,6 @@ ...@@ -3,7 +3,6 @@
package leon package leon
package repair package repair
import leon.datagen.GrammarDataGen
import purescala.Path import purescala.Path
import purescala.Definitions._ import purescala.Definitions._
import purescala.Expressions._ import purescala.Expressions._
...@@ -17,6 +16,7 @@ import solvers._ ...@@ -17,6 +16,7 @@ import solvers._
import utils._ import utils._
import codegen._ import codegen._
import verification._ import verification._
import datagen.GrammarDataGen
import synthesis._ import synthesis._
import synthesis.rules._ import synthesis.rules._
...@@ -25,18 +25,15 @@ import synthesis.graph.{dotGenIds, DotGenerator} ...@@ -25,18 +25,15 @@ import synthesis.graph.{dotGenIds, DotGenerator}
import rules._ import rules._
class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeoutMs: Option[Long], repairTimeoutMs: Option[Long]) { class Repairman(ctx: LeonContext, program: Program, fd: FunDef, verifTimeoutMs: Option[Long], repairTimeoutMs: Option[Long]) {
implicit val ctx = ctx0 implicit val ctx0 = ctx
val reporter = ctx.reporter val reporter = ctx.reporter
val doBenchmark = ctx.findOptionOrDefault(GlobalOptions.optBenchmark) val doBenchmark = ctx.findOptionOrDefault(GlobalOptions.optBenchmark)
var program = initProgram
implicit val debugSection = DebugSectionRepair implicit val debugSection = DebugSectionRepair
def repair(): Unit = { def repair(): Unit = {
val to = new TimeoutFor(ctx.interruptManager) val to = new TimeoutFor(ctx.interruptManager)
...@@ -147,7 +144,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou ...@@ -147,7 +144,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
try { try {
fw.write(f"$date: $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%2.1f & ${timeSynth/1000.0}%2.1f & $proof%7s \\\\\n") fw.write(f"$date: $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%2.1f & ${timeSynth/1000.0}%2.1f & $proof%7s \\\\\n")
} finally { } finally {
fw.close fw.close()
} }
}(DebugSectionReport) }(DebugSectionReport)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment