Improve support for diagnosing timeouts.

1 files changed, 100 insertions, 108 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e4691a4b..ac804b31 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -30,8 +30,6 @@ namespace Microsoft.Boogie.SMTLib
     private readonly SMTLibProverOptions options;

     private bool usingUnsatCore;

     private RPFP rpfp = null;

-    private string currentVC;

-    private string currentDescriptiveName;

 

     [ContractInvariantMethod]

     void ObjectInvariant()

@@ -402,8 +400,6 @@ namespace Microsoft.Boogie.SMTLib
       PrepareCommon();

 

       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";

-      currentVC = vcString;

-      currentDescriptiveName = descriptiveName;

       FlushAxioms();

 

       PossiblyRestart();

@@ -1265,119 +1261,125 @@ namespace Microsoft.Boogie.SMTLib
             errorsLeft--;

             

             result = GetResponse();

-            if (globalResult == Outcome.Undetermined)

-              globalResult = result;

-            

-            if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {

-            

-              if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)

-              {

-                #region Run timeout diagnostics

 

-                SendThisVC("; begin timeout diagnostics");

-            

-                var verified = new bool[Context.TimoutDiagnosticsCount];

-                var lastCnt = verified.Length + 1;

-                var mod = 2;

-                while (true)

+            if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)

+            {

+              #region Run timeout diagnostics

+

+              SendThisVC("; begin timeout diagnostics");

+

+              var verified = new bool[Context.TimoutDiagnosticsCount];

+              var lastCnt = verified.Length + 1;

+              var mod = 2;

+              var timeLimit = options.TimeLimit;

+              var timeLimitFactor = 1;

+              while (true)

+              {

+                var split0 = verified.ToArray();

+                var split1 = verified.ToArray();

+                int cnt0 = 0;

+                int cnt1 = 0;

+                for (int i = 0; i < split0.Length; i++)

                 {

-                  var split0 = verified.ToArray();

-                  var split1 = verified.ToArray();

-                  int cnt0 = 0;

-                  int cnt1 = 0;

-                  for (int i = 0; i < split0.Length; i++)

+                  if (!split0[i])

                   {

-                    if (!split0[i])

+                    // TODO(wuestholz): Try out different ways for splitting up the work.

+                    if ((cnt0 + cnt1) % mod == 0)

                     {

-                      // TODO(wuestholz): Try out different ways for splitting up the work.

-                      if ((cnt0 + cnt1) % mod == 0)

-                      {

-                        split0[i] = true;

-                        cnt1++;

-                      }

-                      else

-                      {

-                        split1[i] = true;

-                        cnt0++;

-                      }

+                      split0[i] = true;

+                      cnt1++;

+                    }

+                    else

+                    {

+                      split1[i] = true;

+                      cnt0++;

                     }

                   }

-            

-                  bool doReset = false;

-                  var cnt = cnt0 + cnt1;

-                  if (cnt == 0)

+                }

+

+                var cnt = cnt0 + cnt1;

+                if (cnt == 0)

+                {

+                  result = Outcome.Valid;

+                  break;

+                }

+                else if (lastCnt <= cnt)

+                {

+                  if (mod < cnt)

                   {

-                    return Outcome.Valid;

+                    mod++;

                   }

-                  else if (lastCnt <= cnt)

+                  else if (timeLimitFactor <= 3 && 0 < timeLimit)

                   {

-                    doReset = (errorLimit == errorsLeft + 1);

-                    if (mod < cnt)

-                    {

-                      mod++;

-                    }

-                    else

-                    {

-                      // Give up and report which assertions were not verified.

-                      var cmds = new List<Tuple<AssertCmd, TransferCmd>>();

-                      for (int i = 0; i < verified.Length; i++)

-                      {

-                        if (!verified[i])

-                        {

-                          cmds.Add(ctx.TimeoutDiagnosticIDToAssertion[i]);

-                        }

-                      }

-            

-                      if (cmds.Any())

-                      {

-                        handler.OnResourceExceeded("timeout after running diagnostics", cmds);

-                      }

-            

-                      break;

-                    }

+                    // TODO(wuestholz): Add a commandline option to control this.

+                    timeLimitFactor++;

                   }

-                  lastCnt = cnt;

-            

-                  if (0 < cnt0)

+                  else

                   {

-                    var result0 = CheckSplit(split0, cnt0, ref popLater, doReset);

-                    if (result0 == Outcome.Valid)

+                    // Give up and report which assertions were not verified.

+                    var cmds = new List<Tuple<AssertCmd, TransferCmd>>();

+                    for (int i = 0; i < verified.Length; i++)

                     {

-                      for (int i = 0; i < split0.Length; i++)

+                      if (!verified[i])

                       {

-                        verified[i] = verified[i] || !split0[i];

+                        cmds.Add(ctx.TimeoutDiagnosticIDToAssertion[i]);

                       }

                     }

-                    else if (result0 == Outcome.Invalid)

+

+                    if (cmds.Any())

                     {

-                      result = result0;

-                      break;

+                      handler.OnResourceExceeded("timeout after running diagnostics", cmds);

                     }

+

+                    break;

                   }

-            

-                  if (0 < cnt1)

+                }

+                lastCnt = cnt;

+

+                if (0 < cnt0)

+                {

+                  var result0 = CheckSplit(split0, cnt0, ref popLater, timeLimitFactor * timeLimit);

+                  if (result0 == Outcome.Valid)

                   {

-                    var result1 = CheckSplit(split1, cnt1, ref popLater, doReset);

-                    if (result1 == Outcome.Valid)

+                    for (int i = 0; i < split0.Length; i++)

                     {

-                      for (int i = 0; i < split1.Length; i++)

-                      {

-                        verified[i] = verified[i] || !split1[i];

-                      }

+                      verified[i] = verified[i] || !split0[i];

                     }

-                    else if (result1 == Outcome.Invalid)

+                  }

+                  else if (result0 == Outcome.Invalid)

+                  {

+                    result = result0;

+                    break;

+                  }

+                }

+

+                if (0 < cnt1)

+                {

+                  var result1 = CheckSplit(split1, cnt1, ref popLater, timeLimitFactor * timeLimit);

+                  if (result1 == Outcome.Valid)

+                  {

+                    for (int i = 0; i < split1.Length; i++)

                     {

-                      result = result1;

-                      break;

+                      verified[i] = verified[i] || !split1[i];

                     }

                   }

+                  else if (result1 == Outcome.Invalid)

+                  {

+                    result = result1;

+                    break;

+                  }

                 }

-            

-                SendThisVC("; end timeout diagnostics");

-

-                #endregion

               }

+

+              SendThisVC("; end timeout diagnostics");

+

+              #endregion

+            }

