when a query times out, all asserted candidates are dropped

2 files changed, 72 insertions, 38 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 7832da89..0d5a5d9a 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -16,17 +16,20 @@ using VC;
 

 namespace Microsoft.Boogie.Houdini {

   public class ExistentialConstantCollector : StandardVisitor {

-    public static HashSet<Variable> CollectHoudiniConstants(Houdini houdini, Implementation impl) {

+    public static void CollectHoudiniConstants(Houdini houdini, Implementation impl, out HashSet<Variable> houdiniAssertConstants, out HashSet<Variable> houdiniAssumeConstants) {

       ExistentialConstantCollector collector = new ExistentialConstantCollector(houdini);

       collector.VisitImplementation(impl);

-      return collector.houdiniConstants;

+      houdiniAssertConstants = collector.houdiniAssertConstants;

+      houdiniAssumeConstants = collector.houdiniAssumeConstants;

     }

     private ExistentialConstantCollector(Houdini houdini) {

       this.houdini = houdini;

-      this.houdiniConstants = new HashSet<Variable>();

+      this.houdiniAssertConstants = new HashSet<Variable>();

+      this.houdiniAssumeConstants = new HashSet<Variable>();

     }

     private Houdini houdini;

-    private HashSet<Variable> houdiniConstants;

+    private HashSet<Variable> houdiniAssertConstants;

+    private HashSet<Variable> houdiniAssumeConstants;

     public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {

       AddHoudiniConstant(node);

       return base.VisitAssertRequiresCmd(node);

@@ -43,10 +46,17 @@ namespace Microsoft.Boogie.Houdini {
       AddHoudiniConstant(node);

       return base.VisitAssumeCmd(node);

     }

-    private void AddHoudiniConstant(PredicateCmd node) {

-      Variable houdiniConstant;

-      if (houdini.MatchCandidate(node.Expr, out houdiniConstant))

-        houdiniConstants.Add(houdiniConstant);

+    private void AddHoudiniConstant(AssertCmd assertCmd)

+    {

+        Variable houdiniConstant;

+        if (houdini.MatchCandidate(assertCmd.Expr, out houdiniConstant))

+            houdiniAssertConstants.Add(houdiniConstant);

+    }

+    private void AddHoudiniConstant(AssumeCmd assumeCmd)

+    {

+        Variable houdiniConstant;

+        if (houdini.MatchCandidate(assumeCmd.Expr, out houdiniConstant))

+            houdiniAssumeConstants.Add(houdiniConstant);

     }

   }

 

@@ -63,6 +73,7 @@ namespace Microsoft.Boogie.Houdini {
     ConditionGeneration.CounterexampleCollector collector;

     HashSet<Variable> unsatCoreSet;

     HashSet<Variable> houdiniConstants;

+    public HashSet<Variable> houdiniAssertConstants;

     Houdini houdini;

     Implementation implementation;

 

@@ -84,7 +95,11 @@ namespace Microsoft.Boogie.Houdini {
       ModelViewInfo mvInfo;

       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);

 

-      houdiniConstants = ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl);

+      HashSet<Variable> houdiniAssumeConstants;

+      ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out houdiniAssertConstants, out houdiniAssumeConstants);

+      houdiniConstants = new HashSet<Variable>();

+      houdiniConstants.UnionWith(houdiniAssertConstants);

+      houdiniConstants.UnionWith(houdiniAssumeConstants);

 

       var exprGen = proverInterface.Context.ExprGen;

       VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

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;