Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)

6 files changed, 37 insertions, 21 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index b0269d2e..b46ba916 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -322,20 +322,33 @@ namespace Microsoft.Boogie.SMTLib
         var globalResult = Outcome.Undetermined;

 

         while (errorsLeft-- > 0) {

-          string negLabel = null;

+          string[] labels = null;

 

           result = GetResponse();

           if (globalResult == Outcome.Undetermined)

             globalResult = result;

 

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

-            negLabel = GetLabelsInfo(handler);

+            labels = GetLabelsInfo(handler);

           }

 

-          if (negLabel == null) break;

+          if (labels == null) break;

 

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

-          SendThisVC("(check-sat)");

+          var negLabels = labels.Where(l => l.StartsWith("@")).ToArray();

+          var posLabels = labels.Where(l => !l.StartsWith("@"));

+          Func<string,string> lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s));

+          if (negLabels.Length != 1) {

+            HandleProverError("Wrong number of negative labels: " + negLabels.Length);

+            break;

+          } else {

+            if (!options.MultiTraces)

+              posLabels = Enumerable.Empty<string>();

+            var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat1(lbl(negLabels[0])).ToArray();

+            var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");

+            SendThisVC("(assert " + expr + ")");

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

+          }

+          

         }

 

         SendThisVC("(pop 1)");

@@ -348,16 +361,16 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

-    private string GetLabelsInfo(ErrorHandler handler)

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

+      string[] res = null;

 

       while (true) {

         var resp = Process.GetProverResponse();

@@ -365,11 +378,9 @@ namespace Microsoft.Boogie.SMTLib
           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("@"));

+          res = labels;

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

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

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

           var modelStr = resp[0].Name;

           List<Model> models = null;

@@ -397,7 +408,7 @@ namespace Microsoft.Boogie.SMTLib
         handler.OnModel(labelNums, m);

       }

 

-      return negLabel;

+      return res;

     }

 

     private Outcome GetResponse()

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 4884b44f..35c4d5f0 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -511,12 +511,11 @@ namespace Microsoft.Boogie.SMTLib
           wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

         }

 

-        if (!op.pos)

-          wr.Write("(or {0} ", SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(op.label)));

+        wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label)));

             

         ExprLineariser.Linearise(node[0], options);

 

-        if (!op.pos) wr.Write(")");

+        wr.Write(")");

 

         if (ExprLineariser.ProverOptions.UseLabels)

           wr.Write(")");

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 600d6e51..e669e407 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -95,9 +95,9 @@ namespace Microsoft.Boogie.SMTLib
       return s;

     }

 

-    public static string BlockedLabel(string s)

+    public static string LabelVar(string s)

     {

-      return "%block%" + s;

+      return "%lbl%" + s;

     }

 

     public static string QuoteId(string s)

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 76bce71c..44f91cc2 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -33,6 +33,7 @@ namespace Microsoft.Boogie.SMTLib
     public bool UseLabels { get { return UseZ3; } }

     public List<OptionValue> SmtOptions = new List<OptionValue>();

     public List<string> SolverArguments = new List<string>();

+    public bool MultiTraces = false;

 

     // Z3 specific (at the moment; some of them make sense also for other provers)

     public bool UseZ3 = true;

@@ -86,6 +87,7 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       return

+        ParseBool(opt, "MULTI_TRACES", ref MultiTraces) ||

         ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||

         ParseBool(opt, "USE_Z3", ref UseZ3) ||

         ParseString(opt, "INSPECTOR", ref Inspector) ||

@@ -115,6 +117,7 @@ C:<string>                Pass <string> to the SMT on the command line.
 

 Z3-specific options:

 ~~~~~~~~~~~~~~~~~~~~

+MULTI_TRACES=<bool>       Report errors with multiple paths leading to the same assertion.

 INSPECTOR=<string>        Use the specified Z3Inspector binary.

 OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.

 USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (default: true)

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 60527ae8..96f16366 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -55,7 +55,7 @@ void ObjectInvariant()
     private readonly Dictionary<Type/*!*/, bool>/*!*/ KnownTypes = new Dictionary<Type, bool>();

     private readonly Dictionary<string/*!*/, bool>/*!*/ KnownStoreFunctions = new Dictionary<string, bool>();

     private readonly Dictionary<string/*!*/, bool>/*!*/ KnownSelectFunctions = new Dictionary<string, bool>();

-    private readonly HashSet<string> KnownLBLNEG = new HashSet<string>();

+    private readonly HashSet<string> KnownLBL = new HashSet<string>();

 

 

     public List<string/*!>!*/> AllDeclarations { get {

@@ -124,9 +124,9 @@ void ObjectInvariant()
           KnownFunctions.Add(f, true);

         } else {

           var lab = node.Op as VCExprLabelOp;

-          if (lab != null && !lab.pos && !KnownLBLNEG.Contains(lab.label)) {

-            KnownLBLNEG.Add(lab.label);

-            var name = SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(lab.label));

+          if (lab != null && !KnownLBL.Contains(lab.label)) {

+            KnownLBL.Add(lab.label);

+            var name = SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(lab.label));

             AddDeclaration("(declare-fun " + name + " () Bool)");

           }

         }

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 74af2b84..27d86915 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -161,6 +161,9 @@ namespace Microsoft.Boogie.SMTLib
         options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

 

       // legacy option handling

+      if (!CommandLineOptions.Clo.z3AtFlag)

+        options.MultiTraces = true;

+

       foreach (string opt in CommandLineOptions.Clo.Z3Options) {

         Contract.Assert(opt != null);

         int eq = opt.IndexOf("=");