Merge pull request #1463 from diffblue/ldg

move `--show-ldg` and `--compute-ct` out of `ebmc_baset`

Author: tautschnig

src/ebmc/ebmc_base.cpp

@@ -61,65 +61,6 @@ int ebmc_baset::get_properties()
 
 /*******************************************************************\
 
-Function: ebmc_baset::show_ldg
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void ebmc_baset::show_ldg(std::ostream &out)
-{
-  netlistt netlist;
-
-  if(make_netlist(netlist))
-    return;
-  
-  if(!netlist.transition.empty())
-    out << "WARNING: transition constraint found!" << '\n'
-        << '\n';
-  
-  ldgt ldg;
- 
-  ldg.compute(netlist);
-    
-  out << "Latch dependencies:" << '\n';
-
-  for(var_mapt::mapt::const_iterator
-      it=netlist.var_map.map.begin();
-      it!=netlist.var_map.map.end();
-      it++)
-  {
-    const var_mapt::vart &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 << "  " << 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';
-      }
-    }
-  }
-}
-
-/*******************************************************************\
-
 Function: ebmc_baset::make_netlist
 
   Inputs:
@@ -153,36 +94,3 @@ bool ebmc_baset::make_netlist(netlistt &netlist)
 
   return false;
 }
-
-/*******************************************************************\
-
-Function: ebmc_baset::do_compute_ct
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int ebmc_baset::do_compute_ct()
-{
-  // make net-list
-  message.status() << "Making Netlist" << messaget::eom;
-
-  netlistt netlist;
-  if(make_netlist(netlist)) return 1;
-
-  message.status() << "Latches: " << netlist.var_map.latches.size()
-                   << ", nodes: " << netlist.number_of_nodes() << messaget::eom;
-
-  message.status() << "Making LDG" << messaget::eom;
-
-  ldgt ldg;
-  ldg.compute(netlist);
-
-  std::cout << "CT = " << compute_ct(ldg) << '\n';
-  
-  return 0;
-}

src/ebmc/ebmc_base.h

@@ -33,7 +33,6 @@ class ebmc_baset
   virtual ~ebmc_baset() { }
 
   int get_properties();
-  void show_ldg(std::ostream &out);
   bool make_netlist(netlistt &);
 
   transition_systemt transition_system;
@@ -53,9 +52,6 @@ class ebmc_baset
   bool typecheck();
 
   std::size_t bound;
-
-public:
-  int do_compute_ct();
 };
 
 #endif

src/ebmc/ebmc_parse_options.cpp

@@ -13,11 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/help_formatter.h>
 #include <util/string2int.h>
 
+#include <trans-netlist/compute_ct.h>
+#include <trans-netlist/ldg.h>
 #include <trans-netlist/smv_netlist.h>
 
 #include "build_transition_system.h"
 #include "diatest.h"
-#include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_language.h"
 #include "ebmc_version.h"
@@ -270,10 +271,19 @@ int ebmc_parse_optionst::doit()
 
     if(cmdline.isset("show-ldg"))
     {
-      ebmc_baset ebmc_base(cmdline, ui_message_handler);
-      ebmc_base.transition_system = std::move(transition_system);
-      ebmc_base.properties = std::move(properties);
-      ebmc_base.show_ldg(std::cout);
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+
+      if(!netlist.transition.empty())
+      {
+        messaget message(ui_message_handler);
+        message.warning() << "transition constraint found!" << messaget::eom;
+      }
+
+      ldgt ldg;
+      ldg.compute(netlist);
+      std::cout << "Latch dependencies:" << '\n';
+      ldg.output(netlist, std::cout);
       return 0;
     }
 
@@ -321,10 +331,21 @@ int ebmc_parse_optionst::doit()
 
     if(cmdline.isset("compute-ct"))
     {
-      ebmc_baset ebmc_base(cmdline, ui_message_handler);
-      ebmc_base.transition_system = std::move(transition_system);
-      ebmc_base.properties = std::move(properties);
-      return ebmc_base.do_compute_ct();
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+
+      messaget message{ui_message_handler};
+
+      message.status() << "Latches: " << netlist.var_map.latches.size()
+                       << ", nodes: " << netlist.number_of_nodes()
+                       << messaget::eom;
+
+      message.status() << "Making LDG" << messaget::eom;
+
+      ldgt ldg;
+      ldg.compute(netlist);
+      std::cout << "CT = " << compute_ct(ldg) << '\n';
+      return 0;
     }
 
     auto checker_result = property_checker(

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