Refactor: remove m_ prefix from member fields

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -336,21 +336,21 @@ class string_constraint_generatort final
   // Used to store information about witnesses for not_contains constraints
   std::map<string_not_contains_constraintt, symbol_exprt> witness;
 private:
-  std::set<array_string_exprt> m_created_strings;
-  unsigned m_symbol_count=0;
-  const messaget m_message;
-  const bool m_force_printable_characters;
-
-  std::vector<exprt> m_axioms;
-  std::vector<symbol_exprt> m_boolean_symbols;
-  std::vector<symbol_exprt> m_index_symbols;
-  const namespacet m_ns;
+  std::set<array_string_exprt> created_strings;
+  unsigned symbol_count=0;
+  const messaget message;
+  const bool force_printable_characters;
+
+  std::vector<exprt> axioms;
+  std::vector<symbol_exprt> boolean_symbols;
+  std::vector<symbol_exprt> index_symbols;
+  const namespacet ns;
   // To each string on which hash_code was called we associate a symbol
   // representing the return value of the hash_code function.
-  std::map<array_string_exprt, exprt> m_hash_code_of_string;
+  std::map<array_string_exprt, exprt> hash_code_of_string;
 
   // Pool used for the intern method
-  std::map<array_string_exprt, symbol_exprt> m_intern_of_string;
+  std::map<array_string_exprt, symbol_exprt> intern_of_string;
 
   // associate arrays to char pointers
   std::map<exprt, array_string_exprt> arrays_of_pointers_;

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -41,27 +41,27 @@ exprt string_constraint_generatort::add_axioms_for_code_point(
 
   binary_relation_exprt small(code_point, ID_lt, hex010000);
   implies_exprt a1(small, res.axiom_for_has_length(1));
-  m_axioms.push_back(a1);
+  axioms.push_back(a1);
 
   implies_exprt a2(not_exprt(small), res.axiom_for_has_length(2));
-  m_axioms.push_back(a2);
+  axioms.push_back(a2);
 
   typecast_exprt code_point_as_char(code_point, char_type);
   implies_exprt a3(small, equal_exprt(res[0], code_point_as_char));
-  m_axioms.push_back(a3);
+  axioms.push_back(a3);
 
   plus_exprt first_char(
     hexD800, div_exprt(minus_exprt(code_point, hex010000), hex0400));
   implies_exprt a4(
     not_exprt(small),
     equal_exprt(res[0], typecast_exprt(first_char, char_type)));
-  m_axioms.push_back(a4);
+  axioms.push_back(a4);
 
   plus_exprt second_char(hexDC00, mod_exprt(code_point, hex0400));
   implies_exprt a5(
     not_exprt(small),
     equal_exprt(res[1], typecast_exprt(second_char, char_type)));
-  m_axioms.push_back(a5);
+  axioms.push_back(a5);
 
   return from_integer(0, get_return_code_type());
 }
@@ -136,8 +136,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
     is_low_surrogate(str[plus_exprt_with_overflow_check(pos, index1)]);
   const and_exprt return_pair(is_high_surrogate(str[pos]), is_low);
 
-  m_axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
-  m_axioms.push_back(
+  axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
+  axioms.push_back(
     implies_exprt(not_exprt(return_pair), equal_exprt(result, char1_as_int)));
   return result;
 }
@@ -167,8 +167,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   const and_exprt return_pair(
     is_high_surrogate(char1), is_low_surrogate(char2));
 
-  m_axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
-  m_axioms.push_back(
+  axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
+  axioms.push_back(
     implies_exprt(not_exprt(return_pair), equal_exprt(result, char2_as_int)));
   return result;
 }
@@ -189,8 +189,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const symbol_exprt result = fresh_symbol("code_point_count", return_type);
   const minus_exprt length(end, begin);
   const div_exprt minimum(length, from_integer(2, length.type()));
-  m_axioms.push_back(binary_relation_exprt(result, ID_le, length));
-  m_axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
+  axioms.push_back(binary_relation_exprt(result, ID_le, length));
+  axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
 
   return result;
 }
@@ -212,8 +212,8 @@ exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
 
   const exprt minimum = plus_exprt_with_overflow_check(index, offset);
   const exprt maximum = plus_exprt_with_overflow_check(minimum, offset);
