Bug fix for ExplainHoudini. Made it robust under timeouts.

3 files changed, 53 insertions, 36 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 09d12420..940b355f 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -65,7 +65,7 @@ namespace Microsoft.Boogie.Houdini {
         if (houdini.MatchCandidate(assertCmd.Expr, out houdiniConstant))

             houdiniAssertConstants.Add(houdiniConstant);

         

-        if (houdiniConstant != null && CommandLineOptions.Clo.ExplainHoudini)

+        if (houdiniConstant != null && CommandLineOptions.Clo.ExplainHoudini && !constToControl.ContainsKey(houdiniConstant.Name))

         {

             // For each houdini constant c, create two more constants c_pos and c_neg.

             // Then change the asserted condition (c ==> \phi) to

@@ -334,49 +334,65 @@ namespace Microsoft.Boogie.Houdini {
         var el = CommandLineOptions.Clo.ProverCCLimit;

         CommandLineOptions.Clo.ProverCCLimit = 1;

 

-        List<int> unsatisfiedSoftAssumptions;

-        

-        hardAssumptions.Add(controlExprNoop);

-        proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, handler);

-        hardAssumptions.RemoveAt(hardAssumptions.Count - 1);

+        var outcome = ProverInterface.Outcome.Undetermined;

 

-        var reason = new HashSet<string>();

-        unsatisfiedSoftAssumptions.Iter(i => reason.Add(softAssumptions[i].ToString()));

-        if (CommandLineOptions.Clo.Trace)

+        do

         {

-            Console.Write("Reason for removal of {0}: ", refutedConstant.Name);

-            reason.Iter(r => Console.Write("{0} ", r));

-            Console.WriteLine();

-        }

+            List<int> unsatisfiedSoftAssumptions;

 

-        // Get rid of those constants from the "reason" that can even make

-        // "assert false" pass

+            hardAssumptions.Add(controlExprNoop);

+            outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, handler);

+            hardAssumptions.RemoveAt(hardAssumptions.Count - 1);

 

-        hardAssumptions.Add(controlExprFalse);

-        var softAssumptions2 = new List<VCExpr>();

-        for (int i = 0; i < softAssumptions.Count; i++)

-        {

-            if (unsatisfiedSoftAssumptions.Contains(i))

+            if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)

+                break;

+

+            var reason = new HashSet<string>();

+            unsatisfiedSoftAssumptions.Iter(i => reason.Add(softAssumptions[i].ToString()));

+            if (CommandLineOptions.Clo.Trace)

             {

-                softAssumptions2.Add(softAssumptions[i]);

-                continue;

+                Console.Write("Reason for removal of {0}: ", refutedConstant.Name);

+                reason.Iter(r => Console.Write("{0} ", r));

+                Console.WriteLine();

             }

-            hardAssumptions.Add(softAssumptions[i]);

-        }

 

-        var unsatisfiedSoftAssumptions2 = new List<int>();

-        proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, out unsatisfiedSoftAssumptions2, handler);

+            // Get rid of those constants from the "reason" that can even make

+            // "assert false" pass

 

-        unsatisfiedSoftAssumptions2.Iter(i => reason.Remove(softAssumptions2[i].ToString()));

-        if (CommandLineOptions.Clo.Trace)

-        {

-            Console.Write("Revised reason for removal of {0}: ", refutedConstant.Name);

-            reason.Iter(r => Console.Write("{0} ", r));

-            Console.WriteLine();

-        }

-        foreach (var r in reason)

+            hardAssumptions.Add(controlExprFalse);

+            var softAssumptions2 = new List<VCExpr>();

+            for (int i = 0; i < softAssumptions.Count; i++)

+            {

+                if (unsatisfiedSoftAssumptions.Contains(i))

+                {

+                    softAssumptions2.Add(softAssumptions[i]);

+                    continue;

+                }

+                hardAssumptions.Add(softAssumptions[i]);

+            }

+

+            var unsatisfiedSoftAssumptions2 = new List<int>();

+            outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, out unsatisfiedSoftAssumptions2, handler);

+

+            if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)

+                break;

+

+            unsatisfiedSoftAssumptions2.Iter(i => reason.Remove(softAssumptions2[i].ToString()));

+            if (CommandLineOptions.Clo.Trace)

+            {

+                Console.Write("Revised reason for removal of {0}: ", refutedConstant.Name);

+                reason.Iter(r => Console.Write("{0} ", r));

+                Console.WriteLine();

+            }

+            foreach (var r in reason)

+            {

+                Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, implementation.Name);

+            }

+        } while (false);

+

+        if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)

         {

-            Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"\" color=red ];", refutedConstant.Name, r);

+            Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", implementation.Name);

         }

 

         CommandLineOptions.Clo.ProverCCLimit = el;

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index e93d41ca..17b537eb 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -369,6 +369,7 @@ namespace Microsoft.Boogie.Houdini {
           explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");

           foreach (var constant in houdiniConstants)

               explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);

+          explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");

       }

     }

 

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 4d002956..b1cef239 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -45,7 +45,7 @@ namespace Microsoft.Boogie.SMTLib
     public bool OptimizeForBv = false;

 

     public bool ProduceModel() {

-      return !CommandLineOptions.Clo.UseLabels ||

+      return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini ||

              ExpectingModel();

     }