Remove ebmc_baset

src/ebmc/Makefile

@@ -12,7 +12,6 @@ SRC = \
       diameter.cpp \
       diatest.cpp \
       dimacs_writer.cpp \
-      ebmc_base.cpp \
       ebmc_language.cpp \
       ebmc_language_file.cpp \
       ebmc_languages.cpp \

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/ebmc/random_traces.cpp

@@ -20,9 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
-#include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "output_file.h"
+#include "transition_system.h"
 #include "waveform.h"
 
 #include <algorithm>

src/ebmc/ranking_function.cpp

@@ -21,7 +21,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <trans-word-level/unwind.h>
 #include <verilog/sva_expr.h>
 
-#include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "property_checker.h"

src/ebmc/show_trans.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <verilog/expr2verilog.h>
 
-#include "ebmc_base.h"
 #include "ebmc_version.h"
 #include "output_file.h"
 #include "output_verilog.h"

src/ic3/dnf_io.hh

@@ -10,6 +10,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #ifndef DNF_IO_HH
 #define DNF_IO_HH
 
+#include <cstdlib>
 #include <deque>
 #include <iosfwd>
 #include <map>

src/ic3/m4y_aiger_print.cc

@@ -6,21 +6,19 @@ Module: Printing circuit in text version of aiger format
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
-#include <queue>
-#include <set>
-#include <map>
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
 #include <algorithm>
 #include <iostream>
-
-#include <ebmc/ebmc_base.h>
+#include <map>
+#include <queue>
+#include <set>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
-
 /*====================================
 
  P R I N T _ A I G E R _ F O R M A T