From 669abe4057d8c04b1e75bd6bd3372437fb32c01c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Mon, 25 Apr 2011 15:53:20 +0000
Subject: [PATCH] Some detailed profiling for fair solver
---
cp-demo/RedBlackTree.scala | 3 ++-
src/purescala/FairZ3Solver.scala | 11 +++++++++++
src/purescala/Stopwatch.scala | 15 ++++++++++++++-
3 files changed, 27 insertions(+), 2 deletions(-)
diff --git a/cp-demo/RedBlackTree.scala b/cp-demo/RedBlackTree.scala
index 46d611b73..d787a0c0c 100644
--- a/cp-demo/RedBlackTree.scala
+++ b/cp-demo/RedBlackTree.scala
@@ -46,7 +46,7 @@ object RedBlackTree {
}
@spec def blackHeight(t : Tree) : Int = t match {
- case Empty() => 1
+ case Empty() => 0
case Node(Black(), l, _, _) => blackHeight(l) + 1
case Node(Red(), l, _, _) => blackHeight(l)
}
@@ -106,6 +106,7 @@ object RedBlackTree {
// for (tree <- solutionSet)
// println(print(tree) + "\n-----------\n")
println("Fixed-size solution set size : " + solutionSet.size)
+ Stopwatch.printSummary
}
def enumerateAllUpTo(bound : Int) : Unit = {
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 2e61161ab..9adb24518 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -254,6 +254,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
def decideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
+ val initializationStopwatch = new Stopwatch("decideWithModel init", true).start
var forceStop : Boolean = false
var foundDefinitiveAnswer : Boolean = false
@@ -307,12 +308,16 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
var iterationsLeft : Int = if(Settings.unrollingLevel > 0) Settings.unrollingLevel else 16121984
+ initializationStopwatch.stop
while(!foundDefinitiveAnswer && !forceStop) {
iterationsLeft -= 1
+ val blocking2Z3Stopwatch = new Stopwatch("Blocking to Z3 conv").start
val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.map(toZ3Formula(z3, _).get).toSeq
// println("Blocking set : " + blockingSet)
+ blocking2Z3Stopwatch.stop
+ val assertBlockingStopwatch = new Stopwatch("Assert blocking set").start
if(Settings.useCores) {
// NOOP
} else {
@@ -320,6 +325,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
if(!blockingSetAsZ3.isEmpty)
z3.assertCnstr(z3.mkAnd(blockingSetAsZ3 : _*))
}
+ assertBlockingStopwatch.stop
reporter.info(" - Running Z3 search...")
val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
@@ -379,7 +385,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
if(!Settings.useCores) {
z3.pop(1)
+ val stopwatch = new Stopwatch("Second Z3 search", true).start
val (result2,m2) = z3.checkAndGetModel()
+ stopwatch.stop
if (result2 == Some(false)) {
foundAnswer(Some(true))
@@ -399,6 +407,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
if(!foundDefinitiveAnswer) {
reporter.info("- We need to keep going.")
+ val unrollingStopwatch = new Stopwatch("Unrolling", true).start
+
val toRelease : Set[Expr] = if(Settings.useCores) {
core.map(ast => fromZ3Formula(ast) match {
case n @ Not(Variable(_)) => n
@@ -470,6 +480,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
//z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
+ unrollingStopwatch.stop
}
}
}
diff --git a/src/purescala/Stopwatch.scala b/src/purescala/Stopwatch.scala
index 86823fcbe..ee71110f5 100644
--- a/src/purescala/Stopwatch.scala
+++ b/src/purescala/Stopwatch.scala
@@ -11,7 +11,20 @@ class Stopwatch(description : String, verbose : Boolean = false) {
def stop : Double = {
end = System.currentTimeMillis
val seconds = (end - beginning) / 1000.0
- if (verbose) println("Stopwatch \"" + description + "\": " + seconds + " s")
+ if (verbose) println("Stopwatch %-25s: %-3.3fs" format (description, seconds))
+ Stopwatch.timeLog +=
+ (description -> (Stopwatch.timeLog.getOrElse(description, Nil) :+ seconds))
seconds
}
}
+
+object Stopwatch {
+ val timeLog = scala.collection.mutable.Map[String, Seq[Double]]()
+
+ def printSummary : Unit = {
+ val toPrint = timeLog.map{case (k, v) => ("%-25s" format k, v.foldLeft(0.0){case (a, b) => a + b})}.mkString("\n")
+
+ println("Total times per stopwatch description")
+ println(toPrint)
+ }
+}
--
GitLab