+

+            if (globalResult == Outcome.Undetermined)

+              globalResult = result;

             

+            if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {

               IList<string> xlabels;

               if (CommandLineOptions.Clo.UseLabels) {

                 labels = GetLabelsInfo();

@@ -1445,27 +1447,17 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

-    private Outcome CheckSplit(bool[] split, int unverifiedCount, ref bool popLater, bool doReset = false)

+    private Outcome CheckSplit(bool[] split, int unverifiedCount, ref bool popLater, int timeLimit)

     {

-      if (doReset && currentVC != null && currentDescriptiveName != null)

+      if (popLater)

       {

-        Reset(gen);

-        PossiblyRestart();

-        SendThisVC("(push 1)");

-        SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(currentDescriptiveName) + ")");

-        SendThisVC(currentVC);

-        popLater = false;

-      }

-      else

-      {

-        if (popLater)

-        {

-          SendThisVC("(pop 1)");

-        }

-        SendThisVC("(push 1)");

-        SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), options.TimeLimit));

-        popLater = true;

+        SendThisVC("(pop 1)");

       }

+

+      SendThisVC("(push 1)");

+      SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), timeLimit));

+      popLater = true;

+

       SendThisVC(string.Format("; checking split VC with {0} unverified assertions", unverifiedCount));

       var expr = VCExpressionGenerator.True;

       for (int i = 0; i < split.Length; i++)