From bc5b252f0760be84bf96edc2750b85fb0238e772 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 20 May 2015 13:15:01 +0200 Subject: Improve support for diagnosing timeouts. --- Source/Provers/SMTLib/ProverInterface.cs | 208 +++++++++++++++---------------- 1 file changed, 100 insertions(+), 108 deletions(-) (limited to 'Source/Provers') 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>(); - 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>(); + 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 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++) -- cgit v1.2.3