From 7b1b91e940fd8ec7ac60074c843eb08f5715bc91 Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Sat, 10 Jan 2015 11:01:14 +0000
Subject: Removed unnecessary stage-related attributes from candidate
 annotations.

---
 Source/Houdini/AnnotationDependenceAnalyser.cs |  5 +++--
 Source/Houdini/StagedHoudini.cs                | 19 +++++++++++++++++--
 2 files changed, 20 insertions(+), 4 deletions(-)

(limited to 'Source/Houdini')

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
-- 
cgit v1.2.3