merge

4 files changed, 72 insertions, 16 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index eaa42b38..4cb85435 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -395,6 +395,21 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();

     }

 

+    public override void Reset()

+    {

+      SendThisVC("(reset)");

+      Process.Send(common.ToString());

+    }

+

+    public override void FullReset()

+    {

+      SendThisVC("(reset)");

+      common.Clear();

+      AxiomsAreSetup = false;

+      ctx.Clear();

+      DeclCollector.Reset();

+    }

+

     private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, 

                                  Dictionary<int,Dictionary<string,string>> varSubst)

     {

@@ -423,6 +438,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 +482,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 +510,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 +594,7 @@ namespace Microsoft.Boogie.SMTLib
             currentLogFile.Write(common.ToString());

         }

 

+        Push();

         SendThisVC("(fixedpoint-push)");

         foreach (var node in rpfp.nodes)

         {

@@ -588,7 +610,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 +702,8 @@ namespace Microsoft.Boogie.SMTLib
 #endif

         }

         SendThisVC("(fixedpoint-pop)");

+        Pop();

+        AxiomsAreSetup = false;

         return result;

     }

 

@@ -806,7 +838,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 = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); ;

             if (!conjuncts.Any())

             {

               expr = "false";

@@ -983,7 +1015,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;

@@ -1178,7 +1210,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() + ")");

     }

 

     public override object Evaluate(VCExpr expr)

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index f4fa5e75..2374a157 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -63,12 +63,14 @@ namespace Microsoft.Boogie.SMTLib
 

 

       try {

-        prover = Process.Start(psi);

+        prover = new Process();

+        prover.StartInfo = psi;        

         prover.ErrorDataReceived += prover_ErrorDataReceived;

-        prover.OutputDataReceived += prover_OutputDataReceived;        

-        prover.BeginErrorReadLine();

-        prover.BeginOutputReadLine();

+        prover.OutputDataReceived += prover_OutputDataReceived;

+        prover.Start();

         toProver = prover.StandardInput;

+        prover.BeginErrorReadLine();

+        prover.BeginOutputReadLine();        

       } catch (System.ComponentModel.Win32Exception e) {

         throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));

       }

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 9d908138..2bbe4978 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -101,6 +101,19 @@ void ObjectInvariant()
         _KnownLBL.Push(new HashSet<string>());

     }

 

+    public void Reset()

+    {

+      _KnownFunctions.Clear();

+      _KnownVariables.Clear();

+      _KnownTypes.Clear();

+      _KnownStoreFunctions.Clear();

+      _KnownSelectFunctions.Clear();

+      _KnownLBL.Clear();

+      AllDecls.Clear();

+      IncDecls.Clear();

+      InitializeKnownDecls();

+    }

+

     public void Push()

     {

         Contract.Assert(_KnownFunctions.Count > 0);

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 04bdc0df..66b1809a 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -160,10 +160,10 @@ namespace Microsoft.Boogie.SMTLib
                 proc.StartInfo.UseShellExecute = false;

                 proc.StartInfo.CreateNoWindow = true;

                 proc.Start();

+                string answer = proc.StandardOutput.ReadToEnd();

                 proc.WaitForExit();

                 if (proc.ExitCode == 0)

-                {

-                    string answer = proc.StandardOutput.ReadToEnd();

+                {                    

                     var firstdot = answer.IndexOf('.');

                     if (firstdot >= 0)

                     {

@@ -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