From 9f2b3b64b05d69603ddb222a62b9ed24e4496dab Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 18 Feb 2011 22:05:56 +0000
Subject: Allow use ErrorModel as a container for Model - make -mv work with
 SMTLib on Z3

---
 Source/Provers/SMTLib/ProverInterface.cs | 72 ++++++++++++++++++++++++--------
 Source/Provers/SMTLib/SMTLib.csproj      |  4 ++
 2 files changed, 59 insertions(+), 17 deletions(-)

(limited to 'Source/Provers')

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>
-- 
cgit v1.2.3