Stop propt inheriting from messaget

No functional changes.
A propt object should not be used as a messaget so the messaget should
rather be a field.

Author: romainbrenguier

src/solvers/flattening/arrays.cpp

@@ -48,7 +48,7 @@ literalt arrayst::record_array_equality(
   // check types
   if(!base_type_eq(op0.type(), op1.type(), ns))
   {
-    prop.error() << equality.pretty() << messaget::eom;
+    prop.message.error() << equality.pretty() << messaget::eom;
     DATA_INVARIANT(
       false,
       "record_array_equality got equality without matching types");
@@ -117,7 +117,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, with_expr.old().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      prop.message.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
     }
 
@@ -135,7 +135,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, update_expr.old().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      prop.message.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "collect_arrays got 'update' without matching types");
@@ -157,14 +157,14 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      prop.message.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     // check types
     if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      prop.message.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
@@ -518,7 +518,7 @@ void arrayst::add_array_constraints_with(
 
     if(index_expr.type()!=value.type())
     {
-      prop.error() << expr.pretty() << messaget::eom;
+      prop.message.error() << expr.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "with-expression operand should match array element type");
@@ -588,7 +588,7 @@ void arrayst::add_array_constraints_update(
 
     if(index_expr.type()!=value.type())
     {
-      prop.error() << expr.pretty() << messaget::eom;
+      prop.message.error() << expr.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "update operand should match array element type");

src/solvers/prop/prop.h

@@ -21,9 +21,10 @@ Author: Daniel Kroening, [email protected]
 
 /*! \brief TO_BE_DOCUMENTED
 */
-class propt:public messaget
+class propt
 {
 public:
+  messaget message;
   propt() { }
   virtual ~propt() { }
 
@@ -113,7 +114,7 @@ class propt:public messaget
   // Resource limits:
   virtual void set_time_limit_seconds(uint32_t)
   {
-    warning() << "CPU limit ignored (not implemented)" << eom;
+    message.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
   }
 
 protected:

src/solvers/prop/prop_conv.h

@@ -117,7 +117,6 @@ class prop_conv_solvert:public prop_convt
   typedef std::map<irep_idt, literalt> symbolst;
   typedef std::unordered_map<exprt, literalt, irep_hash> cachet;
 
-  const cachet &get_cache() const { return cache; }
   const symbolst &get_symbols() const { return symbols; }
 
   void set_time_limit_seconds(uint32_t lim) override

src/solvers/qbf/qbf_quantor.cpp

@@ -34,10 +34,10 @@ const std::string qbf_quantort::solver_text()
 propt::resultt qbf_quantort::prop_solve()
 {
   {
-    messaget::status() <<
+    message.status() <<
       "Quantor: " <<
       no_variables() << " variables, " <<
-      no_clauses() << " clauses" << eom;
+      no_clauses() << " clauses" << messaget::eom;
   }
 
   std::string qbf_tmp_file="quantor.qdimacs";
@@ -87,19 +87,19 @@ propt::resultt qbf_quantort::prop_solve()
 
     if(!result_found)
     {
-      messaget::error() << "Quantor failed: unknown result" << eom;
+      message.error() << "Quantor failed: unknown result" << messaget::eom;
       return resultt::P_ERROR;
     }
   }
 
   if(result)
   {
-    messaget::status() << "Quantor: TRUE" << eom;
+    message.status() << "Quantor: TRUE" << messaget::eom;
     return resultt::P_SATISFIABLE;
   }
   else
   {
-    messaget::status() << "Quantor: FALSE" << eom;
+    message.status() << "Quantor: FALSE" << messaget::eom;
     return resultt::P_UNSATISFIABLE;
   }
 

src/solvers/qbf/qbf_qube.cpp

@@ -40,10 +40,10 @@ propt::resultt qbf_qubet::prop_solve()
     return resultt::P_SATISFIABLE;
 
   {
-    messaget::status() <<
+    message.status() <<
       "QuBE: " <<
       no_variables() << " variables, " <<
-      no_clauses() << " clauses" << eom;
+      no_clauses() << " clauses" << messaget::eom;
   }
 
   std::string qbf_tmp_file="qube.qdimacs";
@@ -95,19 +95,19 @@ propt::resultt qbf_qubet::prop_solve()
 
     if(!result_found)
     {
-      messaget::error() << "QuBE failed: unknown result" << eom;
+      message.error() << "QuBE failed: unknown result" << messaget::eom;
       return resultt::P_ERROR;
     }
   }
 
   if(result)
   {
-    messaget::status() << "QuBE: TRUE" << eom;
+    message.status() << "QuBE: TRUE" << messaget::eom;
     return resultt::P_SATISFIABLE;
   }
   else
   {
-    messaget::status() << "QuBE: FALSE" << eom;
+    message.status() << "QuBE: FALSE" << messaget::eom;
     return resultt::P_UNSATISFIABLE;
   }