Implement builtin string_to_lower_case function

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -187,6 +187,25 @@ exprt string_set_char_builtin_functiont::length_constraint() const
     equal_exprt(return_code, return_value));
 }
 
+optionalt<exprt> string_to_lower_case_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  auto input_opt = eval_string(input, get_value);
+  if(!input_opt)
+    return {};
+  for(mp_integer &c : input_opt.value())
+  {
+    if(
+      ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) ||
+      (0xd8 <= c && c <= 0xde))
+      c += 0x20;
+  }
+  const auto length =
+    from_integer(input_opt.value().size(), result.length().type());
+  const array_typet type(result.type().subtype(), length);
+  return make_string(input_opt.value(), type);
+}
+
 std::vector<mp_integer> string_insertion_builtin_functiont::eval(
   const std::vector<mp_integer> &input1_value,
   const std::vector<mp_integer> &input2_value,

src/solvers/refinement/string_builtin_function.h

@@ -177,6 +177,39 @@ class string_set_char_builtin_functiont
   exprt length_constraint() const override;
 };
 
+/// Converting each uppercase character of Basic Latin and Latin-1 supplement
+/// to the corresponding lowercase character.
+class string_to_lower_case_builtin_functiont
+  : public string_transformation_builtin_functiont
+{
+public:
+  string_to_lower_case_builtin_functiont(
+    const exprt &return_code,
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
+  {
+  }
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  std::string name() const override
+  {
+    return "to_lower_case";
+  }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_to_lower_case(result, input);
+  };
+
+  exprt length_constraint() const override
+  {
+    return equal_exprt(result.length(), input.length());
+  };
+};
+
 /// String inserting a string into another one
 class string_insertion_builtin_functiont : public string_builtin_functiont
 {

src/solvers/refinement/string_refinement_util.cpp

@@ -232,6 +232,10 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
     return util_make_unique<string_set_char_builtin_functiont>(
       return_code, fun_app.arguments(), array_pool);
 
+  if(id == ID_cprover_string_to_lower_case_func)
+    return util_make_unique<string_to_lower_case_builtin_functiont>(
+      return_code, fun_app.arguments(), array_pool);
+
   return util_make_unique<string_builtin_function_with_no_evalt>(
     return_code, fun_app, array_pool);
 }