Add and add_constraint method to builtin functions

This will be used to directly add constraints by traversing the string
dependency graph.

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.h

@@ -7,6 +7,7 @@
 #include <vector>
 #include <util/optional.h>
 #include <util/string_expr.h>
+#include "string_constraint_generator.h"
 
 class array_poolt;
 
@@ -32,6 +33,11 @@ class string_builtin_functiont
 
   virtual std::string name() const = 0;
 
+  /// Add constraints ensuring that the value of result expression of the
+  /// builtin function corresponds to the value of the function call.
+  virtual exprt
+  add_constraints(string_constraint_generatort &constraint_generator) const = 0;
+
 protected:
   string_builtin_functiont() = default;
 };
@@ -96,6 +102,11 @@ class string_concat_char_builtin_functiont
   {
     return "concat_char";
   }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_concat_char(result, input, args[0]);
+  };
 };
 
 /// String inserting a string into another one
@@ -141,6 +152,15 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
     return "insert";
   }
 
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    if(args.size() == 1)
+      return generator.add_axioms_for_insert(result, input1, input2, args[0]);
+    if(args.size() == 3)
+      UNIMPLEMENTED;
+    UNREACHABLE;
+  };
+
 protected:
   string_insertion_builtin_functiont() = default;
 };
@@ -168,6 +188,16 @@ class string_concatenation_builtin_functiont final
   {
     return "concat";
   }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    if(args.size() == 0)
+      return generator.add_axioms_for_concat(result, input1, input2);
+    if(args.size() == 2)
+      return generator.add_axioms_for_concat_substr(
+        result, input1, input2, args[0], args[1]);
+    UNREACHABLE;
+  };
 };
 
 /// String creation from other types
@@ -231,6 +261,11 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   {
     return {};
   }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_function_application(function_application);
+  };
 };
 
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H

src/solvers/refinement/string_constraint_generator.h

@@ -148,6 +148,26 @@ class string_constraint_generatort final
     return signedbv_typet(32);
   }
 
+  exprt add_axioms_for_concat_char(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const exprt &c);
+  exprt add_axioms_for_concat(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const array_string_exprt &s2);
+  exprt add_axioms_for_concat_substr(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const array_string_exprt &s2,
+    const exprt &start_index,
+    const exprt &end_index);
+  exprt add_axioms_for_insert(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const array_string_exprt &s2,
+    const exprt &offset);
+
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
   array_string_exprt
@@ -203,21 +223,7 @@ class string_constraint_generatort final
   exprt add_axioms_for_empty_string(const function_application_exprt &f);
   exprt add_axioms_for_char_set(const function_application_exprt &f);
   exprt add_axioms_for_copy(const function_application_exprt &f);
-  exprt add_axioms_for_concat(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const array_string_exprt &s2);
-  exprt add_axioms_for_concat_char(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const exprt &c);
   exprt add_axioms_for_concat_char(const function_application_exprt &f);
-  exprt add_axioms_for_concat_substr(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const array_string_exprt &s2,
-    const exprt &start_index,
-    const exprt &end_index);
   exprt add_axioms_for_concat(const function_application_exprt &f);
   exprt add_axioms_for_concat_code_point(const function_application_exprt &f);
   exprt add_axioms_for_constant(
@@ -244,11 +250,6 @@ class string_constraint_generatort final
     const typet &index_type,
     const typet &char_type);
 
-  exprt add_axioms_for_insert(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const array_string_exprt &s2,
-    const exprt &offset);
   exprt add_axioms_for_insert(const function_application_exprt &f);
   exprt add_axioms_for_insert_int(const function_application_exprt &f);
   exprt add_axioms_for_insert_bool(const function_application_exprt &f);