A decision_proceduret does not need a namespace

This is a generic interface towards decisions procedures, there is no reason all
decision procedures should need a namespace.

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -21,9 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
-arrayst::arrayst(
-  const namespacet &_ns,
-  propt &_prop):equalityt(_ns, _prop)
+arrayst::arrayst(const namespacet &_ns, propt &_prop)
+  : equalityt(_prop), ns(_ns)
 {
   lazy_arrays = false;        // will be set to true when --refine is used
   incremental_cache = false;  // for incremental solving

src/solvers/flattening/arrays.h

@@ -43,6 +43,8 @@ class arrayst:public equalityt
   void record_array_index(const index_exprt &expr);
 
 protected:
+  const namespacet &ns;
+
   virtual void post_process_arrays()
   {
     add_array_constraints();

src/solvers/flattening/equality.h

@@ -19,9 +19,9 @@ Author: Daniel Kroening, [email protected]
 class equalityt:public prop_conv_solvert
 {
 public:
-  equalityt(
-    const namespacet &_ns,
-    propt &_prop):prop_conv_solvert(_ns, _prop) { }
+  explicit equalityt(propt &_prop) : prop_conv_solvert(_prop)
+  {
+  }
 
   virtual literalt equality(const exprt &e1, const exprt &e2);
 

src/solvers/prop/prop_conv.h

@@ -27,9 +27,6 @@ Author: Daniel Kroening, [email protected]
 class prop_convt:public decision_proceduret
 {
 public:
-  explicit prop_convt(
-    const namespacet &_ns):
-    decision_proceduret(_ns) { }
   virtual ~prop_convt() { }
 
   // conversion to handle
@@ -70,9 +67,9 @@ class prop_convt:public decision_proceduret
 class prop_conv_solvert:public prop_convt
 {
 public:
-  prop_conv_solvert(const namespacet &_ns, propt &_prop):
-    prop_convt(_ns),
-    prop(_prop) { }
+  explicit prop_conv_solvert(propt &_prop) : prop(_prop)
+  {
+  }
 
   virtual ~prop_conv_solvert() = default;
 

src/solvers/smt2/smt2_conv.h

@@ -50,21 +50,21 @@ class smt2_convt:public prop_convt
     const std::string &_notes,
     const std::string &_logic,
     solvert _solver,
-    std::ostream &_out):
-    prop_convt(_ns),
-    use_FPA_theory(false),
-    use_datatypes(false),
-    use_array_of_bool(false),
-    emit_set_logic(true),
-    out(_out),
-    benchmark(_benchmark),
-    notes(_notes),
-    logic(_logic),
-    solver(_solver),
-    boolbv_width(_ns),
-    let_id_count(0),
-    pointer_logic(_ns),
-    no_boolean_variables(0)
+    std::ostream &_out)
+    : use_FPA_theory(false),
+      use_datatypes(false),
+      use_array_of_bool(false),
+      emit_set_logic(true),
+      ns(_ns),
+      out(_out),
+      benchmark(_benchmark),
+      notes(_notes),
+      logic(_logic),
+      solver(_solver),
+      boolbv_width(_ns),
+      let_id_count(0),
+      pointer_logic(_ns),
+      no_boolean_variables(0)
   {
     // We set some defaults differently
     // for some solvers.
@@ -128,6 +128,7 @@ class smt2_convt:public prop_convt
   void convert_literal(const literalt);
 
 protected:
+  const namespacet &ns;
   std::ostream &out;
   std::string benchmark, notes, logic;
   solvert solver;

src/util/decision_procedure.h

@@ -15,15 +15,10 @@ Author: Daniel Kroening, [email protected]
 #include "message.h"
 
 class exprt;
-class namespacet;
 
 class decision_proceduret:public messaget
 {
 public:
-  explicit decision_proceduret(const namespacet &_ns):ns(_ns)
-  {
-  }
-
   virtual ~decision_proceduret();
 
   // get a value from satisfying instance if satisfiable
@@ -56,9 +51,6 @@ class decision_proceduret:public messaget
 
   // return a textual description of the decision procedure
   virtual std::string decision_procedure_text() const=0;
-
-protected:
-  const namespacet &ns;
 };
 
 inline decision_proceduret &operator<<(

unit/solvers/bdd/miniBDD/miniBDD.cpp

@@ -186,11 +186,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]")
 {
   GIVEN("A bdd for x&!x")
   {
-    symbol_tablet symbol_table;
-    namespacet ns(symbol_table);
     mini_bdd_mgrt bdd_mgr;
     bdd_propt bdd_prop(bdd_mgr);
-    prop_conv_solvert solver(ns, bdd_prop);
+    prop_conv_solvert solver(bdd_prop);
 
     symbol_exprt var("x", bool_typet());
     literalt result = solver.convert(and_exprt(var, not_exprt(var)));