Removed unnecessary stage-related attributes from candidate annotations.

2 files changed, 20 insertions, 4 deletions

diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs
index fd283f3e..7cb43fbd 100644
--- a/Source/Houdini/AnnotationDependenceAnalyser.cs
+++ b/Source/Houdini/AnnotationDependenceAnalyser.cs
@@ -436,8 +436,9 @@ namespace Microsoft.Boogie.Houdini {
 

         if (NoStages())

         {

-          // TODO: need to figure out what to do here

-          throw new NotImplementedException();

+          var TrivialGraph = new Graph<ScheduledStage>();

+          TrivialGraph.AddSource(new ScheduledStage(0, new HashSet<string>()));

+          return new StagedHoudiniPlan(TrivialGraph);

         }

 

         #region Assign annotations to stages at a given level of granularity

diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs
index 49482b3d..f5ddc92a 100644
--- a/Source/Houdini/StagedHoudini.cs
+++ b/Source/Houdini/StagedHoudini.cs
@@ -15,6 +15,7 @@ namespace Microsoft.Boogie.Houdini
   {

 

     private Program program;

+    private HoudiniSession.HoudiniStatistics houdiniStats;

     private Func<string, Program> ProgramFromFile;

     private StagedHoudiniPlan plan;

     private List<Houdini>[] houdiniInstances;

@@ -23,8 +24,9 @@ namespace Microsoft.Boogie.Houdini
 

     private const string tempFilename = "__stagedHoudiniTemp.bpl";

 

-    public StagedHoudini(Program program, Func<string, Program> ProgramFromFile) {

+    public StagedHoudini(Program program, HoudiniSession.HoudiniStatistics houdiniStats, Func<string, Program> ProgramFromFile) {

       this.program = program;

+      this.houdiniStats = houdiniStats;

       this.ProgramFromFile = ProgramFromFile;

       this.houdiniInstances = new List<Houdini>[CommandLineOptions.Clo.StagedHoudiniThreads];

       for (int i = 0; i < CommandLineOptions.Clo.StagedHoudiniThreads; i++) {

@@ -40,16 +42,29 @@ namespace Microsoft.Boogie.Houdini
 

         if(CommandLineOptions.Clo.DebugStagedHoudini) {

           Console.WriteLine("Plan\n====\n");

-          Console.WriteLine(this.plan);

+          if(plan == null) {

+            Console.WriteLine("No plan, as there were no stages");

+          } else {

+            Console.WriteLine(this.plan);

+          }

         }

         

         EmitProgram("staged.bpl");

       }

     }

 

+    private bool NoStages() {

+      return plan == null;

+    }

+

     public HoudiniOutcome PerformStagedHoudiniInference()

     {

 

+      if (NoStages()) {

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

+        return houdini.PerformHoudiniInference();

+      }

+

       EmitProgram(tempFilename);

 

       #region Prepare the tasks, but do not launch them