Pass message_handler to incremental_solver

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

src/2ls/summary_checker_base.h

@@ -61,6 +61,7 @@ class summary_checker_baset:public messaget
   {
     messaget::set_message_handler(_message_handler);
     ssa_inliner.set_message_handler(_message_handler);
+    ssa_db.set_message_handler(_message_handler);
   }
 
   propertiest property_map;

src/domains/incremental_solver.h

@@ -37,7 +37,9 @@ class incremental_solvert:public messaget
 
   explicit incremental_solvert(
     const namespacet &_ns,
+    message_handlert &_message_handler,
     bool _arith_refinement=false):
+    messaget(_message_handler),
     sat_check(NULL),
     solver(NULL),
     ns(_ns),
@@ -110,9 +112,10 @@ class incremental_solvert:public messaget
 
   static incremental_solvert *allocate(
     const namespacet &_ns,
+    message_handlert &_message_handler,
     bool arith_refinement=false)
   {
-    return new incremental_solvert(_ns, arith_refinement);
+    return new incremental_solvert(_ns, _message_handler, arith_refinement);
   }
 
   inline prop_convt & get_solver() { return *solver; }

src/domains/lexlinrank_domain.cpp

@@ -43,7 +43,7 @@ void lexlinrank_domaint::initialize_value(domaint::valuet &value)
 void lexlinrank_domaint::initialize()
 {
   delete inner_solver;
-  inner_solver=incremental_solvert::allocate(ns);
+  inner_solver=incremental_solvert::allocate(ns, message_handler);
 }
 
 bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved)
@@ -133,7 +133,7 @@ bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved)
       {
         number_elements_per_row[row]++;
         delete inner_solver;
-        inner_solver=incremental_solvert::allocate(ns);
+        inner_solver=incremental_solvert::allocate(ns, message_handler);
         reset_refinements();
 
         rank[row].add_element();

src/domains/lexlinrank_domain.h

@@ -102,14 +102,16 @@ class lexlinrank_domaint:public simple_domaint
     replace_mapt &_renaming_map,
     unsigned _max_elements, // lexicographic components
     unsigned _max_inner_iterations,
-    const namespacet &_ns):
+    const namespacet &_ns,
+    message_handlert &_message_handler):
     simple_domaint(_domain_number, _renaming_map, _ns),
     refinement_level(0),
     max_elements(_max_elements),
     max_inner_iterations(_max_inner_iterations),
-    number_inner_iterations(0)
+    number_inner_iterations(0),
+    message_handler(_message_handler)
   {
-    inner_solver=incremental_solvert::allocate(_ns);
+    inner_solver=incremental_solvert::allocate(_ns, _message_handler);
   }
 
 
@@ -162,6 +164,7 @@ class lexlinrank_domaint:public simple_domaint
   const unsigned max_inner_iterations;
   incremental_solvert *inner_solver;
   unsigned number_inner_iterations;
+  message_handlert &message_handler;
 
   std::vector<unsigned> number_elements_per_row;
 };

src/domains/linrank_domain.h

@@ -79,14 +79,16 @@ class linrank_domaint:public simple_domaint
     replace_mapt &_renaming_map,
     unsigned _max_elements, // lexicographic components
     unsigned _max_inner_iterations,
-    const namespacet &_ns):
+    const namespacet &_ns,
+    message_handlert &_message_handler):
     simple_domaint(_domain_number, _renaming_map, _ns),
     refinement_level(0),
     max_elements(_max_elements),
     max_inner_iterations(_max_inner_iterations),
-    number_inner_iterations(0)
+    number_inner_iterations(0),
+    message_handler(_message_handler)
   {
-    inner_solver=incremental_solvert::allocate(_ns);
+    inner_solver=incremental_solvert::allocate(_ns, _message_handler);
   }
 
   // initialize value
@@ -132,6 +134,7 @@ class linrank_domaint:public simple_domaint
   const unsigned max_inner_iterations;
   incremental_solvert *inner_solver;
   unsigned number_inner_iterations;
+  message_handlert &message_handler;
 };
 
 #endif // CPROVER_2LS_DOMAINS_LINRANK_DOMAIN_H

src/domains/template_generator_ranking.cpp

@@ -38,7 +38,8 @@ void template_generator_rankingt::operator()(
         post_renaming_map,
         options.get_unsigned_int_option("lexicographic-ranking-function"),
         options.get_unsigned_int_option("max-inner-ranking-iterations"),
-        SSA.ns));
+        SSA.ns,
+        get_message_handler()));
   }
   else
   {
@@ -48,7 +49,8 @@ void template_generator_rankingt::operator()(
         post_renaming_map,
         options.get_unsigned_int_option("lexicographic-ranking-function"),
         options.get_unsigned_int_option("max-inner-ranking-iterations"),
-        SSA.ns));
+        SSA.ns,
+        get_message_handler()));
   }
   collect_variables_ranking(SSA, forward);
 

src/ssa/ssa_db.h

@@ -18,7 +18,7 @@ Author: Peter Schrammel
 #include <domains/incremental_solver.h>
 #include <goto-programs/goto_functions.h>
 
-class ssa_dbt
+class ssa_dbt:public messaget
 {
 public:
   typedef irep_idt function_namet;
@@ -52,6 +52,7 @@ class ssa_dbt
     the_solvers[function_name]=
       incremental_solvert::allocate(
         store.at(function_name)->ns,
+        get_message_handler(),
         options.get_bool_option("refine"));
     return *the_solvers.at(function_name);
   }