move LDG output into a method of ldgt

Author: kroening

src/ebmc/ebmc_base.cpp

@@ -88,30 +88,7 @@ void ebmc_baset::show_ldg(std::ostream &out)
 
   out << "Latch dependencies:" << '\n';
 
-  for(auto var_it : netlist.var_map.sorted())
-  {
-    auto &var = var_it->second;
-
-    for(std::size_t i=0; i<var.bits.size(); i++)
-    {
-      if(var.is_latch())
-      {
-        literalt::var_not v=var.bits[i].current.var_no();
-
-        out << "  " << var_it->first << "[" << i << "] = " << v << ":";
-
-        const ldg_nodet &node=ldg[v];
-
-        for(ldg_nodet::edgest::const_iterator
-            i_it=node.in.begin();
-            i_it!=node.in.end();
-            i_it++)
-          out << " " << i_it->first;
-
-        out << '\n';
-      }
-    }
-  }
+  ldg.output(netlist, out);
 }
 
 /*******************************************************************\

src/trans-netlist/ldg.cpp

@@ -98,3 +98,30 @@ void ldgt::compute(
     }
   }
 }
+
+void ldgt::output(const netlistt &netlist, std::ostream &out) const
+{
+  for(auto var_it : netlist.var_map.sorted())
+  {
+    auto &var = var_it->second;
+
+    for(std::size_t i = 0; i < var.bits.size(); i++)
+    {
+      if(var.is_latch())
+      {
+        literalt::var_not v = var.bits[i].current.var_no();
+
+        out << "  " << var_it->first << "[" << i << "] = " << v << ":";
+
+        const ldg_nodet &node = (*this)[v];
+
+        for(ldg_nodet::edgest::const_iterator i_it = node.in.begin();
+            i_it != node.in.end();
+            i_it++)
+          out << " " << i_it->first;
+
+        out << '\n';
+      }
+    }
+  }
+}

src/trans-netlist/ldg.h

@@ -9,12 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_TRANS_LDG_H
 #define CPROVER_TRANS_LDG_H
 
-#include <set>
-
 #include <util/graph.h>
 
 #include "netlist.h"
 
+#include <iosfwd>
+#include <set>
+
 struct ldg_nodet:public graph_nodet<>
 {
 public:
@@ -35,6 +36,8 @@ class ldgt:public grapht<ldg_nodet>
   // latches that are to be considered
   void compute(const netlistt &netlist,
                const latchest &localization);
+
+  void output(const netlistt &, std::ostream &) const;
 };
 
 #endif