fixup! Stop propt inheriting from messaget

Author: romainbrenguier

src/cbmc/cbmc_solvers.cpp

@@ -67,15 +67,14 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
      !options.get_bool_option("sat-preprocessor")) // no simplifier
   {
     // simplifier won't work with beautification
-    solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
+    solver->set_prop(
+      util_make_unique<satcheck_no_simplifiert>(message_handler));
   }
   else // with simplifier
   {
-    solver->set_prop(util_make_unique<satcheckt>());
+    solver->set_prop(util_make_unique<satcheckt>(message_handler));
   }
 
-  solver->prop().set_message_handler(message_handler);
-
   auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
 
   if(options.get_option("arrays-uf")=="never")
@@ -93,11 +92,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
   no_beautification();
   no_incremental_check();
 
-  auto prop=util_make_unique<dimacs_cnft>();
-  prop->set_message_handler(message_handler);
-
+  auto prop = util_make_unique<dimacs_cnft>(message_handler);
   std::string filename=options.get_option("outfile");
-
   auto bv_dimacs = util_make_unique<bv_dimacst>(ns, *prop, filename);
   return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
 }
@@ -110,13 +106,11 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
     if(options.get_bool_option("sat-preprocessor"))
     {
       no_beautification();
-      return util_make_unique<satcheckt>();
+      return util_make_unique<satcheckt>(message_handler);
     }
-    return util_make_unique<satcheck_no_simplifiert>();
+    return util_make_unique<satcheck_no_simplifiert>(message_handler);
   }();
 
-  prop->set_message_handler(message_handler);
-
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=prop.get();
@@ -142,8 +136,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
 {
   string_refinementt::infot info;
   info.ns=&ns;
-  auto prop=util_make_unique<satcheck_no_simplifiert>();
-  prop->set_message_handler(message_handler);
+  auto prop = util_make_unique<satcheck_no_simplifiert>(message_handler);
   info.prop=prop.get();
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
   info.output_xml = output_xml_in_refinement;

src/solvers/prop/prop.h

@@ -117,11 +117,6 @@ class propt
     message.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
   }
 
-  void set_message_handler(message_handlert &message_handler)
-  {
-    message.set_message_handler(message_handler);
-  }
-
 protected:
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;

src/solvers/sat/dimacs_cnf.cpp

@@ -19,6 +19,11 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
 {
 }
 
+dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
+{
+  message.set_message_handler(message_handler);
+}
+
 void dimacs_cnft::set_assignment(literalt, bool)
 {
   UNIMPLEMENTED;

src/solvers/sat/dimacs_cnf.h

@@ -18,6 +18,7 @@ class dimacs_cnft:public cnf_clause_listt
 {
 public:
   dimacs_cnft();
+  explicit dimacs_cnft(message_handlert &);
   virtual ~dimacs_cnft() { }
 
   virtual void write_dimacs_cnf(std::ostream &out);

src/solvers/sat/satcheck_minisat2.cpp

@@ -343,11 +343,25 @@ satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert():
 {
 }
 
+satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_minisat_no_simplifiert()
+{
+  message.set_message_handler(message_handler);
+}
+
 satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
   satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
 {
 }
 
+satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_minisat_simplifiert()
+{
+  message.set_message_handler(message_handler);
+}
+
 void satcheck_minisat_simplifiert::set_frozen(literalt a)
 {
   try

src/solvers/sat/satcheck_minisat2.h

@@ -70,6 +70,7 @@ class satcheck_minisat_no_simplifiert:
 {
 public:
   satcheck_minisat_no_simplifiert();
+  explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text();
 };
 
@@ -78,6 +79,7 @@ class satcheck_minisat_simplifiert:
 {
 public:
   satcheck_minisat_simplifiert();
+  explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text() final;
   virtual void set_frozen(literalt a) final;
   bool is_eliminated(literalt a) const;

src/solvers/smt2/smt2_solver.cpp

@@ -227,9 +227,8 @@ int solver(std::istream &in)
   // this is our default verbosity
   message_handler.set_verbosity(messaget::M_STATISTICS);
 
-  satcheckt satcheck;
+  satcheckt satcheck(message_handler);
   boolbvt boolbv(ns, satcheck);
-  satcheck.set_message_handler(message_handler);
   boolbv.set_message_handler(message_handler);
 
   smt2_solvert smt2_solver(in, boolbv);