Extracted Houdini statistics into a record, and parametersied Houdini class with a statistics object. This means that if one runs multiple Houdini instances, each can record its own statistics.

3 files changed, 30 insertions, 23 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index b83a7d52..79043832 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1109,8 +1109,8 @@ namespace Microsoft.Boogie
       {

         return RunAbstractHoudini(program, stats, er);

       }

-

-      Houdini.Houdini houdini = new Houdini.Houdini(program);

+      Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();

+      Houdini.Houdini houdini = new Houdini.Houdini(program, houdiniStats);

       Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();

 

       if (CommandLineOptions.Clo.PrintAssignment)

@@ -1132,11 +1132,11 @@ namespace Microsoft.Boogie
         }

         Console.WriteLine("Number of true assignments = " + numTrueAssigns);

         Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));

-        Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2"));

-        Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2"));

-        Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);

-        Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);

-        Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);

+        Console.WriteLine("Prover time = " + houdiniStats.proverTime.ToString("F2"));

+        Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2"));

+        Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries);

+        Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries);

+        Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings);

       }

 

       foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index d0796c4c..52fb3796 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -94,14 +94,20 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

+

+

   public class HoudiniSession {

-    public static double proverTime = 0;

-    public static int numProverQueries = 0;

-    public static double unsatCoreProverTime = 0;

-    public static int numUnsatCoreProverQueries = 0;

-    public static int numUnsatCorePrunings = 0;

+

+    public class HoudiniStatistics {

+      public double proverTime = 0;

+      public int numProverQueries = 0;

+      public double unsatCoreProverTime = 0;

+      public int numUnsatCoreProverQueries = 0;

+      public int numUnsatCorePrunings = 0;

+    }

 

     public string descriptiveName;

+    public HoudiniStatistics stats;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

     ConditionGeneration.CounterexampleCollector collector;

@@ -120,12 +126,13 @@ namespace Microsoft.Boogie.Houdini {
         return true;

       if (unsatCoreSet.Contains(constant))

         return true;

-      numUnsatCorePrunings++;

+      stats.numUnsatCorePrunings++;

       return false;

     }

 

-    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl) {

-      descriptiveName = impl.Name;

+    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats) {

+      this.descriptiveName = impl.Name;

+      this.stats = stats;

       collector = new ConditionGeneration.CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

 

@@ -224,8 +231,8 @@ namespace Microsoft.Boogie.Houdini {
       ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);

 

       double queryTime = (DateTime.UtcNow - now).TotalSeconds;

-      proverTime += queryTime;

-      numProverQueries++;

+      stats.proverTime += queryTime;

+      stats.numProverQueries++;

       if (CommandLineOptions.Clo.Trace) {

         Console.WriteLine("Time taken = " + queryTime);

       }

@@ -394,8 +401,8 @@ namespace Microsoft.Boogie.Houdini {
         CommandLineOptions.Clo.ProverCCLimit = el;

 

         double queryTime = (DateTime.UtcNow - now).TotalSeconds;

-        proverTime += queryTime;

-        numProverQueries++;

+        stats.proverTime += queryTime;

+        stats.numProverQueries++;

         if (CommandLineOptions.Clo.Trace)

         {

             Console.WriteLine("Time taken = " + queryTime);

@@ -429,8 +436,8 @@ namespace Microsoft.Boogie.Houdini {
       proverInterface.Pop();

 

       double unsatCoreQueryTime = (DateTime.UtcNow - now).TotalSeconds;

-      unsatCoreProverTime += unsatCoreQueryTime;

-      numUnsatCoreProverQueries++;

+      stats.unsatCoreProverTime += unsatCoreQueryTime;

+      stats.numUnsatCoreProverQueries++;

     }

 

   }

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index abc5a7e8..ee1bdb90 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -327,7 +327,7 @@ namespace Microsoft.Boogie.Houdini {
 

     public static TextWriter explainHoudiniDottyFile;

 

-    public Houdini(Program program) {

+    public Houdini(Program program, HoudiniSession.HoudiniStatistics stats) {

       this.program = program;

 

       if (CommandLineOptions.Clo.Trace)

@@ -360,7 +360,7 @@ namespace Microsoft.Boogie.Houdini {
         try {

           if (CommandLineOptions.Clo.Trace)

             Console.WriteLine("Generating VC for {0}", impl.Name);

-          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl);

+          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats);

           houdiniSessions.Add(impl, session);

         }

         catch (VCGenException) {