Refactor string_concat_char builtin function

This makes the argument an explicit field in the class which is clearer
and safer than using a vector of arguments.

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -29,33 +29,6 @@ string_transformation_builtin_functiont::
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
   input = array_pool.find(arg1.op1(), arg1.op0());
   result = array_pool.find(fun_args[1], fun_args[0]);
-  args.insert(args.end(), fun_args.begin() + 3, fun_args.end());
-}
-
-optionalt<exprt> string_transformation_builtin_functiont::eval(
-  const std::function<exprt(const exprt &)> &get_value) const
-{
-  const auto &input_value = eval_string(input, get_value);
-  if(!input_value.has_value())
-    return {};
-
-  std::vector<mp_integer> arg_values;
-  const auto &insert = std::back_inserter(arg_values);
-  const mp_integer unknown('?');
-  std::transform(
-    args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
-      if(const auto val = numeric_cast<mp_integer>(get_value(e)))
-        return *val;
-      INVARIANT(
-        get_value(e).id() == ID_unknown,
-        "array valuation should only contain constants and unknown");
-      return unknown;
-    });
-
-  const auto result_value = eval(*input_value, arg_values);
-  const auto length = from_integer(result_value.size(), result.length().type());
-  const array_typet type(result.type().subtype(), length);
-  return make_string(result_value, type);
 }
 
 string_insertion_builtin_functiont::string_insertion_builtin_functiont(
@@ -162,14 +135,25 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
   return result;
 }
 
-std::vector<mp_integer> string_concat_char_builtin_functiont::eval(
-  const std::vector<mp_integer> &input_value,
-  const std::vector<mp_integer> &args_value) const
+optionalt<exprt> string_concat_char_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
 {
-  PRECONDITION(args_value.size() == 1);
-  std::vector<mp_integer> result(input_value);
-  result.push_back(args_value[0]);
-  return result;
+  auto input_opt = eval_string(input, get_value);
+  if(!input_opt.has_value())
+    return {};
+  const mp_integer char_val = [&] {
+    if(const auto val = numeric_cast<mp_integer>(get_value(character)))
+      return *val;
+    INVARIANT(
+      get_value(character).id() == ID_unknown,
+      "character valuation should only contain constants and unknown");
+    return mp_integer(CHARACTER_FOR_UNKNOWN);
+  }();
+  input_opt.value().push_back(char_val);
+  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(

src/solvers/refinement/string_builtin_function.h

@@ -11,6 +11,8 @@
 
 class array_poolt;
 
+#define CHARACTER_FOR_UNKNOWN '?'
+
 /// Base class for string functions that are built in the solver
 class string_builtin_functiont
 {
@@ -68,7 +70,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
 public:
   array_string_exprt result;
   array_string_exprt input;
-  std::vector<exprt> args;
 
   /// Constructor from arguments of a function application.
   /// The arguments in `fun_args` should be in order:
@@ -88,15 +89,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   {
     return {input};
   }
-
-  /// Evaluate the result from a concrete valuation of the arguments
-  virtual std::vector<mp_integer> eval(
-    const std::vector<mp_integer> &input_value,
-    const std::vector<mp_integer> &args_value) const = 0;
-
-  optionalt<exprt>
-  eval(const std::function<exprt(const exprt &)> &get_value) const override;
-
   bool maybe_testing_function() const override
   {
     return false;
@@ -108,6 +100,8 @@ class string_concat_char_builtin_functiont
   : public string_transformation_builtin_functiont
 {
 public:
+  exprt character;
+
   /// Constructor from arguments of a function application.
   /// The arguments in `fun_args` should be in order:
   /// an integer `result.length`, a character pointer `&result[0]`,
@@ -118,11 +112,12 @@ class string_concat_char_builtin_functiont
     array_poolt &array_pool)
     : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
   {
+    PRECONDITION(fun_args.size() == 4);
+    character = fun_args[3];
   }
 
-  std::vector<mp_integer> eval(
-    const std::vector<mp_integer> &input_value,
-    const std::vector<mp_integer> &args_value) const override;
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
   std::string name() const override
   {
@@ -131,7 +126,7 @@ class string_concat_char_builtin_functiont
 
   exprt add_constraints(string_constraint_generatort &generator) const override
   {
-    return generator.add_axioms_for_concat_char(result, input, args[0]);
+    return generator.add_axioms_for_concat_char(result, input, character);
   }
 
   exprt length_constraint() const override

src/solvers/refinement/string_refinement.h

@@ -30,7 +30,6 @@ Author: Alberto Griggio, [email protected]
 #include <solvers/refinement/string_refinement_util.h>
 
 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
-#define CHARACTER_FOR_UNKNOWN '?'
 
 class string_refinementt final: public bv_refinementt
 {