Require a message handler when constructing a propt

tautschnig · tautschnig · commit 89641a2b47b8 · 2019-02-03T02:20:18.000Z
Constructing a messaget without a message handler is deprecated.
diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -6,6 +6,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 
 \*******************************************************************/
 
+#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;
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/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)
diff --git a/src/solvers/flattening/bv_minimize.h b/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)
   {
   }
 
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
@@ -24,7 +24,9 @@ Author: Daniel Kroening, kroening@kroening.com
 class propt
 {
 public:
-  propt() { }
+  explicit propt(message_handlert &message_handler) : log(message_handler)
+  {
+  }
 
   virtual ~propt() { }
 
diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp
@@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/invariant.h>
 
-qbf_quantort::qbf_quantort()
+qbf_quantort::qbf_quantort(message_handlert &message_handler)
+  : qdimacs_cnft(message_handler)
 {
 }
 
diff --git a/src/solvers/qbf/qbf_quantor.h b/src/solvers/qbf/qbf_quantor.h
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 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();
diff --git a/src/solvers/qbf/qbf_qube.cpp b/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;
diff --git a/src/solvers/qbf/qbf_qube.h b/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();
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/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";
diff --git a/src/solvers/qbf/qbf_qube_core.h b/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();
diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp
@@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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;
diff --git a/src/solvers/qbf/qbf_skizzo.h b/src/solvers/qbf/qbf_skizzo.h
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 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();
diff --git a/src/solvers/qbf/qdimacs_cnf.h b/src/solvers/qbf/qdimacs_cnf.h
@@ -18,7 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com
 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);
diff --git a/src/solvers/qbf/qdimacs_core.h b/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;
 
diff --git a/src/solvers/refinement/refine_arrays.cpp b/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;
 
diff --git a/src/solvers/sat/cnf.h b/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)
   {
   }
 
diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
@@ -23,7 +23,10 @@ Author: Daniel Kroening, kroening@kroening.com
 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()
diff --git a/src/solvers/sat/dimacs_cnf.cpp b/src/solvers/sat/dimacs_cnf.cpp
@@ -15,15 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #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)
 {
 }
 
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 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()
diff --git a/src/solvers/sat/pbs_dimacs_cnf.h b/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)
   {
   }
 
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/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)
 {
 }
 
diff --git a/src/solvers/sat/satcheck_glucose.h b/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;
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/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)
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
diff --git a/src/solvers/strings/string_constraint.cpp b/src/solvers/strings/string_constraint.cpp
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
diff --git a/unit/solvers/floatbv/float_utils.cpp b/unit/solvers/floatbv/float_utils.cpp

Original file line number	Diff line number	Diff line change
`@@ -48,8 +48,8 @@ class bv_minimizing_dect:public bv_pointerst`
`48`	`48`	`return "Bit vector minimizing SAT";`
`49`	`49`	`}`
`50`	`50`
`51`		`- explicit bv_minimizing_dect(const namespacet &_ns):`
`52`		`- bv_pointerst(_ns, satcheck)`
	`51`	`+ bv_minimizing_dect(const namespacet &_ns, message_handlert &message_handler)`
	`52`	`+ : bv_pointerst(_ns, satcheck), satcheck(message_handler)`
`53`	`53`	`{`
`54`	`54`	`}`
`55`	`55`
Original file line number	Diff line number	Diff line change
`@@ -24,7 +24,9 @@ Author: Daniel Kroening, kroening@kroening.com`
`24`	`24`	`class propt`
`25`	`25`	`{`
`26`	`26`	`public:`
`27`		`- propt() { }`
	`27`	`+ explicit propt(message_handlert &message_handler) : log(message_handler)`
	`28`	`+ {`
	`29`	`+ }`
`28`	`30`
`29`	`31`	`virtual ~propt() { }`
`30`	`32`
Original file line number	Diff line number	Diff line change
`@@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com`
`13`	`13`
`14`	`14`	`#include <util/invariant.h>`
`15`	`15`
`16`		`-qbf_quantort::qbf_quantort()`
	`16`	`+qbf_quantort::qbf_quantort(message_handlert &message_handler)`
	`17`	`+ : qdimacs_cnft(message_handler)`
`17`	`18`	`{`
`18`	`19`	`}`
`19`	`20`
Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com`
`15`	`15`	`class qbf_quantort:public qdimacs_cnft`
`16`	`16`	`{`
`17`	`17`	`public:`
`18`		`- qbf_quantort();`
	`18`	`+ explicit qbf_quantort(message_handlert &message_handler);`
`19`	`19`	`virtual ~qbf_quantort();`
`20`	`20`
`21`	`21`	`virtual const std::string solver_text();`
Original file line number	Diff line number	Diff line change
`@@ -13,7 +13,8 @@ Author: CM Wintersteiger`
`13`	`13`
`14`	`14`	`#include <util/invariant.h>`
`15`	`15`
`16`		`-qbf_qubet::qbf_qubet()`
	`16`	`+qbf_qubet::qbf_qubet(message_handlert &message_handler)`
	`17`	`+ : qdimacs_cnft(message_handler)`
`17`	`18`	`{`
`18`	`19`	`// skizzo crashes on broken lines`
`19`	`20`	`break_lines=false;`
Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,7 @@ Author: CM Wintersteiger`
`15`	`15`	`class qbf_qubet:public qdimacs_cnft`
`16`	`16`	`{`
`17`	`17`	`public:`
`18`		`- qbf_qubet();`
	`18`	`+ explicit qbf_qubet(message_handlert &message_handler);`
`19`	`19`	`virtual ~qbf_qubet();`
`20`	`20`
`21`	`21`	`virtual const std::string solver_text();`
Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,8 @@ Author: CM Wintersteiger`
`15`	`15`	`#include <util/arith_tools.h>`
`16`	`16`	`#include <util/invariant.h>`
`17`	`17`
`18`		`-qbf_qube_coret::qbf_qube_coret() : qdimacs_coret()`
	`18`	`+qbf_qube_coret::qbf_qube_coret(message_handlert &message_handler)`
	`19`	`+ : qdimacs_coret(message_handler)`
`19`	`20`	`{`
`20`	`21`	`break_lines=false;`
`21`	`22`	`qbf_tmp_file="qube.qdimacs";`