package leon.benchmark import leon._ import leon.purescala.Definitions._ import leon.purescala.Trees._ import leon.purescala.TreeOps._ import leon.solvers.z3._ import leon.solvers.Solver import leon.synthesis._ import leon.test.synthesis._ import java.io.File object SynthesisBenchmarks extends App { private def forEachFileIn(dirName : String)(block : File=>Unit) { import scala.collection.JavaConversions._ for(f <- (new File(dirName)).listFiles() if f.getPath().endsWith(".scala")) { block(f) } } val infoSep : String = "╟" + ("┄" * 86) + "╢" val infoFooter : String = "╚" + ("═" * 86) + "╝" val infoHeader : String = ". ┌────────────┐\n" + "╔═╡ Benchmarks ╞" + ("═" * 71) + "╗\n" + "║ └────────────┘" + (" " * 71) + "║" def infoLine(file: String, f: String, ts: Long, nAlt: Int, nSuccess: Int, nInnap: Int, nDecomp: Int) : String = { "║ %-30s %-24s %3d %10s %10s ms ║".format( file, f, nAlt, nSuccess+"/"+nInnap+"/"+nDecomp, ts) } println(infoHeader) var nSuccessTotal, nInnapTotal, nDecompTotal, nAltTotal = 0 var tTotal: Long = 0 for (path <- args) { val file = new File(path) val ctx = LeonContext( settings = Settings( synthesis = true, xlang = false, verify = false ), files = List(file), reporter = new DefaultReporter ) val opts = SynthesizerOptions() val pipeline = leon.plugin.ExtractionPhase andThen ExtractProblemsPhase val (results, solver) = pipeline.run(ctx)(file.getPath :: Nil) val sctx = SynthesisContext(solver, new SilentReporter, new java.util.concurrent.atomic.AtomicBoolean) for ((f, ps) <- results; p <- ps) { val ts = System.currentTimeMillis val rr = rules.CEGIS.instantiateOn(sctx, p) val nAlt = rr.size var nSuccess, nInnap, nDecomp = 0 for (alt <- rr) { alt.apply(sctx) match { case RuleApplicationImpossible => nInnap += 1 case s: RuleDecomposed => nDecomp += 1 case s: RuleSuccess => nSuccess += 1 } } val t = System.currentTimeMillis - ts nAltTotal += nAlt tTotal += t nSuccessTotal += nSuccess nInnapTotal += nInnap nDecompTotal += nDecomp println(infoLine(file.getName().toString, f.id.toString, t, nAlt, nSuccess, nInnap, nDecomp)) } println(infoSep) } println(infoLine("TOTAL", "", tTotal, nAltTotal, nSuccessTotal, nInnapTotal, nDecompTotal)) println(infoFooter) }