Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3

2 files changed, 59 insertions, 17 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 54e5524a..854c97ea 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -146,7 +146,7 @@ namespace Microsoft.Boogie.SMTLib
         SendCommon("(set-option :print-success false)");

         SendCommon("(set-info :smt-lib-version 2.0)");

         if (options.ExpectingModel())

-          SendCommon("(set-option :produce-proofs true)");

+          SendCommon("(set-option :produce-models true)");

         foreach (var opt in options.SmtOptions) {

           SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

         }

@@ -301,25 +301,11 @@ namespace Microsoft.Boogie.SMTLib
             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("|", "")).ToArray();

-                negLabel = labels.FirstOrDefault(l => l.StartsWith("@"));

-                var labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

-                handler.OnModel(labelNums, null);

-                if (negLabel == null)

-                  HandleProverError("No negative label in: " + labels.Concat(" "));

-              }

-            }

+            negLabel = GetLabelsInfo(handler);

           }

 

           if (negLabel == null) break;

+

           SendThisVC("(assert " + SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(negLabel)) + ")");

           SendThisVC("(check-sat)");

         }

@@ -334,6 +320,58 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    private string GetLabelsInfo(ErrorHandler handler)

+    {

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

+      if (options.ExpectingModel())

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

+      Process.Ping();

+

+      string negLabel = null;

+      List<string> labelNums = null;

+      Model theModel = null;

+

+      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("|", "")).ToArray();

+          negLabel = labels.FirstOrDefault(l => l.StartsWith("@"));

+          if (labelNums != null) HandleProverError("Got multiple :labels responses");

+          labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();          

+          if (negLabel == null)

+            HandleProverError("No negative label in: " + labels.Concat(" "));

+        } else if (resp.Name == ":model" && resp.ArgCount >= 1) {

+          var modelStr = resp[0].Name;

+          List<Model> models = null;

+          try {

+            models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));

+          } catch (ArgumentException exn) {

+            HandleProverError("Model parsing error: " + exn.Message);

+          }

+

+          if (models != null) {

+            if (models.Count == 0) HandleProverError("Could not parse any models");

+            else {

+              if (models.Count > 1) HandleProverError("Expecting only one model, got multiple");

+              if (theModel != null) HandleProverError("Got multiple :model responses");

+              theModel = models[0];

+            }

+          }

+        }

+      }

+

+      if (labelNums != null) {

+        ErrorModel m = null;

+        if (theModel != null)

+          m = new ErrorModel(theModel);

+        handler.OnModel(labelNums, m);

+      }

+

+      return negLabel;

+    }

+

     private Outcome GetResponse()

     {

       var result = Outcome.Undetermined;

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 4eb753a2..6a776d6a 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -134,6 +134,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\..\Model\Model.csproj">

+      <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

+      <Name>Model</Name>

+    </ProjectReference>

     <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">

       <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>