Stopwatch in package purescala

cp-demo/RedBlackTree.scala

 import cp.Definitions._
-import cp.Utils._
+import purescala.Stopwatch
 
 object RedBlackTree { 
   @spec sealed abstract class Color
@@ -96,12 +96,12 @@ object RedBlackTree {
 
     val solutionSet = scala.collection.mutable.Set[Tree]()
     println("Fixing size of trees to " + (bound))
-    val timer = new Timer("Fixed-size enumeration", true)
-    timer.start
+    val sw = new Stopwatch("Fixed-size enumeration", false)
+    sw.start
     for (tree <- findAll((t : Tree) => isRedBlackTree(t) && boundValues(t, bound - 1) && size(t) == bound)) {
       solutionSet += tree
     }
-    timer.stop
+    sw.stop
 
     // for (tree <- solutionSet)
     //   println(print(tree) + "\n-----------\n")

src/cp/RuntimeMethods.scala

@@ -11,8 +11,10 @@ object RuntimeMethods {
   import purescala.{DefaultReporter,QuietReporter}
   import purescala.FairZ3Solver
 
-  private def newReporter() = new QuietReporter()
-  // private def newReporter() = new DefaultReporter()
+  import purescala.Stopwatch
+  
+  private val silent = true
+  private def newReporter() = if (silent) new QuietReporter() else new DefaultReporter()
   private def newSolver() = new FairZ3Solver(newReporter())
 
   def chooseExec(progString : String, progId : Int, exprString : String, exprId : Int, outputVarsString : String, outputVarsId : Int, inputConstraints : Expr) : Seq[Expr] = {
@@ -325,7 +327,9 @@ object RuntimeMethods {
       override def hasNext : Boolean = nextModel match {
         case None => 
           // Check whether there are any more models
+          val stopwatch = new Stopwatch("hasNext", true).start
           val (outcome, model) = solver.decideWithModel(toCheck, false)
+          stopwatch.stop
           val toReturn = (outcome match {
             case Some(false) =>
               // there is a solution, we need to complete model for nonmentioned variables
@@ -362,7 +366,9 @@ object RuntimeMethods {
       override def next() : Map[Identifier, Expr] = nextModel match {
         case None => {
           // Let's compute the next model
+          val stopwatch = new Stopwatch("next", true).start
           val (outcome, model) = solver.decideWithModel(toCheck, false)
+          stopwatch.stop
           val toReturn = (outcome match {
             case Some(false) =>
               // there is a solution, we need to complete model for nonmentioned variables

src/cp/Utils.scala

-package cp
-
-object Utils {
-  class Timer(description : String, verbose : Boolean = false) {
-    var beginning: Long = 0L
-    var end: Long = 0L
-    def start = {
-      beginning = System.currentTimeMillis
-    }
-    def stop : Double = {
-      end = System.currentTimeMillis
-      val seconds = (end - beginning) / 1000.0
-      if (verbose) println("Timer \"" + description + "\": " + seconds + " s")
-      seconds
-    }
-  }
-}

src/purescala/FairZ3Solver.scala

@@ -326,7 +326,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
         println(blockingSetAsZ3)
         z3.checkAssumptions(blockingSetAsZ3 : _*)
       } else {
+        val stopwatch = new Stopwatch("Z3 search", true).start
         val (a, m) = z3.checkAndGetModel()
+        stopwatch.stop
         (a, m, Seq.empty[Z3AST])
       }
 

src/purescala/Stopwatch.scala

+package purescala
+
+/** Implements a stopwatch for profiling purposes */
+class Stopwatch(description : String, verbose : Boolean = false) {
+  var beginning: Long = 0L
+  var end: Long = 0L
+  def start : Stopwatch = {
+    beginning = System.currentTimeMillis
+    this
+  }
+  def stop : Double = {
+    end = System.currentTimeMillis
+    val seconds = (end - beginning) / 1000.0
+    if (verbose) println("Stopwatch \"" + description + "\": " + seconds + " s")
+    seconds
+  }
+}