summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
diff options
context:
space:
mode:
authorGravatar Michal Moskal <michal@moskal.me>2011-10-27 15:06:00 -0700
committerGravatar Michal Moskal <michal@moskal.me>2011-10-27 15:06:00 -0700
commite001f91572a2ab46771bc2529693c1bc0e0b7628 (patch)
treedbffbae3ad317fd18b771bfa6215132ea17830fe /Source/Provers/SMTLib
parentcfbfbb0229db8f71c4fb21c0f4c7cfb60debd507 (diff)
Restart prover after out-of-memory error; honour -restartProver option
Diffstat (limited to 'Source/Provers/SMTLib')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs43
-rw-r--r--Source/Provers/SMTLib/SMTLibProcess.cs2
2 files changed, 36 insertions, 9 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e70f2bae..cd5cdb31 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -75,14 +75,7 @@ namespace Microsoft.Boogie.SMTLib
ctx.parent = this;
this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);
- if (this.options.UseZ3) {
- var path = this.options.ProverPath;
- if (path == null)
- path = Z3.ExecutablePath();
- var psi = SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");
- Process = new SMTLibProcess(psi, this.options);
- Process.ErrorHandler += this.HandleProverError;
- }
+ SetupProcess();
if (CommandLineOptions.Clo.StratifiedInlining > 0)
{
@@ -98,6 +91,32 @@ namespace Microsoft.Boogie.SMTLib
pendingPop = false;
}
+ void SetupProcess()
+ {
+ if (!this.options.UseZ3)
+ return;
+
+ if (Process != null) return;
+
+ var path = this.options.ProverPath;
+ if (path == null)
+ path = Z3.ExecutablePath();
+ var psi = SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");
+ Process = new SMTLibProcess(psi, this.options);
+ Process.ErrorHandler += this.HandleProverError;
+ }
+
+
+ void PossiblyRestart()
+ {
+ if (Process != null && Process.NeedsRestart) {
+ Process.Close();
+ Process = null;
+ SetupProcess();
+ Process.Send(common.ToString());
+ }
+ }
+
public override ProverContext Context
{
get
@@ -111,7 +130,7 @@ namespace Microsoft.Boogie.SMTLib
internal readonly TypeAxiomBuilder AxBuilder;
internal readonly UniqueNamer Namer;
readonly TypeDeclCollector DeclCollector;
- readonly SMTLibProcess Process;
+ SMTLibProcess Process;
readonly List<string> proverErrors = new List<string>();
readonly List<string> proverWarnings = new List<string>();
readonly StringBuilder common = new StringBuilder();
@@ -275,6 +294,8 @@ namespace Microsoft.Boogie.SMTLib
string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
+ PossiblyRestart();
+
SendThisVC("(push 1)");
SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
SendThisVC(vcString);
@@ -410,6 +431,9 @@ namespace Microsoft.Boogie.SMTLib
FlushLogFile();
+ if (CommandLineOptions.Clo.RestartProverPerVC && Process != null)
+ Process.NeedsRestart = true;
+
return globalResult;
} finally {
@@ -527,6 +551,7 @@ namespace Microsoft.Boogie.SMTLib
case "memout":
currentErrorHandler.OnResourceExceeded("memory");
result = Outcome.OutOfMemory;
+ Process.NeedsRestart = true;
break;
case "timeout":
currentErrorHandler.OnResourceExceeded("timeout");
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 2b2d3f94..1dcfdbff 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -26,6 +26,7 @@ namespace Microsoft.Boogie.SMTLib
readonly int smtProcessId;
static int smtProcessIdSeq = 0;
ConsoleCancelEventHandler cancelEvent;
+ public bool NeedsRestart;
public static ProcessStartInfo ComputerProcessStartInfo(string executable, string options)
{
@@ -110,6 +111,7 @@ namespace Microsoft.Boogie.SMTLib
while (true) {
var sx = GetProverResponse();
if (sx == null) {
+ this.NeedsRestart = true;
HandleError("Prover died");
return;
}