Improve logging when -proverOpt:VERBOSITY=1 or 2 is specified

1 files changed, 25 insertions, 9 deletions

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);

         }