Require a message handler when constructing a propt [blocks: #3800]

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -6,6 +6,7 @@ Author: Jesse Sigal, [email protected]
 
 \*******************************************************************/
 
+#include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
 #include <java_bytecode/java_bytecode_language.h>
@@ -154,7 +155,7 @@ std::string create_info(std::vector<exprt> &lemmas, const namespacet &ns)
 /// \return SAT solver result
 decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
 {
-  satcheck_no_simplifiert sat_check;
+  satcheck_no_simplifiert sat_check(null_message_handler);
   bv_refinementt::infot info;
   info.ns = &ns;
   info.prop = &sat_check;

src/goto-instrument/accelerate/scratch_program.h

@@ -45,7 +45,7 @@ class scratch_programt:public goto_programt
       path_storage(),
       options(get_default_options()),
       symex(mh, symbol_table, equation, options, path_storage),
-      satcheck(util_make_unique<satcheckt>()),
+      satcheck(util_make_unique<satcheckt>(mh)),
       satchecker(ns, *satcheck),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
       checker(&z3) // checker(&satchecker)

src/solvers/flattening/bv_minimize.h

@@ -48,8 +48,8 @@ class bv_minimizing_dect:public bv_pointerst
     return "Bit vector minimizing SAT";
   }
 
-  explicit bv_minimizing_dect(const namespacet &_ns):
-    bv_pointerst(_ns, satcheck)
+  bv_minimizing_dect(const namespacet &_ns, message_handlert &message_handler)
+    : bv_pointerst(_ns, satcheck), satcheck(message_handler)
   {
   }
 

src/solvers/prop/prop.h

@@ -24,7 +24,9 @@ Author: Daniel Kroening, [email protected]
 class propt
 {
 public:
-  propt() { }
+  explicit propt(message_handlert &message_handler) : log(message_handler)
+  {
+  }
 
   virtual ~propt() { }
 

src/solvers/qbf/qbf_quantor.cpp

@@ -13,7 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 
-qbf_quantort::qbf_quantort()
+qbf_quantort::qbf_quantort(message_handlert &message_handler)
+  : qdimacs_cnft(message_handler)
 {
 }
 

src/solvers/qbf/qbf_quantor.h

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 class qbf_quantort:public qdimacs_cnft
 {
 public:
-  qbf_quantort();
+  explicit qbf_quantort(message_handlert &message_handler);
   virtual ~qbf_quantort();
 
   virtual const std::string solver_text();

src/solvers/qbf/qbf_qube.cpp

@@ -13,7 +13,8 @@ Author: CM Wintersteiger
 
 #include <util/invariant.h>
 
-qbf_qubet::qbf_qubet()
+qbf_qubet::qbf_qubet(message_handlert &message_handler)
+  : qdimacs_cnft(message_handler)
 {
   // skizzo crashes on broken lines
   break_lines=false;

src/solvers/qbf/qbf_qube.h

@@ -15,7 +15,7 @@ Author: CM Wintersteiger
 class qbf_qubet:public qdimacs_cnft
 {
 public:
-  qbf_qubet();
+  explicit qbf_qubet(message_handlert &message_handler);
   virtual ~qbf_qubet();
 
   virtual const std::string solver_text();

src/solvers/qbf/qbf_qube_core.cpp

@@ -15,7 +15,8 @@ Author: CM Wintersteiger
 #include <util/arith_tools.h>
 #include <util/invariant.h>
 
-qbf_qube_coret::qbf_qube_coret() : qdimacs_coret()
+qbf_qube_coret::qbf_qube_coret(message_handlert &message_handler)
+  : qdimacs_coret(message_handler)
 {
   break_lines=false;
   qbf_tmp_file="qube.qdimacs";

src/solvers/qbf/qbf_qube_core.h

@@ -23,7 +23,7 @@ class qbf_qube_coret:public qdimacs_coret
   assignmentt assignment;
 
 public:
-  qbf_qube_coret();
+  explicit qbf_qube_coret(message_handlert &message_handler);
   virtual ~qbf_qube_coret();
 
   virtual const std::string solver_text();

src/solvers/qbf/qbf_skizzo.cpp

@@ -13,7 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 
-qbf_skizzot::qbf_skizzot()
+qbf_skizzot::qbf_skizzot(message_handlert &message_handler)
+  : qdimacs_cnft(message_handler)
 {
   // skizzo crashes on broken lines
   break_lines=false;

src/solvers/qbf/qbf_skizzo.h

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 class qbf_skizzot:public qdimacs_cnft
 {
 public:
-  qbf_skizzot();
+  explicit qbf_skizzot(message_handlert &message_handler);
   virtual ~qbf_skizzot();
 
   virtual const std::string solver_text();

src/solvers/qbf/qdimacs_cnf.h

@@ -18,7 +18,10 @@ Author: Daniel Kroening, [email protected]
 class qdimacs_cnft:public dimacs_cnft
 {
 public:
-  qdimacs_cnft() { }
+  explicit qdimacs_cnft(message_handlert &message_handler)
+    : dimacs_cnft(message_handler)
+  {
+  }
   virtual ~qdimacs_cnft() { }
 
   virtual void write_qdimacs_cnf(std::ostream &out);

src/solvers/qbf/qdimacs_core.h

@@ -19,6 +19,11 @@ Author: CM Wintersteiger
 class qdimacs_coret:public qdimacs_cnft
 {
 public:
+  explicit qdimacs_coret(message_handlert &message_handler)
+    : qdimacs_cnft(message_handler)
+  {
+  }
+
   virtual tvt l_get(literalt a) const=0;
   virtual bool is_in_core(literalt l) const=0;
 

src/solvers/refinement/refine_arrays.cpp

@@ -43,7 +43,7 @@ void bv_refinementt::arrays_overapproximated()
   std::list<lazy_constraintt>::iterator it=lazy_array_constraints.begin();
   while(it!=lazy_array_constraints.end())
   {
-    satcheck_no_simplifiert sat_check;
+    satcheck_no_simplifiert sat_check(get_message_handler());
     bv_pointerst solver(ns, sat_check);
     solver.unbounded_array=bv_pointerst::unbounded_arrayt::U_ALL;
 

src/solvers/sat/cnf.h

@@ -19,7 +19,10 @@ class cnft:public propt
 public:
   // For CNF, we don't use index 0 as a matter of principle,
   // so we'll start counting variables at 1.
-  cnft():_no_variables(1) { }
+  explicit cnft(message_handlert &message_handler)
+    : propt(message_handler), _no_variables(1)
+  {
+  }
   virtual ~cnft() { }
 
   virtual literalt land(literalt a, literalt b) override;
@@ -66,7 +69,8 @@ class cnft:public propt
 class cnf_solvert:public cnft
 {
 public:
-  cnf_solvert():status(statust::INIT), clause_counter(0)
+  explicit cnf_solvert(message_handlert &message_handler)
+    : cnft(message_handler), status(statust::INIT), clause_counter(0)
   {
   }
 

src/solvers/sat/cnf_clause_list.h

@@ -23,7 +23,10 @@ Author: Daniel Kroening, [email protected]
 class cnf_clause_listt:public cnft
 {
 public:
-  cnf_clause_listt() { }
+  explicit cnf_clause_listt(message_handlert &message_handler)
+    : cnft(message_handler)
+  {
+  }
   virtual ~cnf_clause_listt() { }
 
   virtual void lcnf(const bvt &bv);
@@ -82,6 +85,11 @@ class cnf_clause_listt:public cnft
 class cnf_clause_list_assignmentt:public cnf_clause_listt
 {
 public:
+  explicit cnf_clause_list_assignmentt(message_handlert &message_handler)
+    : cnf_clause_listt(message_handler)
+  {
+  }
+
   typedef std::vector<tvt> assignmentt;
 
   assignmentt &get_assignment()

src/solvers/sat/dimacs_cnf.cpp

@@ -15,15 +15,11 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <sstream>
 
-dimacs_cnft::dimacs_cnft():break_lines(false)
+dimacs_cnft::dimacs_cnft(message_handlert &message_handler)
+  : cnf_clause_listt(message_handler), break_lines(false)
 {
 }
 
-dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
-{
-  log.set_message_handler(message_handler);
-}
-
 void dimacs_cnft::set_assignment(literalt, bool)
 {
   UNIMPLEMENTED;
@@ -35,7 +31,10 @@ bool dimacs_cnft::is_in_conflict(literalt) const
   return false;
 }
 
-dimacs_cnf_dumpt::dimacs_cnf_dumpt(std::ostream &_out):out(_out)
+dimacs_cnf_dumpt::dimacs_cnf_dumpt(
+  std::ostream &_out,
+  message_handlert &message_handler)
+  : cnft(message_handler), out(_out)
 {
 }
 

src/solvers/sat/dimacs_cnf.h

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 class dimacs_cnft:public cnf_clause_listt
 {
 public:
-  dimacs_cnft();
   explicit dimacs_cnft(message_handlert &);
   virtual ~dimacs_cnft() { }
 
@@ -43,7 +42,7 @@ class dimacs_cnft:public cnf_clause_listt
 class dimacs_cnf_dumpt:public cnft
 {
 public:
-  explicit dimacs_cnf_dumpt(std::ostream &_out);
+  dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
   virtual ~dimacs_cnf_dumpt() { }
 
   virtual const std::string solver_text()

src/solvers/sat/pbs_dimacs_cnf.h

@@ -19,12 +19,13 @@ Author: Alex Groce
 class pbs_dimacs_cnft:public dimacs_cnft
 {
 public:
-  pbs_dimacs_cnft():
-    optimize(false),
-    maximize(false),
-    binary_search(false),
-    goal(0),
-    opt_sum(0)
+  explicit pbs_dimacs_cnft(message_handlert &message_handler)
+    : dimacs_cnft(message_handler),
+      optimize(false),
+      maximize(false),
+      binary_search(false),
+      goal(0),
+      opt_sum(0)
   {
   }
 

src/solvers/sat/satcheck_glucose.cpp

@@ -215,9 +215,11 @@ void satcheck_glucose_baset<T>::set_assignment(literalt a, bool value)
   }
 }
 
-template<typename T>
-satcheck_glucose_baset<T>::satcheck_glucose_baset(T *_solver):
-  solver(_solver)
+template <typename T>
+satcheck_glucose_baset<T>::satcheck_glucose_baset(
+  T *_solver,
+  message_handlert &message_handler)
+  : cnf_solvert(message_handler), solver(_solver)
 {
 }
 
@@ -254,13 +256,19 @@ void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
     INVARIANT(!it->is_constant(), "assumption literals must not be constant");
 }
 
-satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert():
-  satcheck_glucose_baset<Glucose::Solver>(new Glucose::Solver)
+satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_glucose_baset<Glucose::Solver>(
+      new Glucose::Solver,
+      message_handler)
 {
 }
 
-satcheck_glucose_simplifiert::satcheck_glucose_simplifiert():
-  satcheck_glucose_baset<Glucose::SimpSolver>(new Glucose::SimpSolver)
+satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_glucose_baset<Glucose::SimpSolver>(
+      new Glucose::SimpSolver,
+      message_handler)
 {
 }
 

src/solvers/sat/satcheck_glucose.h

@@ -27,7 +27,7 @@ template<typename T>
 class satcheck_glucose_baset:public cnf_solvert
 {
 public:
-  explicit satcheck_glucose_baset(T *);
+  satcheck_glucose_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_glucose_baset();
 
   virtual resultt prop_solve();
@@ -57,15 +57,15 @@ class satcheck_glucose_no_simplifiert:
   public satcheck_glucose_baset<Glucose::Solver>
 {
 public:
-  satcheck_glucose_no_simplifiert();
+  explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text();
 };
 
 class satcheck_glucose_simplifiert:
   public satcheck_glucose_baset<Glucose::SimpSolver>
 {
 public:
-  satcheck_glucose_simplifiert();
+  explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text();
   virtual void set_frozen(literalt a);
   bool is_eliminated(literalt a) const;

src/solvers/sat/satcheck_minisat2.cpp

@@ -293,9 +293,11 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
   }
 }
 
-template<typename T>
-satcheck_minisat2_baset<T>::satcheck_minisat2_baset(T *_solver):
-  solver(_solver), time_limit_seconds(0)
+template <typename T>
+satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
+  T *_solver,
+  message_handlert &message_handler)
+  : cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
 {
 }
 
@@ -336,28 +338,20 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
     }
 }
 
-satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert():
-  satcheck_minisat2_baset<Minisat::Solver>(new Minisat::Solver)
-{
-}
-
 satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
   message_handlert &message_handler)
-  : satcheck_minisat_no_simplifiert()
-{
-  log.set_message_handler(message_handler);
-}
-
-satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
-  satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
+  : satcheck_minisat2_baset<Minisat::Solver>(
+      new Minisat::Solver,
+      message_handler)
 {
 }
 
 satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
   message_handlert &message_handler)
-  : satcheck_minisat_simplifiert()
+  : satcheck_minisat2_baset<Minisat::SimpSolver>(
+      new Minisat::SimpSolver,
+      message_handler)
 {
-  log.set_message_handler(message_handler);
 }
 
 void satcheck_minisat_simplifiert::set_frozen(literalt a)