Skip to content
Snippets Groups Projects
Commit be48611d authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Collect stats code to produce reports for papers/thesis

parent a6259e94
No related branches found
No related tags found
No related merge requests found
...@@ -8,6 +8,7 @@ import purescala.ExprOps._ ...@@ -8,6 +8,7 @@ import purescala.ExprOps._
import purescala.DefOps._ import purescala.DefOps._
import purescala.ScalaPrinter import purescala.ScalaPrinter
import solvers._ import solvers._
import leon.utils._
import scala.concurrent.duration._ import scala.concurrent.duration._
...@@ -34,9 +35,10 @@ class Synthesizer(val context : LeonContext, ...@@ -34,9 +35,10 @@ class Synthesizer(val context : LeonContext,
} }
} }
def synthesize(): (Search, Stream[Solution]) = { private var lastTime: Long = 0
reporter.ifDebug { printer => def synthesize(): (Search, Stream[Solution]) = {
reporter.ifDebug { printer =>
printer(problem.eb.asString("Tests available for synthesis")(context)) printer(problem.eb.asString("Tests available for synthesis")(context))
} }
...@@ -47,8 +49,12 @@ class Synthesizer(val context : LeonContext, ...@@ -47,8 +49,12 @@ class Synthesizer(val context : LeonContext,
val sols = s.search(sctx) val sols = s.search(sctx)
val diff = t.stop() val diff = t.stop()
lastTime = diff
reporter.info("Finished in "+diff+"ms") reporter.info("Finished in "+diff+"ms")
(s, sols) (s, sols)
} }
...@@ -62,6 +68,43 @@ class Synthesizer(val context : LeonContext, ...@@ -62,6 +68,43 @@ class Synthesizer(val context : LeonContext,
validateSolution(s, sol, 5.seconds) validateSolution(s, sol, 5.seconds)
} }
// Print out report for synthesis, if necessary
reporter.ifDebug { printer =>
import java.io.FileWriter
import java.text.SimpleDateFormat
import java.util.Date
val categoryName = ci.fd.getPos.file.toString.split("/").dropRight(1).lastOption.getOrElse("?")
val benchName = categoryName+"."+ci.fd.id.name
var time = lastTime/1000.0;
val defs = visibleDefsFrom(ci.fd)(program).collect {
case cd: ClassDef => 1 + cd.fields.size
case fd: FunDef => 1 + fd.params.size + formulaSize(fd.fullBody)
}
val psize = defs.sum;
val (size, calls, proof) = result.headOption match {
case Some((sol, trusted)) =>
val expr = sol.toSimplifiedExpr(context, program)
(formulaSize(expr), functionCallsOf(expr).size, if (trusted) "$\\surd$" else "")
case _ =>
(0, 0, "X")
}
val date = new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(new Date())
val fw = new java.io.FileWriter("synthesis-report.txt", true)
try {
fw.write(f"$date: $benchName%-50s & $psize%4d & $size%4d & $calls%4d & $proof%7s & $time%.2f \\\\\n")
} finally {
fw.close
}
}(DebugSectionReport)
(s, if (result.isEmpty && allowPartial) { (s, if (result.isEmpty && allowPartial) {
List((new PartialSolution(s.g, true).getSolution, false)).toStream List((new PartialSolution(s.g, true).getSolution, false)).toStream
} else { } else {
......
...@@ -23,6 +23,7 @@ case object DebugSectionLeon extends DebugSection("leon", 1 << 1 ...@@ -23,6 +23,7 @@ case object DebugSectionLeon extends DebugSection("leon", 1 << 1
case object DebugSectionXLang extends DebugSection("xlang", 1 << 12) case object DebugSectionXLang extends DebugSection("xlang", 1 << 12)
case object DebugSectionTypes extends DebugSection("types", 1 << 13) case object DebugSectionTypes extends DebugSection("types", 1 << 13)
case object DebugSectionIsabelle extends DebugSection("isabelle", 1 << 14) case object DebugSectionIsabelle extends DebugSection("isabelle", 1 << 14)
case object DebugSectionReport extends DebugSection("report", 1 << 15)
object DebugSections { object DebugSections {
val all = Set[DebugSection]( val all = Set[DebugSection](
...@@ -40,6 +41,7 @@ object DebugSections { ...@@ -40,6 +41,7 @@ object DebugSections {
DebugSectionLeon, DebugSectionLeon,
DebugSectionXLang, DebugSectionXLang,
DebugSectionTypes, DebugSectionTypes,
DebugSectionIsabelle DebugSectionIsabelle,
DebugSectionReport
) )
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment