Get rid of constraints field of constraint generator

The constraints should be a return value of the generator methods
rather than a field.

Author: romainbrenguier

src/solvers/strings/string_constraint_generator.h

@@ -60,20 +60,24 @@ class string_constraint_generatort final
 
   array_poolt array_pool;
 
-  string_constraintst constraints;
-
   const namespacet ns;
 
   /// Associate array to pointer, and array to length
   /// \return an expression if the given function application is one of
   ///   associate pointer and associate length
   optionalt<exprt>
-  make_array_pointer_association(const function_application_exprt &expr);
+  make_array_pointer_association(
+    const exprt &return_code,
+    const function_application_exprt &expr);
 
 private:
-  exprt associate_array_to_pointer(const function_application_exprt &f);
+  exprt associate_array_to_pointer(
+    const exprt &return_code,
+    const function_application_exprt &f);
 
-  exprt associate_length_to_array(const function_application_exprt &f);
+  exprt associate_length_to_array(
+    const exprt &return_code,
+    const function_application_exprt &f);
 };
 
 // Type used by primitives to signal errors

src/solvers/strings/string_constraint_generator_main.cpp

@@ -58,6 +58,7 @@ exprt sum_overflows(const plus_exprt &sum)
 /// \param f: a function application with argument a character array `arr` and
 ///   a character pointer `ptr`.
 exprt string_constraint_generatort::associate_array_to_pointer(
+  const exprt &return_code,
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 2);
@@ -76,19 +77,22 @@ exprt string_constraint_generatort::associate_array_to_pointer(
 
 /// Associate an integer length to a char array.
 /// This adds an axiom ensuring that `arr.length` and `length` are equal.
+/// \param return code: expression which is assigned the result of the function
 /// \param f: a function application with argument a character array `arr` and
 ///   an integer `length`.
-/// \return integer expression equal to 0
+/// \return a constraint
 exprt string_constraint_generatort::associate_length_to_array(
+  const exprt &return_code,
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 2);
   array_string_exprt array_expr = to_array_string_expr(f.arguments()[0]);
   const exprt &new_length = f.arguments()[1];
 
   const auto &length = array_pool.get_or_create_length(array_expr);
-  constraints.existential.push_back(equal_exprt(length, new_length));
-  return from_integer(0, f.type());
+  return and_exprt{
+  equal_exprt{return_code, from_integer(0, f.type())},
+      equal_exprt(length, new_length)};
 }
 
 void string_constraintst::clear()
@@ -200,13 +204,14 @@ static irep_idt get_function_name(const function_application_exprt &expr)
 }
 
 optionalt<exprt> string_constraint_generatort::make_array_pointer_association(
+  const exprt &return_code,
   const function_application_exprt &expr)
 {
   const irep_idt &id = get_function_name(expr);
   if(id == ID_cprover_associate_array_to_pointer_func)
-    return associate_array_to_pointer(expr);
+    return associate_array_to_pointer(return_code, expr);
   else if(id == ID_cprover_associate_length_to_array_func)
-    return associate_length_to_array(expr);
+    return associate_length_to_array(return_code, expr);
   return {};
 }
 

src/solvers/strings/string_dependencies.cpp

@@ -328,7 +328,7 @@ void string_dependenciest::output_dot(std::ostream &stream) const
   stream << '}' << std::endl;
 }
 
-void string_dependenciest::add_constraints(
+string_constraintst string_dependenciest::add_constraints(
   string_constraint_generatort &generator)
 {
   std::unordered_set<nodet, node_hash> test_dependencies;
@@ -346,16 +346,16 @@ void string_dependenciest::add_constraints(
       for_each_successor(n, f);
     });
 
+  string_constraintst constraints;
   for(const auto &node : builtin_function_nodes)
   {
     if(test_dependencies.count(nodet(node)))
     {
       const auto &builtin = builtin_function_nodes[node.index];
-      string_constraintst constraints = builtin.data->constraints(generator);
-      merge(generator.constraints, std::move(constraints));
+      merge(constraints, builtin.data->constraints(generator));
     }
     else
-      generator.constraints.existential.push_back(
-        node.data->length_constraint());
+      constraints.existential.push_back(node.data->length_constraint());
   }
+  return constraints;
 }

src/solvers/strings/string_dependencies.h

@@ -14,6 +14,8 @@ Author: Diffblue Ltd.
 
 #include <memory>
 
+#include <util/nodiscard.h>
+
 #include "string_builtin_function.h"
 
 /// Keep track of dependencies between strings.
@@ -114,7 +116,8 @@ class string_dependenciest
   /// For all builtin call on which a test (or an unsupported buitin)
   /// result depends, add the corresponding constraints. For the other builtin
   /// only add constraints on the length.
-  void add_constraints(string_constraint_generatort &generatort);
+  NODISCARD string_constraintst add_constraints(
+    string_constraint_generatort &generatort);
 
   /// Clear the content of the dependency graph
   void clear();

src/solvers/strings/string_refinement.cpp

@@ -251,8 +251,10 @@ static void make_char_array_pointer_associations(
       const auto fun_app =
         expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
     {
-      if(const auto result = generator.make_array_pointer_association(*fun_app))
-        eq.rhs() = *result;
+      const auto new_equation =
+        generator.make_array_pointer_association(eq.lhs(), *fun_app);
+      if(new_equation)
+        eq = equal_exprt{true_exprt{}, *new_equation};
     }
   }
 }
@@ -645,9 +647,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     }
   }
 
-  // Generator is also used by get, so we have to use it as a class member
-  // but we make sure it is cleared at each `dec_solve` call.
-  generator.constraints.clear();
+  // Constraints start clear at each `dec_solve` call.
+  string_constraintst constraints;
   make_char_array_pointer_associations(generator, equations);
 
 #ifdef DEBUG
@@ -677,7 +678,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #endif
 
   log.debug() << "dec_solve: add constraints" << messaget::eom;
-  dependencies.add_constraints(generator);
+  merge(constraints, dependencies.add_constraints(generator));
 
 #ifdef DEBUG
   output_equations(log.debug(), equations);
@@ -702,8 +703,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   }
 
   std::transform(
-    generator.constraints.universal.begin(),
-    generator.constraints.universal.end(),
+    constraints.universal.begin(),
+    constraints.universal.end(),
     std::back_inserter(axioms.universal),
     [&](string_constraintt constraint) {
       constraint.replace_expr(symbol_resolve);
@@ -715,8 +716,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     });
 
   std::transform(
-    generator.constraints.not_contains.begin(),
-    generator.constraints.not_contains.end(),
+    constraints.not_contains.begin(),
+    constraints.not_contains.end(),
     std::back_inserter(axioms.not_contains),
     [&](string_not_contains_constraintt axiom) {
       replace(symbol_resolve, axiom);
@@ -737,7 +738,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       nc_axiom, generator.fresh_symbol("not_contains_witness", witness_type));
   }
 
-  for(const exprt &lemma : generator.constraints.existential)
+  for(const exprt &lemma : constraints.existential)
   {
     add_lemma(substitute_array_access(lemma, generator.fresh_symbol, true));
   }