Merge fixes for duality

2 files changed, 36 insertions, 10 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 8f6c4503..5b32ced3 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -423,6 +423,12 @@ namespace Microsoft.Boogie.SMTLib
             var labs = line[4];

             var refs = line[5];

             var predName = conseq.Name;

+            {

+                string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!

+                int pos = predName.LastIndexOf(spacer);

+                if (pos >= 0)

+                    predName = predName.Substring(0, pos);

+            }

             RPFP.Node node = null;

             if (!pmap.TryGetValue(predName, out node))

             {

@@ -461,7 +467,7 @@ namespace Microsoft.Boogie.SMTLib
                 return null;

             }

             int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;

-            if(ruleNum < 0 || ruleNum > rpfp.edges.Count)

+            if (ruleNum < 0 || ruleNum > rpfp.edges.Count)

             {

                 HandleProverError("bad rule name from prover: " + refs.ToString());

                 return null;

@@ -489,7 +495,7 @@ namespace Microsoft.Boogie.SMTLib
             varSubst[e.number] = dict;

             foreach (var s in subst.Arguments)

             {

-                if(s.Name != "=" || s.Arguments.Length != 2)

+                if (s.Name != "=" || s.Arguments.Length != 2)

                 {

                     HandleProverError("bad equation from prover: " + s.ToString());

                     return null;

@@ -573,6 +579,7 @@ namespace Microsoft.Boogie.SMTLib
             currentLogFile.Write(common.ToString());

         }

 

+        Push();

         SendThisVC("(fixedpoint-push)");

         foreach (var node in rpfp.nodes)

         {

@@ -588,7 +595,15 @@ namespace Microsoft.Boogie.SMTLib
             string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";

             ruleStrings.Add(ruleString);

         }

-        string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n   :engine duality\n  :print-certificate true\n)";

+        string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n   :engine duality\n  :print-certificate true\n";

+       

+#if true

+        if (CommandLineOptions.Clo.StratifiedInlining != 0)

+            queryString += "    :stratified-inlining true\n";

+        if (CommandLineOptions.Clo.RecursionBound > 0)

+            queryString += "    :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n";

+#endif

+        queryString += ")";

         LineariserOptions.Default.LabelsBelowQuantifiers = false;

         FlushAxioms();

 

@@ -672,6 +687,8 @@ namespace Microsoft.Boogie.SMTLib
 #endif

         }

         SendThisVC("(fixedpoint-pop)");

+        Pop();

+        AxiomsAreSetup = false;

         return result;

     }

 

@@ -806,7 +823,7 @@ namespace Microsoft.Boogie.SMTLib
             if (!options.MultiTraces)

               posLabels = Enumerable.Empty<string>();

             var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();

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

+            string expr;

             if (!conjuncts.Any())

             {

               expr = "false";

@@ -967,7 +984,7 @@ namespace Microsoft.Boogie.SMTLib
                 result = Outcome.OutOfMemory;

                 Process.NeedsRestart = true;

                 break;

-              case "timeout":

+                case "timeout": case "canceled":

                 currentErrorHandler.OnResourceExceeded("timeout");

                 result = Outcome.TimeOut;

                 break;

@@ -1162,7 +1179,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public override void SetTimeOut(int ms)

     {

-        SendThisVC("(set-option :SOFT_TIMEOUT " + ms.ToString() + ")\n");

+        SendThisVC("(set-option " + Z3.SetTimeoutOption() + "  " + ms.ToString() + ")\n");

     }

 

     public override object Evaluate(VCExpr expr)

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 81d5d5d1..bc9e6992 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -187,6 +187,16 @@ namespace Microsoft.Boogie.SMTLib
             minor = Z3MinorVersion;

         }

 

+        public static string SetTimeoutOption()

+        {

+            int major, minor;

+            GetVersion(out major, out minor);

+            if (major > 4 || major == 4 && minor >= 3)

+                return "TIMEOUT";

+            else

+                return "SOFT_TIMEOUT";

+        }

+

         // options that work only on the command line

         static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };

 

@@ -251,7 +261,7 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (options.TimeLimit > 0)

                 {

-                    options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

+                    options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());

                     // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

                     // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

                 }

@@ -261,9 +271,8 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (CommandLineOptions.Clo.WeakArrayTheory)

                 {

-                    // TODO: these options don't seem to exist in recent Z3

-                    // options.AddWeakSmtOption("ARRAY_WEAK", "true");

-                    // options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");

+                    options.AddWeakSmtOption("smt.array.weak", "true");

+                    options.AddWeakSmtOption("smt.array.extensional", "false");

                 } 

             }

             else