options to reduce the output to a single line

src/main/scala/leon/Analysis.scala

@@ -151,6 +151,14 @@ class Analysis(val program : Program, val reporter: Reporter = Settings.reporter
       )
       reporter.info(summaryString)
 
+      if(Settings.simpleOutput) {
+        val outStr =
+          if(vcs.forall(_.status == "valid")) "valid" 
+          else if(vcs.exists(_.status == "invalid")) "invalid"
+          else "unknown"
+        println(outStr)
+      }
+
       // Printing summary for the evaluation section of paper:
       val writeSummary = false
       if (writeSummary) {

src/main/scala/leon/Reporter.scala

@@ -28,7 +28,8 @@ class DefaultReporter extends Reporter {
   protected val fatalPfx   = "[ Fatal ] "
 
   def output(msg: String) : Unit = {
-    /*Console.err.*/println(msg)
+    if(!Settings.simpleOutput)
+      println(msg)
   }
 
   protected def reline(pfx: String, msg: String) : String = {

src/main/scala/leon/Settings.scala

@@ -26,4 +26,5 @@ object Settings {
   var bitvectorBitwidth : Option[Int] = None
   var debugLevel: Int = 0
   var debugTags: Set[String] = Set.empty
+  var simpleOutput: Boolean = false
 }

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

@@ -42,7 +42,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
     "  --noLuckyTests       Do not perform additional tests to potentially find models early" + "\n" +
     "  --noverifymodel      Do not verify the correctness of models returned by Z3" + "\n" +
     "  --debug=[1-5]        Debug level" + "\n" +
-    "  --tags=t1:...        Filter out debug information that are not of one of the given tags"
+    "  --tags=t1:...        Filter out debug information that are not of one of the given tags" + "\n" +
+    "  --oneline            Reduce the output to a single line: valid if all properties were valid, invalid if at least one is invalid, unknown else"
   )
 
   /** Processes the command-line options. */
@@ -50,22 +51,24 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
   override def processOptions(options: List[String], error: String => Unit) {
     for(option <- options) {
       option match {
-        case "with-code"  =>                     stopAfterAnalysis = false
-        case "uniqid"     =>                     leon.Settings.showIDs = true
-        case "parse"      =>                     stopAfterExtraction = true
-        case "tolerant"   =>                     silentlyTolerateNonPureBodies = true
-        case "nodefaults" =>                     leon.Settings.runDefaultExtensions = false
-        case "axioms"     =>                     leon.Settings.noForallAxioms = false
-        case "bapa"       =>                     leon.Settings.useBAPA = true
-        case "impure"     =>                     leon.Settings.impureTestcases = true
-        case "XP"         =>                     leon.Settings.experimental = true
-        case "BV"         =>                     leon.Settings.bitvectorBitwidth = Some(32)
-        case "prune"      =>                     leon.Settings.pruneBranches = true
-        case "cores"      =>                     leon.Settings.useCores = true
-        case "quickcheck" =>                     leon.Settings.useQuickCheck = true
-        case "parallel"   =>                     leon.Settings.useParallel = true
-        case "noLuckyTests" =>                   leon.Settings.luckyTest = false
-        case "noverifymodel" =>                  leon.Settings.verifyModel = false
+        case "with-code"     =>                     stopAfterAnalysis = false
+        case "uniqid"        =>                     leon.Settings.showIDs = true
+        case "parse"         =>                     stopAfterExtraction = true
+        case "tolerant"      =>                     silentlyTolerateNonPureBodies = true
+        case "nodefaults"    =>                     leon.Settings.runDefaultExtensions = false
+        case "axioms"        =>                     leon.Settings.noForallAxioms = false
+        case "bapa"          =>                     leon.Settings.useBAPA = true
+        case "impure"        =>                     leon.Settings.impureTestcases = true
+        case "XP"            =>                     leon.Settings.experimental = true
+        case "BV"            =>                     leon.Settings.bitvectorBitwidth = Some(32)
+        case "prune"         =>                     leon.Settings.pruneBranches = true
+        case "cores"         =>                     leon.Settings.useCores = true
+        case "quickcheck"    =>                     leon.Settings.useQuickCheck = true
+        case "parallel"      =>                     leon.Settings.useParallel = true
+        case "oneline"       =>                     leon.Settings.simpleOutput = true
+        case "noLuckyTests"  =>                     leon.Settings.luckyTest = false
+        case "noverifymodel" =>                     leon.Settings.verifyModel = false
+
         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 }