From 4b1eae86e95f1599999a0d4ce01efd56ffcb3e99 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Fri, 21 Oct 2011 17:12:53 -0700
Subject: Improve logging when -proverOpt:VERBOSITY=1 or 2 is specified

---
 Source/Provers/SMTLib/SMTLibProcess.cs | 34 +++++++++++++++++++++++++---------
 1 file changed, 25 insertions(+), 9 deletions(-)

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index cea598b0..2b2d3f94 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -23,6 +23,8 @@ namespace Microsoft.Boogie.SMTLib
     readonly Queue<string> proverOutput = new Queue<string>();
     readonly Queue<string> proverErrors = new Queue<string>();
     readonly TextWriter toProver;
+    readonly int smtProcessId;
+    static int smtProcessIdSeq = 0;
     ConsoleCancelEventHandler cancelEvent;
 
     public static ProcessStartInfo ComputerProcessStartInfo(string executable, string options)
@@ -40,6 +42,7 @@ namespace Microsoft.Boogie.SMTLib
     public SMTLibProcess(ProcessStartInfo psi, SMTLibProverOptions options)
     {
       this.options = options;
+      this.smtProcessId = smtProcessIdSeq++;
 
       if (options.Inspector != null) {
         this.inspector = new Inspector(options);
@@ -53,6 +56,11 @@ namespace Microsoft.Boogie.SMTLib
         Console.CancelKeyPress += cancelEvent;
       }
 
+      if (options.Verbosity >= 1) {
+        Console.WriteLine("[SMT-{0}] Starting {1} {2}", smtProcessId, psi.FileName, psi.Arguments);
+      }
+
+
       try {
         prover = Process.Start(psi);
         prover.ErrorDataReceived += prover_ErrorDataReceived;
@@ -80,7 +88,7 @@ namespace Microsoft.Boogie.SMTLib
         if (log.Length > 50)
           log = log.Substring(0, 50) + "...";
         log = log.Replace("\r", "").Replace("\n", " ");
-        Console.WriteLine("[SMT-INP] {0}", log);
+        Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
       }
       toProver.WriteLine(cmd);
     }
@@ -102,14 +110,14 @@ namespace Microsoft.Boogie.SMTLib
       while (true) {
         var sx = GetProverResponse();
         if (sx == null) {
-          ErrorHandler("Prover died");
+          HandleError("Prover died");
           return;
         }
 
         if (IsPong(sx))
           return;
         else
-          ErrorHandler("Invalid PING response from the prover: " + sx.ToString());
+          HandleError("Invalid PING response from the prover: " + sx.ToString());
       }
     }
 
@@ -130,9 +138,9 @@ namespace Microsoft.Boogie.SMTLib
         var resp = exprs[0];
         if (resp.Name == "error") {
           if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId)
-            ErrorHandler(resp.Arguments[0].Name);
+            HandleError(resp.Arguments[0].Name);
           else
-            ErrorHandler(resp.ToString());
+            HandleError(resp.ToString());
         } else if (resp.Name == "progress") {
           if (inspector != null) {
             var sb = new StringBuilder();
@@ -170,6 +178,14 @@ namespace Microsoft.Boogie.SMTLib
     public event Action<string> ErrorHandler;
     int errorCnt;
 
+    private void HandleError(string msg)
+    {
+      if (options.Verbosity >= 2)
+        Console.WriteLine("[SMT-ERR-{0}] Handling error: {1}", smtProcessId, msg);
+      if (ErrorHandler != null)
+        ErrorHandler(msg);
+    }
+
     #region SExpr parsing
     int linePos;
     string currLine;
@@ -239,7 +255,7 @@ namespace Microsoft.Boogie.SMTLib
 
     void ParseError(string msg)
     {
-      ErrorHandler("Error parsing prover output: " + msg);
+      HandleError("Error parsing prover output: " + msg);
     }
 
     IEnumerable<SExpr> ParseSExprs(bool top)
@@ -294,7 +310,7 @@ namespace Microsoft.Boogie.SMTLib
       string error = null;
       while (true) {
         if (error != null) {
-          ErrorHandler(error);
+          HandleError(error);
           errorCnt++;
           error = null;
         }
@@ -334,7 +350,7 @@ namespace Microsoft.Boogie.SMTLib
       lock (this) {
         if (e.Data != null) {
           if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) {
-            Console.WriteLine("[SMT-OUT] {0}", e.Data);
+            Console.WriteLine("[SMT-OUT-{0}] {1}", smtProcessId, e.Data);
           }
           proverOutput.Enqueue(e.Data);
           Monitor.Pulse(this);
@@ -347,7 +363,7 @@ namespace Microsoft.Boogie.SMTLib
       lock (this) {
         if (e.Data != null) {
           if (options.Verbosity >= 1)
-            Console.WriteLine("[SMT-ERR] {0}", e.Data);
+            Console.WriteLine("[SMT-ERR-{0}] {1}", smtProcessId, e.Data);
           proverErrors.Enqueue(e.Data);
           Monitor.Pulse(this);
         }
-- 
cgit v1.2.3