diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2012-11-25 22:53:26 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2012-11-25 22:53:26 -0800 |
| commit | 1d36dd2010c2d569bbe2a94ebe0cf664366033cd (patch) | |
| tree | 9c78f1fb035a5629d1291ec60997c82db5abf394 /Source/Houdini/Houdini.cs | |
| parent | 677a1fb63ac20aabda002d5ab390f8bca86b2276 (diff) | |
when a query times out, all asserted candidates are dropped
Diffstat (limited to 'Source/Houdini/Houdini.cs')
| -rw-r--r-- | Source/Houdini/Houdini.cs | 77 |
1 files changed, 48 insertions, 29 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 5271a6a3..a7484ca2 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -593,40 +593,59 @@ namespace Microsoft.Boogie.Houdini { Contract.Assume(currentHoudiniState.Implementation != null);
bool dequeue = true;
- switch (outcome) {
- case ProverInterface.Outcome.Valid:
- //yeah, dequeue
- break;
- case ProverInterface.Outcome.Invalid:
- Contract.Assume(errors != null);
- foreach (Counterexample error in errors) {
- RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
- if (refutedAnnotation != null) { // some candidate annotation removed
- AddRelatedToWorkList(refutedAnnotation);
- UpdateAssignment(refutedAnnotation);
- dequeue = false;
- #region Extra debugging output
+ switch (outcome)
+ {
+ case ProverInterface.Outcome.Valid:
+ //yeah, dequeue
+ break;
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assume(errors != null);
+ foreach (Counterexample error in errors)
+ {
+ RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+ if (refutedAnnotation != null)
+ { // some candidate annotation removed
+ AddRelatedToWorkList(refutedAnnotation);
+ UpdateAssignment(refutedAnnotation);
+ dequeue = false;
+ #region Extra debugging output
+ if (CommandLineOptions.Clo.Trace)
+ {
+ using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))
+ {
+ cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
+ cexWriter.Write(error.ToString());
+ cexWriter.WriteLine();
+ using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
+ foreach (Microsoft.Boogie.Block blk in error.Trace)
+ blk.Emit(writer, 15);
+ //cexWriter.WriteLine();
+ }
+ }
+ #endregion
+
+ }
+ }
+ break;
+ default:
if (CommandLineOptions.Clo.Trace)
{
- using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))
+ Console.WriteLine("Timeout/Spaceout while verifying " + currentHoudiniState.Implementation.Name);
+ }
+ HoudiniSession houdiniSession;
+ houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out houdiniSession);
+ foreach (Variable v in houdiniSession.houdiniAssertConstants)
+ {
+ if (CommandLineOptions.Clo.Trace)
{
- cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
- cexWriter.Write(error.ToString());
- cexWriter.WriteLine();
- using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
- foreach (Microsoft.Boogie.Block blk in error.Trace)
- blk.Emit(writer, 15);
- //cexWriter.WriteLine();
+ Console.WriteLine("Removing " + v);
}
+ currentHoudiniState.Assignment.Remove(v);
+ currentHoudiniState.Assignment.Add(v, false);
+ this.NotifyConstant(v.Name);
}
- #endregion
-
- }
- }
- break;
- default:
- currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
- break;
+ currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
+ break;
}
return dequeue;
|