-  m_axioms.push_back(binary_relation_exprt(result, ID_le, maximum));
-  m_axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
+  axioms.push_back(binary_relation_exprt(result, ID_le, maximum));
+  axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
 
   return result;
 }

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -41,11 +41,11 @@ exprt string_constraint_generatort::add_axioms_for_equals(
   //       || (0<=witness<s1.length &&s1[witness]!=s2[witness])
 
   implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  m_axioms.push_back(a1);
+  axioms.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_equal", index_type);
   string_constraintt a2(qvar, s1.length(), eq, equal_exprt(s1[qvar], s2[qvar]));
-  m_axioms.push_back(a2);
+  axioms.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
   exprt zero=from_integer(0, index_type);
@@ -57,7 +57,7 @@ exprt string_constraint_generatort::add_axioms_for_equals(
     notequal_exprt(s1.length(), s2.length()),
     equal_exprt(witness, from_integer(-1, index_type)));
   implies_exprt a3(not_exprt(eq), or_exprt(diff_length, witnessing));
-  m_axioms.push_back(a3);
+  axioms.push_back(a3);
 
   return tc_eq;
 }
@@ -118,14 +118,14 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
   // a3 : !eq => |s1|!=s2 || (0 <=witness<|s1| &&!char_equal_ignore_case)
 
   const implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  m_axioms.push_back(a1);
+  axioms.push_back(a1);
 
   const symbol_exprt qvar =
     fresh_univ_index("QA_equal_ignore_case", index_type);
   const exprt constr2 =
     character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
   const string_constraintt a2(qvar, s1.length(), eq, constr2);
-  m_axioms.push_back(a2);
+  axioms.push_back(a2);
 
   const symbol_exprt witness =
     fresh_exist_index("witness_unequal_ignore_case", index_type);
@@ -141,7 +141,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
     or_exprt(
       notequal_exprt(s1.length(), s2.length()),
       and_exprt(bound_witness, witness_diff)));
-  m_axioms.push_back(a3);
+  axioms.push_back(a3);
 
   return typecast_exprt(eq, f.type());
 }
