Simplify when combining string-refinement result constraints

Due to the improvements in constant prop we increasingly have constraints
that are trivially simplified, like:

if 5 >= 2 do x else y

Also because of the way these conditions are combined - the resulting
merged if gets added to all subsequent conditions and values - we end up
with expressions like this:

if 5 >= 2 then (if 5 >= 2 do x ... else y ...) else (if 5 >= 2 do x ... else y ...)

Where the size of the expression increases exponentially to the
complexity of the original if statement even if the entire conditional
is trivial to prove right/wrong. This could likely be worked out by the
SAT solver happily enough but due to the size of the resulting
expressions (I've seen ones 1.34 billion nodes deep) it never gets there
within a reasonable time-frame.

Author: JohnDumbell

src/solvers/README.md

@@ -458,11 +458,11 @@ This is described in more detail \link string_builtin_functiont here. \endlink
     \copybrief add_axioms_for_concat
     \link add_axioms_for_concat More... \endlink
   * `cprover_string_delete` :
-    \copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
+    \link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) More... \endlink
   * `cprover_string_insert` :
-    \copybrief add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
+    \link add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) More... \endlink
   * `cprover_string_replace` :
     \copybrief add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
     \link add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
@@ -488,8 +488,8 @@ This is described in more detail \link string_builtin_functiont here. \endlink
     \copybrief add_axioms_for_format
     \link add_axioms_for_format More... \endlink
   * `cprover_string_from_literal` :
-    \copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
+    \link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) More... \endlink
   * `cprover_string_of_int` :
     \copybrief add_axioms_for_string_of_int
     \link add_axioms_for_string_of_int More... \endlink

src/solvers/strings/string_concatenation_builtin_function.cpp

@@ -182,11 +182,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat(
 /// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with two arguments: a string and a code point
 /// \param array_pool: pool of arrays representing strings
+/// \param ns: the namespace
 /// \return an expression
 std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool)
+  array_poolt &array_pool,
+  const namespacet &ns)
 {
   PRECONDITION(f.arguments().size() == 4);
   const array_string_exprt res =
@@ -198,7 +200,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
     array_pool.fresh_string(index_type, char_type);
   return combine_results(
     add_axioms_for_code_point(code_point, f.arguments()[3], array_pool),
-    add_axioms_for_concat(fresh_symbol, res, s1, code_point, array_pool));
+    add_axioms_for_concat(fresh_symbol, res, s1, code_point, array_pool),
+    ns);
 }
 
 std::vector<mp_integer> string_concatenation_builtin_functiont::eval(

src/solvers/strings/string_constraint_generator.h

@@ -187,7 +187,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_copy(
 std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_constant(
   const array_string_exprt &res,
   irep_idt sval,
@@ -200,20 +201,24 @@ std::pair<exprt, string_constraintst> add_axioms_for_delete(
   const array_string_exprt &str,
   const exprt &start,
   const exprt &end,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_delete(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &expr,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 
 std::pair<exprt, string_constraintst> add_axioms_for_insert(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -222,11 +227,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
 std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_insert_float(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -243,11 +250,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
   const array_string_exprt &res,
   const exprt &arg,
   const exprt &guard,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_from_literal(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool);
+  array_poolt &array_pool,
+  const namespacet &ns);
 
 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
   const array_string_exprt &res,
@@ -490,5 +499,6 @@ exprt zero_if_negative(const exprt &expr);
 
 std::pair<exprt, string_constraintst> combine_results(
   std::pair<exprt, string_constraintst> result1,
-  std::pair<exprt, string_constraintst> result2);
+  std::pair<exprt, string_constraintst> result2,
+  const namespacet &ns);
 #endif

src/solvers/strings/string_constraint_generator_constants.cpp

@@ -78,6 +78,7 @@ add_axioms_for_empty_string(const function_application_exprt &f)
 /// \param arg: expression of type string typet
 /// \param guard: condition under which `res` should be equal to arg
 /// \param array_pool: pool of arrays representing strings
+/// \param ns: the namespace
 /// \return 0 if constraints were added, 1 if expression could not be handled
 ///   and no constraint was added. Expression we can handle are of the form
 ///   \f$ e := "<string constant>" | (expr)? e : e \f$
@@ -86,17 +87,19 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
   const array_string_exprt &res,
   const exprt &arg,
   const exprt &guard,
-  array_poolt &array_pool)
+  array_poolt &array_pool,
+  const namespacet &ns)
 {
   if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
   {
     const and_exprt guard_true(guard, if_expr->cond());
     const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
     return combine_results(
       add_axioms_for_cprover_string(
-        fresh_symbol, res, if_expr->true_case(), guard_true, array_pool),
+        fresh_symbol, res, if_expr->true_case(), guard_true, array_pool, ns),
       add_axioms_for_cprover_string(
-        fresh_symbol, res, if_expr->false_case(), guard_false, array_pool));
+        fresh_symbol, res, if_expr->false_case(), guard_false, array_pool, ns),
+      ns);
   }
   else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
     return add_axioms_for_constant(
@@ -114,15 +117,17 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
 /// \param f: function application with an argument which is a string literal
 ///   that is a constant with a string value.
 /// \param array_pool: pool of arrays representing strings
+/// \param ns: the namespace
 /// \return string expression
 std::pair<exprt, string_constraintst> add_axioms_from_literal(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool)
+  array_poolt &array_pool,
+  const namespacet &ns)
 {
   const function_application_exprt::argumentst &args = f.arguments();
   PRECONDITION(args.size() == 3); // Bad args to string literal?
   const array_string_exprt res = array_pool.find(args[1], args[0]);
   return add_axioms_for_cprover_string(
-    fresh_symbol, res, args[2], true_exprt(), array_pool);
+    fresh_symbol, res, args[2], true_exprt(), array_pool, ns);
 }

