Merge pull request #649 from diffblue/move_bdd

Move BDD engine invocation

src/ebmc/bdd_engine.cpp

@@ -10,8 +10,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/format_expr.h>
 
-#include <ebmc/ebmc_properties.h>
-#include <ebmc/transition_system.h>
 #include <solvers/bdd/miniBDD/miniBDD.h>
 #include <solvers/sat/satcheck.h>
 #include <temporal-logic/negate_property.h>
@@ -42,19 +40,27 @@ class bdd_enginet
 public:
   bdd_enginet(
     const cmdlinet &_cmdline,
-    ui_message_handlert &_ui_message_handler)
-    : cmdline(_cmdline), message(_ui_message_handler)
+    transition_systemt &_transition_system,
+    ebmc_propertiest &_properties,
+    message_handlert &_message_handler)
+    : cmdline(_cmdline),
+      transition_system(_transition_system),
+      properties(_properties),
+      message(_message_handler),
+      ns(transition_system.symbol_table)
   {
   }
 
   int operator()();
 
 protected:
+  using propertiest = ebmc_propertiest;
   using propertyt = ebmc_propertiest::propertyt;
   const cmdlinet &cmdline;
+  transition_systemt &transition_system;
+  propertiest &properties;
   messaget message;
-  transition_systemt transition_system;
-  ebmc_propertiest properties;
+  const namespacet ns;
   netlistt netlist;
 
   // the Manager must appear before any BDDs
@@ -171,12 +177,6 @@ int bdd_enginet::operator()()
 {
   try
   {
-    transition_system =
-      get_transition_system(cmdline, message.get_message_handler());
-
-    properties = ebmc_propertiest::from_command_line(
-      cmdline, transition_system, message.get_message_handler());
-
     const auto property_map = properties.make_property_map();
 
     message.status() << "Building netlist" << messaget::eom;
@@ -229,7 +229,6 @@ int bdd_enginet::operator()()
     for(propertyt &p : properties.properties)
       check_property(p);
 
-    const namespacet ns(transition_system.symbol_table);
     report_results(cmdline, properties, ns, message.get_message_handler());
     return properties.exit_code();
   }
@@ -429,8 +428,6 @@ void bdd_enginet::compute_counterexample(
     throw "unexpected result from SAT solver";
   }
 
-  const namespacet ns(transition_system.symbol_table);
-
   property.witness_trace =
     compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
 }
@@ -901,8 +898,6 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr)
 
     aig_prop_constraintt aig_prop(netlist, message.get_message_handler());
 
-    const namespacet ns(transition_system.symbol_table);
-
     literalt l = instantiate_convert(
       aig_prop, netlist.var_map, expr, ns, message.get_message_handler());
 
@@ -997,7 +992,7 @@ void bdd_enginet::build_BDDs()
 
 /*******************************************************************\
 
-Function: do_bdd
+Function: bdd_engine
 
   Inputs:
 
@@ -1007,10 +1002,12 @@ Function: do_bdd
 
 \*******************************************************************/
 
-int do_bdd(
+int bdd_engine(
   const cmdlinet &cmdline,
-  ui_message_handlert &ui_message_handler)
+  transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
 {
-  return bdd_enginet(cmdline, ui_message_handler)();
+  return bdd_enginet{cmdline, transition_system, properties, message_handler}();
 }
 

src/ebmc/bdd_engine.h

@@ -10,8 +10,14 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_EBMC_BDD_ENGINE_H
 
 #include <util/cmdline.h>
-#include <util/ui_message.h>
+#include <util/message.h>
 
-int do_bdd(const cmdlinet &, ui_message_handlert &);
+#include "ebmc_properties.h"
+
+int bdd_engine(
+  const cmdlinet &,
+  transition_systemt &,
+  ebmc_propertiest &,
+  message_handlert &);
 
 #endif

src/ebmc/ebmc_parse_options.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/help_formatter.h>
 #include <util/string2int.h>
 
-#include "bdd_engine.h"
 #include "diatest.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
@@ -170,9 +169,6 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("ranking-function"))
       return do_ranking_function(cmdline, ui_message_handler);
 
-    if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))
-      return do_bdd(cmdline, ui_message_handler);
-
     if(cmdline.isset("interpolation-word"))
     {
       throw ebmc_errort() << "This option is currently disabled";

src/ebmc/property_checker.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <trans-netlist/trans_trace_netlist.h>
 #include <trans-netlist/unwind_netlist.h>
 
+#include "bdd_engine.h"
 #include "bmc.h"
 #include "dimacs_writer.h"
 #include "ebmc_error.h"
@@ -378,7 +379,11 @@ int property_checker(
   ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
-  if(cmdline.isset("aig") || cmdline.isset("dimacs"))
+  if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))
+  {
+    return bdd_engine(cmdline, transition_system, properties, message_handler);
+  }
+  else if(cmdline.isset("aig") || cmdline.isset("dimacs"))
   {
     return bit_level_bmc(
       cmdline, transition_system, properties, message_handler);