diff options
| author |  shuvendu <unknown> | 2014-07-27 13:25:06 -0700 |
|---|---|---|
| committer | shuvendu <unknown> | 2014-07-27 13:25:06 -0700 |
| commit | 5c5ece158229ad33f36afed8af3b5e47d99987f1 (patch) | |
| tree | bdd9b258e80c0be21f6d032fb7c2588c6e51306d | |
| parent | d4762961dd719a0f0783551aea5a17203cbe42eb (diff) | |
ExplainHoudini change to add reasons for inconsistency as well.
| -rw-r--r-- | Source/Houdini/Checker.cs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 6ffaef22..30056d99 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -385,6 +385,9 @@ namespace Microsoft.Boogie.Houdini { break;
unsatisfiedSoftAssumptions2.Iter(i => reason.Remove(softAssumptions2[i].ToString()));
+ var reason1 = new HashSet<string>(); //these are the reasons for inconsistency
+ unsatisfiedSoftAssumptions2.Iter(i => reason1.Add(softAssumptions2[i].ToString()));
+
if (CommandLineOptions.Clo.Trace)
{
Console.Write("Revised reason for removal of {0}: ", refutedConstant.Name);
@@ -395,6 +398,11 @@ namespace Microsoft.Boogie.Houdini { {
Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, descriptiveName);
}
+ //also add the removed reasons using dotted edges (requires- x != 0, requires- x == 0 ==> assert x != 0)
+ foreach (var r in reason1)
+ {
+ Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=blue style=dotted ];", refutedConstant.Name, r, descriptiveName);
+ }
} while (false);
if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)
|