diff --git a/src/main/scala/leon/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala index 842e3fc0a6989d7ff58c69467a7df7f32132651f..b3e060ba5dcb9738c9a5e5aef797904efadb9798 100644 --- a/src/main/scala/leon/Stopwatch.scala +++ b/src/main/scala/leon/Stopwatch.scala @@ -1,39 +1,54 @@ package leon +class StopwatchCollection(name: String) { + var acc: Long = 0L + + def +=(sw: Stopwatch) = synchronized { acc += sw.getMillis } + + def getMillis = acc + + override def toString = "%20s: %5dms".format(name, acc) +} + /** Implements a stopwatch for profiling purposes */ -class Stopwatch(description : String, verbose : Boolean = false) { +class Stopwatch(name: String = "Stopwatch") { var beginning: Long = 0L var end: Long = 0L var acc: Long = 0L - def start : Stopwatch = { + def start: this.type = { beginning = System.currentTimeMillis + end = 0L this } - def stop : Double = { - end = System.currentTimeMillis - acc += (end - beginning) - val seconds = (end - beginning) / 1000.0 - if (verbose) println("Stopwatch %-25s: %-3.3fs" format (description, seconds)) - seconds + def stop { + end = System.currentTimeMillis + acc += (end - beginning) + beginning = 0L } - def writeToSummary : Unit = { - Stopwatch.timeLog += - (description -> (Stopwatch.timeLog.getOrElse(description, Nil) :+ ((end - beginning) / 1000.0))) + def getMillis: Long = { + if (isRunning) { + acc + (System.currentTimeMillis-beginning) + } else { + acc + } } + + def isRunning = beginning != 0L + + override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "") } -object Stopwatch { - val timeLog = scala.collection.mutable.Map[String, Seq[Double]]() +object StopwatchCollections { + private var all = Map[String, StopwatchCollection]() - def printSummary : Unit = { - val toPrint = timeLog.map{case (k, v) => ("%-25s" format k) + "Total time: " + v.foldLeft(0.0){case (a, b) => a + b}}.mkString("\n") - val forGraph = timeLog.map{ case (k, v) => "GRAPH: " + k + " " + v.mkString(" ")}.mkString("\n") + def get(name: String): StopwatchCollection = all.getOrElse(name, { + val sw = new StopwatchCollection(name) + all += name -> sw + sw + }) - println("Total times per stopwatch description") - println(toPrint) - println(forGraph) - } + def getAll = all } diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala index 70368d7c86d0a2a9a5ff5e9e57cf132601f29d63..c74b03439e58a60315d2e9407c578325817e4866 100644 --- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala @@ -203,68 +203,66 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ } class UnrollingBank { - private val blockMap : MutableMap[(Identifier,Boolean),Set[FunctionInvocation]] = MutableMap.empty - private def registerBlocked(id: Identifier, pol: Boolean, fi: FunctionInvocation) : Boolean = - registerBlocked(id,pol,Set(fi)) - private def registerBlocked(id: Identifier, pol: Boolean, fis: Set[FunctionInvocation]) : Boolean = { - val filtered = fis.filter(i => { - val FunctionInvocation(fd, _) = i - !axiomatizedFunctions(fd) - }) - - if(!filtered.isEmpty) { - val pair = (id, pol) - val alreadyBlocked = blockMap.get(pair) - alreadyBlocked match { - case None => blockMap(pair) = filtered - case Some(prev) => blockMap(pair) = prev ++ filtered - } - true - } else { - false + // Keep which function invocation is guarded by which guard with polarity, + // also specify the generation of the blocker + private val blockersInfo : MutableMap[(Identifier,Boolean), (Int, Z3AST, Set[FunctionInvocation])] = MutableMap.empty + + def currentZ3Blockers = blockersInfo.map(_._2._2) + + def canUnroll = !blockersInfo.isEmpty + + def getBlockersToUnlock: Seq[(Identifier, Boolean)] = { + val minGeneration = blockersInfo.values.map(_._1).min + + blockersInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1) + } + + private def registerBlocker(gen: Int, id: Identifier, pol: Boolean, fis: Set[FunctionInvocation]) { + val pair = (id, pol) + + val z3ast = toZ3Formula(if (pol) Not(Variable(id)) else Variable(id)).get + + blockersInfo.get(pair) match { + case Some((exGen, _, exFis)) => + assert(exGen == gen, "Mixing the same pair "+pair+" with various generations "+ exGen+" and "+gen) + + blockersInfo(pair) = ((gen, z3ast, fis++exFis)) + case None => + blockersInfo(pair) = ((gen, z3ast, fis)) } } - def scanForNewTemplates(expr: Expr): (Seq[Expr], Seq[(Identifier, Boolean)]) = { + def scanForNewTemplates(expr: Expr): Seq[Expr] = { val tmp = FunctionTemplate.mkTemplate(expr) - val allBlocks : MutableSet[(Identifier,Boolean)] = MutableSet.empty - for (((i, p), fis) <- tmp.blockers) { - if(registerBlocked(i, p, fis)) { - allBlocks += i -> p - } + registerBlocker(0, i, p, fis) } - (tmp.asClauses, allBlocks.toSeq) + tmp.asClauses } - private def treatFunctionInvocationSet(sVar : Identifier, pol : Boolean, fis : Set[FunctionInvocation]) : (Seq[Expr],Seq[(Identifier,Boolean)]) = { - val allBlocks : MutableSet[(Identifier,Boolean)] = MutableSet.empty - var allNewExprs : Seq[Expr] = Seq.empty + def unlock(id: Identifier, pol: Boolean) : Seq[Expr] = { + val pair = (id, pol) + assert(blockersInfo contains pair) + + val (gen, _, fis) = blockersInfo(pair) + blockersInfo -= pair + + var newClauses : Seq[Expr] = Seq.empty for(fi <- fis) { - val temp = FunctionTemplate.mkTemplate(fi.funDef) - val (newExprs,newBlocks) = temp.instantiate(sVar, pol, fi.args) + val temp = FunctionTemplate.mkTemplate(fi.funDef) + val (newExprs, newBlocks) = temp.instantiate(id, pol, fi.args) for(((i, p), fis) <- newBlocks) { - if(registerBlocked(i, p, fis)) { - allBlocks += i -> p - } + registerBlocker(gen+1, i, p, fis) } - allNewExprs = allNewExprs ++ newExprs - } - (allNewExprs, allBlocks.toSeq) - } - def unlock(id: Identifier, pol: Boolean) : (Seq[Expr], Seq[(Identifier,Boolean)]) = { - if(!blockMap.isDefinedAt((id,pol))) { - (Seq.empty,Seq.empty) - } else { - val copy = blockMap((id,pol)) - blockMap((id,pol)) = Set.empty - treatFunctionInvocationSet(id, pol, copy) + newClauses ++= newExprs } + + newClauses } } @@ -320,9 +318,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ var definitiveModel : Map[Identifier,Expr] = Map.empty var definitiveCore : Set[Expr] = Set.empty - // Unrolling state - private var blockingSet: Set[Expr] = Set.empty - def assertCnstr(expression: Expr) { val guard = frameGuards.head @@ -330,13 +325,11 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ frameExpressions = (expression :: frameExpressions.head) :: frameExpressions.tail - val (newClauses, newGuards) = unrollingBank.scanForNewTemplates(expression) - + val newClauses = unrollingBank.scanForNewTemplates(expression) + for (cl <- newClauses) { solver.assertCnstr(z3.mkImplies(guard, toZ3Formula(cl).get)) } - - blockingSet ++= newGuards.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) } def getModel = { @@ -348,6 +341,11 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ } def fairCheck(assumptions: Set[Expr]): Option[Boolean] = { + val totalTime = new Stopwatch().start + val luckyTime = new Stopwatch() + val z3Time = new Stopwatch() + val unrollingTime = new Stopwatch() + foundDefinitiveAnswer = false def foundAnswer(answer : Option[Boolean], model : Map[Identifier,Expr] = Map.empty, core: Set[Expr] = Set.empty) : Unit = { @@ -376,15 +374,18 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ while(!foundDefinitiveAnswer && !forceStop) { iterationsLeft -= 1 - val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get) + //val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get) // println("Blocking set : " + blockingSet) reporter.info(" - Running Z3 search...") //reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n")) - //reporter.info("Assumptions:\n"+(blockingSetAsZ3 ++ assumptionsAsZ3).mkString(" AND ")) + //reporter.info("UAssumptions:\n"+unrollingBank.currentZ3Blockers.mkString(" && ")) + //reporter.info("Assumptions:\n"+(unrollingBank.currentZ3Blockers ++ assumptionsAsZ3).mkString(" AND ")) - val res = solver.checkAssumptions((blockingSetAsZ3 ++ assumptionsAsZ3) :_*) + z3Time.start + val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.currentZ3Blockers) :_*) + z3Time.stop reporter.info(" - Finished search with blocked literals") @@ -418,8 +419,8 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ foundAnswer(Some(true), model) } - case Some(false) if blockingSet.isEmpty => - val core = z3CoreToCore(solver.getUnsatCore) + case Some(false) if !unrollingBank.canUnroll => + val core = z3CoreToCore(solver.getUnsatCore) foundAnswer(Some(false), core = core) @@ -427,7 +428,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ // distinction is made inside. case Some(false) => - val core = z3CoreToCore(solver.getUnsatCore) + val core = z3CoreToCore(solver.getUnsatCore) reporter.info("UNSAT BECAUSE: "+core.mkString(" AND ")) @@ -439,7 +440,9 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ reporter.info(" - Running search without blocked literals (w/o lucky test)") } + z3Time.start val res2 = solver.checkAssumptions(assumptionsAsZ3 : _*) + z3Time.stop res2 match { case Some(false) => @@ -449,7 +452,10 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ //reporter.info("SAT WITHOUT Blockers") if (Settings.luckyTest && !forceStop) { // we might have been lucky :D + luckyTime.start val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC) + luckyTime.stop + if(wereWeLucky) { foundAnswer(Some(true), cleanModel) } @@ -465,69 +471,66 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ if(!foundDefinitiveAnswer) { reporter.info("- We need to keep going.") - val toRelease : Set[Expr] = blockingSet - // reporter.info(" - toRelease : " + toRelease) // reporter.info(" - blockingSet : " + blockingSet) - var fixedForEver : Set[Expr] = Set.empty - - if(Settings.pruneBranches) { - for(ex <- blockingSet) ex match { - case Not(Variable(b)) => - solver.push - solver.assertCnstr(toZ3Formula(Variable(b)).get) - solver.check match { - case Some(false) => - //println("We had ~" + b + " in the blocking set. We now know it should stay there forever.") - solver.pop(1) - solver.assertCnstr(toZ3Formula(Not(Variable(b))).get) - fixedForEver = fixedForEver + ex - - case _ => - solver.pop(1) - } - - case Variable(b) => - solver.push - solver.assertCnstr(toZ3Formula(Not(Variable(b))).get) - solver.check match { - case Some(false) => - //println("We had " + b + " in the blocking set. We now know it should stay there forever.") - solver.pop(1) - solver.assertCnstr(toZ3Formula(Variable(b)).get) - fixedForEver = fixedForEver + ex - - case _ => - solver.pop(1) - } - - case _ => - scala.sys.error("Should not have happened.") - } - - if(fixedForEver.size > 0) { - reporter.info("- Pruned out " + fixedForEver.size + " branches.") - } - } - - blockingSet = blockingSet -- toRelease - - val toReleaseAsPairs : Set[(Identifier,Boolean)] = (toRelease -- fixedForEver).map(b => b match { - case Variable(id) => (id, true) - case Not(Variable(id)) => (id, false) - case _ => scala.sys.error("Impossible value in release set: " + b) - }) + //var fixedForEver : Set[Expr] = Set.empty + + //if(Settings.pruneBranches) { + // z3Time.start + // for(ex <- blockingSet) ex match { + // case Not(Variable(b)) => + // solver.push + // solver.assertCnstr(toZ3Formula(Variable(b)).get) + // solver.check match { + // case Some(false) => + // //println("We had ~" + b + " in the blocking set. We now know it should stay there forever.") + // solver.pop(1) + // solver.assertCnstr(toZ3Formula(Not(Variable(b))).get) + // fixedForEver = fixedForEver + ex + + // case _ => + // solver.pop(1) + // } + + // case Variable(b) => + // solver.push + // solver.assertCnstr(toZ3Formula(Not(Variable(b))).get) + // solver.check match { + // case Some(false) => + // //println("We had " + b + " in the blocking set. We now know it should stay there forever.") + // solver.pop(1) + // solver.assertCnstr(toZ3Formula(Variable(b)).get) + // fixedForEver = fixedForEver + ex + + // case _ => + // solver.pop(1) + // } + + // case _ => + // scala.sys.error("Should not have happened.") + // } + + // if(fixedForEver.size > 0) { + // reporter.info("- Pruned out " + fixedForEver.size + " branches.") + // } + // z3Time.stop + //} + + val toReleaseAsPairs = unrollingBank.getBlockersToUnlock reporter.info(" - more unrollings") - for((id,polarity) <- toReleaseAsPairs) { - val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity) + + for((id, polarity) <- toReleaseAsPairs) { + unrollingTime.start + val newClauses = unrollingBank.unlock(id, polarity) + unrollingTime.stop for(ncl <- newClauses) { solver.assertCnstr(toZ3Formula(ncl).get) } - blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*) } + reporter.info(" - finished unrolling") } } @@ -538,6 +541,12 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ } } + totalTime.stop + StopwatchCollections.get("FairZ3 Total") += totalTime + StopwatchCollections.get("FairZ3 Lucky Tests") += luckyTime + StopwatchCollections.get("FairZ3 Z3") += z3Time + StopwatchCollections.get("FairZ3 Unrolling") += unrollingTime + if(forceStop) { None } else { @@ -552,4 +561,3 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ } } - diff --git a/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala b/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala index f5f48403a06855a13a7e55e4c3f3d9382e23f6ff..5ede05a1a461aa192a982e5028122bf1d3669d10 100644 --- a/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala +++ b/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala @@ -60,7 +60,7 @@ object SynthesisBenchmarks extends App { val (results, solver) = pipeline.run(ctx)(file.getPath :: Nil) - val sctx = SynthesisContext(solver, new SilentReporter, new java.util.concurrent.atomic.AtomicBoolean) + val sctx = SynthesisContext(solver, new DefaultReporter, new java.util.concurrent.atomic.AtomicBoolean) for ((f, ps) <- results; p <- ps) { @@ -100,4 +100,16 @@ object SynthesisBenchmarks extends App { println(infoLine("TOTAL", "", tTotal, nAltTotal, nSuccessTotal, nInnapTotal, nDecompTotal)) println(infoFooter) + + println + + val infoHeader2 : String = ". ┌────────────┐\n" + + "╔═╡ Timers ╞" + ("═" * 71) + "╗\n" + + "║ └────────────┘" + (" " * 71) + "║" + + println(infoHeader2) + for ((name, sw) <- StopwatchCollections.getAll.toSeq.sortBy(_._1)) { + println("║ %-70s %10s ms ║".format(name, sw.getMillis)) + } + println(infoFooter) }