Read prover responses; handle labels

3 files changed, 59 insertions, 6 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 8f1542ce..bfcbf682 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -9,6 +9,7 @@ using System.Collections.Generic;
 using System.Threading;

 using System.IO;

 //using ExternalProver;

+using System.Linq;

 using System.Diagnostics;

 using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

@@ -207,6 +208,13 @@ VERBOSITY=<int>           1 - print prover output (default: 0)
       }

     }

 

+    private void FlushLogFile()

+    {

+      if (currentLogFile != null) {

+        currentLogFile.Flush();

+      }

+    }

+

     public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)

     {

       //Contract.Requires(descriptiveName != null);

@@ -229,12 +237,13 @@ VERBOSITY=<int>           1 - print prover output (default: 0)
       SendThisVC("(push)");

       SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");

       SendThisVC(vcString);

+      FlushLogFile();

 

       if (Process != null)

         Process.PingPong(); // flush any errors

 

       SendThisVC("(check-sat)");

-      SendThisVC("(pop 1)");

+      FlushLogFile();

     }

 

     private TextWriter OpenOutputFile(string descriptiveName)

@@ -259,14 +268,53 @@ VERBOSITY=<int>           1 - print prover output (default: 0)
     public override Outcome CheckOutcome(ErrorHandler handler)

     {  //Contract.Requires(handler != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

-

+      

       var result = Outcome.Undetermined;

 

       if (Process == null)

         return result;

 

+      var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;

+      var globalResult = Outcome.Undetermined;

+

+      while (errorsLeft-- > 0) {

+        var seenLabels = false;

+

+        result = GetResponse();

+        if (globalResult == Outcome.Undetermined)

+          globalResult = result;

+

+        if (result == Outcome.Invalid && options.UseZ3) {

+          SendThisVC("(get-info :labels)");

+          Process.Ping();

+

+          while (true) {

+            var resp = Process.GetProverResponse();

+            if (resp == null || Process.IsPong(resp))

+              break;

+            if (resp.Name == ":labels" && resp.ArgCount >= 1) {

+              var labels = resp[0].Arguments.Select(a => a.Name.Replace("|", "").Replace("@", "").Replace("+", "")).ToList();

+              handler.OnModel(labels, null);

+              seenLabels = true;

+            }

+          }

+        }

+

+        if (!seenLabels) break;

+        SendThisVC("(next-sat)");

+      }

+

+      SendThisVC("(pop 1)");

+      FlushLogFile();

+

+      return globalResult;

+    }

+

+    private Outcome GetResponse()

+    {

+      var result = Outcome.Undetermined;

+

       Process.Ping();

-      

 

       while (true) {

         var resp = Process.GetProverResponse();

@@ -286,7 +334,6 @@ VERBOSITY=<int>           1 - print prover output (default: 0)
             break;

         }

       }

-

       return result;

     }

 

diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs
index 2d143830..d9d05f85 100644
--- a/Source/Provers/SMTLib/SExpr.cs
+++ b/Source/Provers/SMTLib/SExpr.cs
@@ -37,6 +37,11 @@ namespace Microsoft.Boogie
       }

     }

 

+    public int ArgCount

+    {

+      get { return arguments.Length; }

+    }

+

     public bool IsId

     {

       get { return Arguments.Length == 0; }

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4a631960..8cc67256 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -71,7 +71,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public bool IsPong(SExpr sx)

     {

-      return sx.Name == "" && sx.Arguments.Length == 1 && sx.Arguments[0].Name.Contains("name");

+      return sx.Name == ":name";

     }

 

     public void PingPong()

@@ -261,8 +261,9 @@ namespace Microsoft.Boogie.SMTLib
     void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

-        if (options.Verbosity >= 1)

+        if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name"))) {

           Console.WriteLine("[SMT-OUT] {0}", e.Data);

+        }

         proverOutput.Enqueue(e.Data);

         Monitor.Pulse(this);

       }