Rewrite axioms for insert

This reduces the number of universal formulas added (from 6 to 3), and
avoid introducing new strings. Ideally the add_axioms_-function should
not introduce new strings, that would make it easier to refactor and add
new functionalities.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -14,8 +14,14 @@ Author: Romain Brenguier, [email protected]
 
 /// Add axioms ensuring the result `res` corresponds to `s1` where we
 /// inserted `s2` at position `offset`.
+/// We write offset' for `max(0, min(res.length, offset))`.
+/// These axioms are:
+/// 1. res.length = s1.length + s2.length
+/// 2. forall i < offset' . res[i] = s1[i]
+/// 3. forall i < s2.length. res[i + offset'] = s2[i]
+/// 4. forall i in [offset', s1.length). res[i + s2.length] = s1[i]
 /// This is equivalent to
-/// `res=concat(substring(s1, 0, offset), concat(s2, substring(s1, offset)))`.
+/// `res=concat(substring(s1, 0, offset'), concat(s2, substring(s1, offset')))`.
 /// \param res: array of characters expression
 /// \param s1: array of characters expression
 /// \param s2: array of characters expression
@@ -30,25 +36,37 @@ exprt string_constraint_generatort::add_axioms_for_insert(
 {
   PRECONDITION(offset.type()==s1.length().type());
   const typet &index_type = s1.length().type();
-  const typet &char_type = s1.content().type().subtype();
-  array_string_exprt pref = fresh_string(index_type, char_type);
-  exprt return_code1 =
-    add_axioms_for_substring(pref, s1, from_integer(0, offset.type()), offset);
-  array_string_exprt suf = fresh_string(index_type, char_type);
-  exprt return_code2 = add_axioms_for_substring(suf, s1, offset, s1.length());
-  array_string_exprt concat1 = fresh_string(index_type, char_type);
-  exprt return_code3 = add_axioms_for_concat(concat1, pref, s2);
-  exprt return_code4 = add_axioms_for_concat(res, concat1, suf);
-  return if_exprt(
-    equal_exprt(return_code1, from_integer(0, return_code1.type())),
-    if_exprt(
-      equal_exprt(return_code2, from_integer(0, return_code1.type())),
-      if_exprt(
-        equal_exprt(return_code3, from_integer(0, return_code1.type())),
-        return_code4,
-        return_code3),
-      return_code2),
-    return_code1);
+  const exprt offset1 =
+    maximum(from_integer(0, index_type), minimum(s1.length(), offset));
+
+  // Axiom 1.
+  lemmas.push_back(
+    equal_exprt(res.length(), plus_exprt(s1.length(), s2.length())));
+
+  // Axiom 2.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt i = fresh_symbol("QA_insert1", index_type);
+    return string_constraintt(i, offset1, equal_exprt(res[i], s1[i]));
+  }());
+
+  // Axiom 3.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt i = fresh_symbol("QA_insert2", index_type);
+    return string_constraintt(
+      i, s2.length(), equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
+  }());
+
+  // Axiom 4.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt i = fresh_symbol("QA_insert3", index_type);
+    return string_constraintt(
+      i,
+      offset1,
+      s1.length(),
+      equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
+  }());
+
+  return from_integer(0, get_return_code_type());
 }
 
 /// Insertion of a string in another at a specific index