Merge branch 'debug' into leon2

Conflicts:
	src/main/scala/leon/Main.scala
	src/main/scala/leon/PassManager.scala
	src/main/scala/leon/plugin/LeonPlugin.scala

src/main/scala/leon/Logger.scala

+package leon
+
+object Logger {
+
+  //the debug level to display, from 0 (no debug information) to 5 (very verbose)
+  //var level = 0
+
+  //each debug information is tagged by a string, the tag variable only display the message with a tag in this set
+  //if the set is empty then all tags are displayed
+  //var tags: Set[String] = Set()
+
+  val defaultTag = "main"
+
+  private def output(msg: String, lvl: Int, tag: String) {
+    if(lvl <= Settings.debugLevel) {
+      if(Settings.debugTags.isEmpty || Settings.debugTags.contains(tag)) {
+        println("DEBUG: [" + tag + "] " + msg)
+      }
+    }
+  }
+
+  def debug(msg: String, lvl: Int, tag: String = defaultTag) = output(msg, lvl, tag)
+
+}

src/main/scala/leon/Main.scala

@@ -31,6 +31,7 @@ object Main {
   }
 
   private def defaultAction(program: Program, reporter: Reporter) : Unit = {
+    Logger.debug("Default action on program: " + program, 5, "main")
     val passManager = new PassManager(Seq(EpsilonElimination, ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
     val program2 = passManager.run(program)
     val analysis = new Analysis(program2, reporter)

src/main/scala/leon/PassManager.scala

@@ -6,9 +6,9 @@ class PassManager(passes: Seq[Pass]) {
 
   def run(program: Program): Program = {
     passes.foldLeft(program)((pgm, pass) => {
-      println("Running Pass: " + pass.description)
+      Logger.debug("Running Pass: " + pass.description, 1, "passman")
       val newPgm = pass(pgm)
-      println("Resulting program: " + newPgm)
+      Logger.debug("Resulting program: " + newPgm, 5, "passman")
       newPgm
     })
   }

src/main/scala/leon/Settings.scala

@@ -24,5 +24,6 @@ object Settings {
   var useParallel : Boolean = false
   // When this is None, use real integers
   var bitvectorBitwidth : Option[Int] = None
-  var verbose : Boolean = false
+  var debugLevel: Int = 0
+  var debugTags: Set[String] = Set.empty
 }

src/main/scala/leon/plugin/LeonPlugin.scala

@@ -41,7 +41,9 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
     "  --parallel           Run all solvers in parallel" + "\n" +
     "  --noLuckyTests       Do not perform additional tests to potentially find models early" + "\n" +
     "  --noverifymodel      Do not verify the correctness of models returned by Z3" + "\n" +
-    "  --verbose            Print debugging informations"
+    "  --verbose            Print debugging informations" + "\n" +
+    "  --debug=[1-5]        Debug level" + "\n" +
+    "  --tags=t1:...        Filter out debug information that are not of one of the given tags"
   )
 
   /** Processes the command-line options. */
@@ -66,6 +68,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
         case "noLuckyTests" =>                   leon.Settings.luckyTest = false
         case "noverifymodel" =>                  leon.Settings.verifyModel = false
         case "verbose"    =>                     leon.Settings.verbose = true
+        case s if s.startsWith("debug=") =>       leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
+        case s if s.startsWith("tags=") =>       leon.Settings.debugTags = Set(splitList(s.substring("tags=".length, s.length)): _*)
         case s if s.startsWith("unrolling=") =>  leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
         case s if s.startsWith("functions=") =>  leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
         case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))