Use numeric_cast instead of refinement/expr_cast

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -13,7 +13,7 @@ Author: Romain Brenguier, [email protected]
 
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
-#include "expr_cast.h"
+#include <util/arith_tools.h>
 
 /// Reduce or extend a string to have the given length
 ///
@@ -442,8 +442,8 @@ static optionalt<std::pair<exprt, exprt>> to_char_pair(
     return std::make_pair(expr1, expr2);
   const auto expr1_str = get_string_expr(expr1);
   const auto expr2_str = get_string_expr(expr2);
-  const auto expr1_length=expr_cast<size_t>(expr1_str.length());
-  const auto expr2_length=expr_cast<size_t>(expr2_str.length());
+  const auto expr1_length = numeric_cast<std::size_t>(expr1_str.length());
+  const auto expr2_length = numeric_cast<std::size_t>(expr2_str.length());
   if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
     return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
   return { };

src/solvers/refinement/string_refinement.cpp

@@ -22,12 +22,11 @@ Author: Alberto Griggio, [email protected]
 #include <iomanip>
 #include <stack>
 #include <util/expr_iterator.h>
-#include <util/optional.h>
+#include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <java_bytecode/java_types.h>
-#include "expr_cast.h"
 
 static exprt substitute_array_with_expr(const exprt &expr, const exprt &index);
 
@@ -852,7 +851,6 @@ static optionalt<exprt> get_array(
 /// \return a string
 static std::string string_of_array(const array_exprt &arr)
 {
-  unsigned n;
   if(arr.type().id()!=ID_array)
       return std::string("");
 
@@ -1010,7 +1008,7 @@ exprt fill_in_array_with_expr(
   std::map<std::size_t, exprt> initial_map;
 
   // Set the last index to be sure the array will have the right length
-  const auto &array_size_opt = expr_cast<std::size_t>(array_type.size());
+  const auto &array_size_opt = numeric_cast<std::size_t>(array_type.size());
   if(array_size_opt && *array_size_opt > 0)
     initial_map.emplace(
       *array_size_opt - 1,
@@ -1022,7 +1020,8 @@ exprt fill_in_array_with_expr(
     // statements
     const with_exprt &with_expr = to_with_expr(it);
     const exprt &then_expr=with_expr.new_value();
-    const auto index=expr_cast_v<std::size_t>(with_expr.where());
+    const auto index =
+      numeric_cast_v<std::size_t>(to_constant_expr(with_expr.where()));
     if(
       index < string_max_length && (!array_size_opt || index < *array_size_opt))
       initial_map.emplace(index, then_expr);
@@ -1047,7 +1046,7 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length)
 
   // Map of the parts of the array that are initialized
   std::map<std::size_t, exprt> initial_map;
-  const auto &array_size_opt = expr_cast<std::size_t>(array_type.size());
+  const auto &array_size_opt = numeric_cast<std::size_t>(array_type.size());
 
   if(array_size_opt && *array_size_opt > 0)
     initial_map.emplace(
@@ -1180,14 +1179,14 @@ static exprt negation_of_not_contains_constraint(
   const exprt &ubu=axiom.univ_upper_bound();
   if(lbu.id()==ID_constant && ubu.id()==ID_constant)
   {
-    const auto lb_int=expr_cast<mp_integer>(lbu);
-    const auto ub_int=expr_cast<mp_integer>(ubu);
+    const auto lb_int = numeric_cast<mp_integer>(lbu);
+    const auto ub_int = numeric_cast<mp_integer>(ubu);
     if(!lb_int || !ub_int || *ub_int<=*lb_int)
       return false_exprt();
   }
 
-  const auto lbe=expr_cast_v<mp_integer>(axiom.exists_lower_bound());
-  const auto ube=expr_cast_v<mp_integer>(axiom.exists_upper_bound());
+  const auto lbe = numeric_cast_v<mp_integer>(axiom.exists_lower_bound());
+  const auto ube = numeric_cast_v<mp_integer>(axiom.exists_upper_bound());
 
   // If the premise is false, the implication is trivially true, so the
   // negation is false.
@@ -1230,8 +1229,8 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
   const exprt &ub=axiom.upper_bound();
   if(lb.id()==ID_constant && ub.id()==ID_constant)
   {
-    const auto lb_int=expr_cast<mp_integer>(lb);
-    const auto ub_int=expr_cast<mp_integer>(ub);
+    const auto lb_int = numeric_cast<mp_integer>(lb);
+    const auto ub_int = numeric_cast<mp_integer>(ub);
     if(!lb_int || !ub_int || ub_int<=lb_int)
       return false_exprt();
   }
@@ -1786,7 +1785,7 @@ static void add_to_index_set(
   exprt i)
 {
   simplify(i, ns);
-  const bool is_size_t=expr_cast<std::size_t>(i).has_value();
+  const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
   if(i.id()!=ID_constant || is_size_t)
   {
     std::vector<exprt> sub_arrays;
@@ -2047,7 +2046,7 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length)
     {
       const exprt &index=expr.operands()[i];
       const exprt &value=expr.operands()[i+1];
-      const auto index_value=expr_cast<std::size_t>(index);
+      const auto index_value = numeric_cast<std::size_t>(index);
       if(!index.is_constant() ||
          (index_value && *index_value<string_max_length))
         ret_expr=with_exprt(ret_expr, index, value);
@@ -2097,7 +2096,7 @@ exprt string_refinementt::get(const exprt &expr) const
       if(set.find(arr) != set.end())
       {
         exprt length = super_get(arr.length());
-        if(const auto n = expr_cast<std::size_t>(length))
+        if(const auto n = numeric_cast<std::size_t>(length))
         {
           exprt arr_model =
             array_exprt(array_typet(arr.type().subtype(), length));