@@ -158,7 +158,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code(
   const typet &return_type = f.type();
   const typet &index_type = str.length().type();
 
-  auto pair=m_hash_code_of_string.insert(
+  auto pair=hash_code_of_string.insert(
     std::make_pair(str, fresh_symbol("hash", return_type)));
   const exprt hash = pair.first->second;
 
@@ -168,7 +168,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code(
   //   c3: (|str|==|s| && exists i<|s|. s[i]!=str[i])
 
   // WARNING: the specification may be incomplete
-  for(auto it : m_hash_code_of_string)
+  for(auto it : hash_code_of_string)
   {
     const symbol_exprt i = fresh_exist_index("index_hash", index_type);
     const equal_exprt c1(it.second, hash);
@@ -178,7 +178,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code(
       and_exprt(
         notequal_exprt(str[i], it.first[i]),
         and_exprt(str.axiom_for_length_gt(i), axiom_for_is_positive_index(i))));
-    m_axioms.push_back(or_exprt(c1, or_exprt(c2, c3)));
+    axioms.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
   return hash;
 }
@@ -212,12 +212,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const equal_exprt res_null(res, from_integer(0, return_type));
   const implies_exprt a1(res_null, equal_exprt(s1.length(), s2.length()));
-  m_axioms.push_back(a1);
+  axioms.push_back(a1);
 
   const symbol_exprt i = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a2(
     i, s1.length(), res_null, equal_exprt(s1[i], s2[i]));
-  m_axioms.push_back(a2);
+  axioms.push_back(a2);
 
   const symbol_exprt x = fresh_exist_index("index_compare_to", index_type);
   const equal_exprt ret_char_diff(
@@ -243,12 +243,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
     and_exprt(
       binary_relation_exprt(x, ID_ge, from_integer(0, return_type)),
       or_exprt(cond1, cond2)));
-  m_axioms.push_back(a3);
+  axioms.push_back(a3);
 
   const symbol_exprt i2 = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a4(
     i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
-  m_axioms.push_back(a4);
+  axioms.push_back(a4);
 
   return res;
 }
@@ -266,7 +266,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern(
   const typet &return_type=f.type();
   const typet index_type = str.length().type();
 
-  auto pair=m_intern_of_string.insert(
+  auto pair=intern_of_string.insert(
     std::make_pair(str, fresh_symbol("pool", return_type)));
   const symbol_exprt intern = pair.first->second;
 
@@ -276,16 +276,16 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern(
   //    || (|str|==|s| &&exists i<|s|. s[i]!=str[i])
 
   exprt::operandst disj;
-  for(auto it : m_intern_of_string)
+  for(auto it : intern_of_string)
     disj.push_back(equal_exprt(intern, it.second));
-  m_axioms.push_back(disjunction(disj));
+  axioms.push_back(disjunction(disj));
 
   // WARNING: the specification may be incomplete or incorrect
-  for(auto it : m_intern_of_string)
+  for(auto it : intern_of_string)
     if(it.second!=str)
     {
       symbol_exprt i=fresh_exist_index("index_intern", index_type);
-      m_axioms.push_back(
+      axioms.push_back(
         or_exprt(
           equal_exprt(it.second, intern),
           or_exprt(

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -45,20 +45,20 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   exprt res_length=plus_exprt_with_overflow_check(
     s1.length(), minus_exprt(end_index, start_index));
   implies_exprt a1(prem, equal_exprt(res.length(), res_length));
-  m_axioms.push_back(a1);
+  axioms.push_back(a1);
 
   implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length()));
-  m_axioms.push_back(a2);
+  axioms.push_back(a2);
 
   symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type());
   string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  m_axioms.push_back(a3);
+  axioms.push_back(a3);
 
   symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type());
   equal_exprt res_eq(
     res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]);
   string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq);
-  m_axioms.push_back(a4);
+  axioms.push_back(a4);
 
   // We should have a enum type for the possible error codes
   return from_integer(0, res.length().type());
@@ -83,14 +83,14 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   const typet &index_type = res.length().type();
   const equal_exprt a1(
     res.length(), plus_exprt(s1.length(), from_integer(1, index_type)));
-  m_axioms.push_back(a1);
+  axioms.push_back(a1);
 
   symbol_exprt idx = fresh_univ_index("QA_index_concat_char", index_type);
   string_constraintt a2(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  m_axioms.push_back(a2);
+  axioms.push_back(a2);
 
   equal_exprt a3(res[s1.length()], c);
-  m_axioms.push_back(a3);
+  axioms.push_back(a3);
 
   // We should have a enum type for the possible error codes
   return from_integer(0, get_return_code_type());

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -43,12 +43,12 @@ exprt string_constraint_generatort::add_axioms_for_constant(
     const exprt idx = from_integer(i, index_type);
     const exprt c = from_integer(str[i], char_type);
     const equal_exprt lemma(res[idx], c);
-    m_axioms.push_back(lemma);
+    axioms.push_back(lemma);
   }
 
   const exprt s_length = from_integer(str.size(), index_type);
 
-  m_axioms.push_back(res.axiom_for_has_length(s_length));
+  axioms.push_back(res.axiom_for_has_length(s_length));
   return from_integer(0, get_return_code_type());
 }
 
@@ -61,7 +61,7 @@ exprt string_constraint_generatort::add_axioms_for_empty_string(
 {
   PRECONDITION(f.arguments().size() == 2);
   exprt length = f.arguments()[0];
-  m_axioms.push_back(equal_exprt(length, from_integer(0, length.type())));
+  axioms.push_back(equal_exprt(length, from_integer(0, length.type())));
   return from_integer(0, get_return_code_type());
 }
 

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -249,7 +249,7 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part(
 
   and_exprt a1(res.axiom_for_length_gt(1),
                res.axiom_for_length_le(max));
-  m_axioms.push_back(a1);
+  axioms.push_back(a1);
 
   equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
 
@@ -287,10 +287,10 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part(
   }
 
   exprt a2=conjunction(digit_constraints);
-  m_axioms.push_back(a2);
+  axioms.push_back(a2);
 
   equal_exprt a3(int_expr, sum);
-  m_axioms.push_back(a3);
+  axioms.push_back(a3);
 
   return from_integer(0, signedbv_typet(32));
 }

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -328,12 +328,12 @@ string_constraint_generatort::add_axioms_for_format_specifier(
   case format_specifiert::DATE_TIME:
     // TODO: DateTime not implemented
     // For all these unimplemented cases we return a non-deterministic string
-    m_message.warning() << "unimplemented format specifier: " << fs.conversion
-                        << m_message.eom;
+    message.warning() << "unimplemented format specifier: " << fs.conversion
+                        << message.eom;
     return fresh_string(index_type, char_type);
   default:
-    m_message.error() << "invalid format specifier: " << fs.conversion
-                      << m_message.eom;
+    message.error() << "invalid format specifier: " << fs.conversion
+                      << message.eom;
     INVARIANT(
       false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
     throw 0;
@@ -463,9 +463,9 @@ exprt string_constraint_generatort::add_axioms_for_format(
   }
   else
   {
-    m_message.warning()
+    message.warning()
       << "ignoring format function with non constant first argument"
-      << m_message.eom;
+      << message.eom;
     return from_integer(1, f.type());
   }
 }