Merge pull request #889 from diffblue/netlist

extract netlist creation

src/ebmc/Makefile

@@ -19,6 +19,7 @@ SRC = \
       liveness_to_safety.cpp \
       live_signal.cpp \
       main.cpp \
+      netlist.cpp \
       neural_liveness.cpp \
       output_file.cpp \
       output_verilog.cpp \

src/ebmc/bdd_engine.cpp

@@ -20,11 +20,12 @@ Author: Daniel Kroening, [email protected]
 #include <temporal-logic/temporal_logic.h>
 #include <trans-netlist/aig_prop.h>
 #include <trans-netlist/instantiate_netlist.h>
-#include <trans-netlist/trans_to_netlist.h>
 #include <trans-netlist/trans_trace_netlist.h>
 #include <trans-netlist/unwind_netlist.h>
 #include <verilog/sva_expr.h>
 
+#include "netlist.h"
+
 #include <algorithm>
 #include <iostream>
 
@@ -193,22 +194,17 @@ property_checker_resultt bdd_enginet::operator()()
     if(cmdline.isset("liveness-to-safety"))
       liveness_to_safety(transition_system, properties);
 
-    const auto property_map = properties.make_property_map();
-
     message.status() << "Building netlist" << messaget::eom;
 
-    convert_trans_to_netlist(
-      transition_system.symbol_table,
-      transition_system.main_symbol->name,
-      transition_system.trans_expr,
-      property_map,
-      netlist,
-      message.get_message_handler());
+    netlist = make_netlist(
+      transition_system, properties, message.get_message_handler());
 
     message.statistics() << "Latches: " << netlist.var_map.latches.size()
                          << ", nodes: " << netlist.number_of_nodes()
                          << messaget::eom;
 
+    const auto property_map = properties.make_property_map();
+
     for(const auto &[_, expr] : property_map)
       get_atomic_propositions(expr);
 

src/ebmc/ebmc_base.cpp

@@ -13,10 +13,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <trans-netlist/compute_ct.h>
 #include <trans-netlist/ldg.h>
-#include <trans-netlist/trans_to_netlist.h>
 
 #include "ebmc_error.h"
 #include "ebmc_version.h"
+#include "netlist.h"
 
 #include <iostream>
 
@@ -149,13 +149,8 @@ bool ebmc_baset::make_netlist(netlistt &netlist)
 
   try
   {
-    convert_trans_to_netlist(
-      transition_system.symbol_table,
-      transition_system.main_symbol->name,
-      transition_system.trans_expr,
-      properties.make_property_map(),
-      netlist,
-      message.get_message_handler());
+    netlist = ::make_netlist(
+      transition_system, properties, message.get_message_handler());
   }
 
   catch(const std::string &error_str)

src/ebmc/netlist.cpp

@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Netlists for EBMC
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "netlist.h"
+
+#include <trans-netlist/netlist.h>
+#include <trans-netlist/trans_to_netlist.h>
+
+netlistt make_netlist(
+  transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
+{
+  netlistt netlist;
+
+  convert_trans_to_netlist(
+    transition_system.symbol_table,
+    transition_system.main_symbol->name,
+    transition_system.trans_expr,
+    properties.make_property_map(),
+    netlist,
+    message_handler);
+
+  return netlist;
+}

src/ebmc/netlist.h

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Netlists for EBMC
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_NETLIST_H
+#define CPROVER_EBMC_NETLIST_H
+
+#include "ebmc_properties.h"
+#include "transition_system.h"
+
+class netlistt;
+
+netlistt
+make_netlist(transition_systemt &, ebmc_propertiest &, message_handlert &);
+
+#endif // CPROVER_EBMC_NETLIST_H

src/ebmc/property_checker.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/string2int.h>
 
 #include <solvers/sat/satcheck.h>
-#include <trans-netlist/trans_to_netlist.h>
 #include <trans-netlist/trans_trace_netlist.h>
 #include <trans-netlist/unwind_netlist.h>
 
@@ -21,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "k_induction.h"
+#include "netlist.h"
 #include "output_file.h"
 #include "report_results.h"
 
@@ -221,16 +221,9 @@ property_checker_resultt bit_level_bmc(
         throw "no properties";
 
     // make net-list
-    netlistt netlist;
     message.status() << "Generating Netlist" << messaget::eom;
 
-    convert_trans_to_netlist(
-      transition_system.symbol_table,
-      transition_system.main_symbol->name,
-      transition_system.trans_expr,
-      properties.make_property_map(),
-      netlist,
-      message.get_message_handler());
+    auto netlist = make_netlist(transition_system, properties, message_handler);
 
     message.statistics() << "Latches: " << netlist.var_map.latches.size()
                          << ", nodes: " << netlist.number_of_nodes()