src/solvers/strings/string_constraint_generator_insert.cpp

@@ -111,12 +111,14 @@ exprt length_constraint_for_insert(
 ///   pointer `&res[0]`, refined_string `s1`, refined_string`s2`, integer
 ///   `offset`, optional integer `start` and optional integer `end`
 /// \param array_pool: pool of arrays representing strings
+/// \param ns: the namespace
 /// \return an integer expression which is different from zero if there is an
 ///   exception to signal
 std::pair<exprt, string_constraintst> add_axioms_for_insert(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool)
+  array_poolt &array_pool,
+  const namespacet &ns)
 {
   PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
   array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
@@ -135,7 +137,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
       add_axioms_for_substring(
         fresh_symbol, substring, s2, start, end, array_pool),
       add_axioms_for_insert(
-        fresh_symbol, res, s1, substring, offset, array_pool));
+        fresh_symbol, res, s1, substring, offset, array_pool),
+      ns);
   }
   else // 5 arguments
   {
@@ -168,7 +171,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
     add_axioms_for_string_of_int(s2, f.arguments()[4], 0, ns, array_pool),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool),
+    ns);
 }
 
 /// add axioms corresponding to the StringBuilder.insert(Z) java function
@@ -177,12 +181,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
 /// \param f: function application with three arguments: a string, an
 ///   integer offset, and a Boolean
 /// \param array_pool: pool of arrays representing strings
+/// \param ns: the namespace
 /// \return a new string expression
 DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
 std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool)
+  array_poolt &array_pool,
+  const namespacet &ns)
 {
   PRECONDITION(f.arguments().size() == 5);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[0]);
@@ -194,7 +200,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
     add_axioms_from_bool(s2, f.arguments()[4], array_pool),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool),
+    ns);
 }
 
 /// Add axioms corresponding to the StringBuilder.insert(C) java function
@@ -203,11 +210,13 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
 /// \param f: function application with three arguments: a string, an
 ///   integer offset, and a character
 /// \param array_pool: pool of arrays representing strings
+/// \param ns: the namespace
 /// \return an expression
 std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
-  array_poolt &array_pool)
+  array_poolt &array_pool,
+  const namespacet &ns)
 {
   PRECONDITION(f.arguments().size() == 5);
   const array_string_exprt res =
@@ -219,7 +228,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
     add_axioms_from_char(s2, f.arguments()[4], array_pool),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool),
+    ns);
 }
 
 /// add axioms corresponding to the StringBuilder.insert(D) java function
@@ -248,7 +258,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
   return combine_results(
     add_axioms_for_string_of_float(
       fresh_symbol, s2, f.arguments()[4], array_pool, ns),
-    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
+    add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool),
+    ns);
 }
 
 /// Add axioms corresponding to the StringBuilder.insert(F) java function

src/solvers/strings/string_constraint_generator_main.cpp

@@ -260,19 +260,19 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id == ID_cprover_string_compare_to_func)
     return add_axioms_for_compare_to(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_literal_func)
-    return add_axioms_from_literal(fresh_symbol, expr, array_pool);
+    return add_axioms_from_literal(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_concat_code_point_func)
-    return add_axioms_for_concat_code_point(fresh_symbol, expr, array_pool);
+    return add_axioms_for_concat_code_point(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_insert_func)
-    return add_axioms_for_insert(fresh_symbol, expr, array_pool);
+    return add_axioms_for_insert(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_insert_int_func)
     return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_insert_long_func)
     return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_insert_bool_func)
-    return add_axioms_for_insert_bool(fresh_symbol, expr, array_pool);
+    return add_axioms_for_insert_bool(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_insert_char_func)
-    return add_axioms_for_insert_char(fresh_symbol, expr, array_pool);
+    return add_axioms_for_insert_char(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_insert_double_func)
     return add_axioms_for_insert_double(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_insert_float_func)
@@ -303,9 +303,9 @@ string_constraint_generatort::add_axioms_for_function_application(
   else if(id == ID_cprover_string_set_length_func)
     return add_axioms_for_set_length(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_delete_func)
-    return add_axioms_for_delete(fresh_symbol, expr, array_pool);
+    return add_axioms_for_delete(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_delete_char_at_func)
-    return add_axioms_for_delete_char_at(fresh_symbol, expr, array_pool);
+    return add_axioms_for_delete_char_at(fresh_symbol, expr, array_pool, ns);
   else if(id == ID_cprover_string_replace_func)
     return add_axioms_for_replace(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_constrain_characters_func)
@@ -441,9 +441,12 @@ exprt zero_if_negative(const exprt &expr)
 /// the return codes and merging the constraints.
 std::pair<exprt, string_constraintst> combine_results(
   std::pair<exprt, string_constraintst> result1,
-  std::pair<exprt, string_constraintst> result2)
+  std::pair<exprt, string_constraintst> result2,
+  const namespacet &ns)
 {
-  const exprt return_code = maximum(result1.first, result2.first);
+  exprt return_code = maximum(result1.first, result2.first);
   merge(result2.second, std::move(result1.second));
+  simplify(return_code, ns);
+
   return {return_code, std::move(result2.second)};
 }