Merge pull request #3819 from peterschrammel/solver-factory-namespace

Solver factory shouldn't have its own namespacet instance

src/cbmc/bmc.cpp

@@ -276,6 +276,7 @@ int bmct::do_language_agnostic_bmc(
   safety_checkert::resultt final_result = safety_checkert::resultt::SAFE;
   safety_checkert::resultt tmp_result = safety_checkert::resultt::SAFE;
   const symbol_tablet &symbol_table = model.get_symbol_table();
+  namespacet ns(symbol_table);
   messaget message(ui);
   std::unique_ptr<path_storaget> worklist;
   std::string strategy = opts.get_option("exploration-strategy");
@@ -285,12 +286,10 @@ int bmct::do_language_agnostic_bmc(
   worklist = path_strategy_chooser.get(strategy);
   try
   {
+    solver_factoryt solvers(
+      opts, ns, ui, ui.get_ui() == ui_message_handlert::uit::XML_UI);
+
     {
-      solver_factoryt solvers(
-        opts,
-        symbol_table,
-        ui,
-        ui.get_ui() == ui_message_handlert::uit::XML_UI);
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
@@ -333,11 +332,6 @@ int bmct::do_language_agnostic_bmc(
 
     while(!worklist->empty())
     {
-      solver_factoryt solvers(
-        opts,
-        symbol_table,
-        ui,
-        ui.get_ui() == ui_message_handlert::uit::XML_UI);
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();

src/goto-checker/solver_factory.cpp

@@ -18,7 +18,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/options.h>
-#include <util/symbol_table.h>
 #include <util/version.h>
 
 #ifdef _MSC_VER
@@ -35,12 +34,11 @@ Author: Daniel Kroening, Peter Schrammel
 
 solver_factoryt::solver_factoryt(
   const optionst &_options,
-  const symbol_tablet &_symbol_table,
+  const namespacet &_ns,
   message_handlert &_message_handler,
   bool _output_xml_in_refinement)
   : options(_options),
-    symbol_table(_symbol_table),
-    ns(_symbol_table),
+    ns(_ns),
     message_handler(_message_handler),
     output_xml_in_refinement(_output_xml_in_refinement)
 {

src/goto-checker/solver_factory.h

@@ -21,14 +21,14 @@ class namespacet;
 class optionst;
 class propt;
 class prop_convt;
-class symbol_tablet;
 
 class solver_factoryt
 {
 public:
+  /// Note: The solver returned will hold a reference to the namespace `ns`.
   solver_factoryt(
     const optionst &_options,
-    const symbol_tablet &_symbol_table,
+    const namespacet &_ns,
     message_handlert &_message_handler,
     bool _output_xml_in_refinement);
 
@@ -62,8 +62,7 @@ public:
 
 protected:
   const optionst &options;
-  const symbol_tablet &symbol_table;
-  namespacet ns;
+  const namespacet &ns;
   message_handlert &message_handler;
   const bool output_xml_in_refinement;
 

unit/path_strategies.cpp

@@ -377,9 +377,10 @@ void _check_with_strategy(
   ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh);
   REQUIRE(ret == -1);
 
-  solver_factoryt initial_solvers(opts, gm.get_symbol_table(), mh, false);
+  namespacet ns(gm.get_symbol_table());
+  solver_factoryt solver_factory(opts, ns, mh, false);
   std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
-    initial_solvers.get_solver();
+    solver_factory.get_solver();
   prop_convt &initial_pc = cbmc_solver->prop_conv();
   std::function<bool(void)> callback = []() { return false; };
 
@@ -404,8 +405,7 @@ void _check_with_strategy(
 
   while(!worklist->empty())
   {
-    solver_factoryt solvers(opts, gm.get_symbol_table(), mh, false);
-    cbmc_solver = solvers.get_solver();
+    cbmc_solver = solver_factory.get_solver();
     prop_convt &pc = cbmc_solver->prop_conv();
     path_storaget::patht &resume = worklist->peek();