Linting corrections to /solvers/refinement/

Author: Joel Allred

src/solvers/refinement/string_constraint_generator.h

@@ -96,7 +96,7 @@ class string_constraint_generatort
   const std::size_t MAX_FLOAT_LENGTH=15;
   const std::size_t MAX_DOUBLE_LENGTH=30;
 
-  std::map<function_application_exprt,exprt> function_application_cache;
+  std::map<function_application_exprt, exprt> function_application_cache;
 
   static irep_idt extract_java_string(const symbol_exprt &s);
 
@@ -305,7 +305,6 @@ class string_constraint_generatort
   exprt is_low_surrogate(const exprt &chr) const;
   exprt character_equals_ignore_case(
     exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z);
-
 };
 
 #endif

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -289,7 +289,8 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   axioms.push_back(a3);
 
   symbol_exprt i2=fresh_univ_index("QA_compare_to", index_type);
-  string_constraintt a4(i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
+  string_constraintt a4(
+    i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
   axioms.push_back(a4);
 
   return res;

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -381,7 +381,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     function_application_exprt new_expr(expr);
     // TODO: This part needs some improvement.
     // Stripping the symbol name is not a very robust process.
-    new_expr.function() = symbol_exprt(str_id.substr(0,pos+4));
+    new_expr.function() = symbol_exprt(str_id.substr(0, pos+4));
     assert(get_mode()==ID_java);
     new_expr.type() = refined_string_typet(java_int_type(), java_char_type());
 
@@ -402,7 +402,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
   if(pos!=std::string::npos)
   {
     function_application_exprt new_expr(expr);
-    new_expr.function() = symbol_exprt(str_id.substr(0,pos+4));
+    new_expr.function() = symbol_exprt(str_id.substr(0, pos+4));
     new_expr.type() = refined_string_typet(java_int_type(), java_char_type());
 
     auto res_it=function_application_cache.insert(std::make_pair(new_expr,

src/solvers/refinement/string_refinement.cpp

@@ -16,7 +16,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/cprover_prefix.h>
 #include <util/replace_expr.h>
 #include <util/refined_string_type.h>
-#include <util/replace_expr.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_refinement.h>
 #include <langapi/language_util.h>
@@ -126,7 +125,7 @@ void string_refinementt::add_symbol_to_symbol_map
   reverse_symbol_resolve[new_rhs].push_back(lhs);
 
   std::list<exprt> symbols_to_update_with_new_rhs(reverse_symbol_resolve[rhs]);
-  for(exprt item:symbols_to_update_with_new_rhs)
+  for(exprt item : symbols_to_update_with_new_rhs)
   {
     symbol_resolve[item]=new_rhs;
     reverse_symbol_resolve[new_rhs].push_back(item);
@@ -154,8 +153,8 @@ void string_refinementt::set_char_array_equality(
     for(size_t i=0, ilim=rhs.operands().size(); i!=ilim; ++i)
     {
       // Introduce axioms to map symbolic rhs to its char array.
-      index_exprt arraycell(rhs, from_integer(i,index_type));
-      equal_exprt arrayeq(arraycell,rhs.operands()[i]);
+      index_exprt arraycell(rhs, from_integer(i, index_type));
+      equal_exprt arrayeq(arraycell, rhs.operands()[i]);
       generator.axioms.push_back(arrayeq);
     }
   }
@@ -503,7 +502,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size)
   }
 
   unsigned n;
-  if(to_unsigned_integer(to_constant_expr(size), n))
+  if(to_unsigned_integer(to_constant_expr(size_val), n))
   {
     debug() << "(sr::get_array) size is not a valid";
     return empty_ret;
@@ -524,7 +523,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size)
     return empty_ret;
   }
 
-  unsigned concrete_array[n];
+  std::vector<unsigned> concrete_array(n);
 
   if(arr_val.id()=="array-list")
   {
@@ -537,7 +536,6 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size)
         if(idx<n)
         {
           exprt value=arr_val.operands()[i*2+1];
-          to_unsigned_integer(to_constant_expr(value), concrete_array[i]);
           to_unsigned_integer(to_constant_expr(value), concrete_array[idx]);
         }
       }
@@ -561,8 +559,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size)
 
   for(size_t i=0; i<n; i++)
   {
-    unsigned c=concrete_array[i];
-    exprt c_expr=from_integer(c, char_type);
+    exprt c_expr=from_integer(concrete_array[i], char_type);
     ret.move_to_operands(c_expr);
   }
 
@@ -630,7 +627,7 @@ replace_mapt string_refinementt::fill_model()
 {
   replace_mapt fmodel;
 
-  for(auto it:symbol_resolve)
+  for(auto it : symbol_resolve)
   {
     if(refined_string_typet::is_refined_string_type(it.second.type()))
     {