Clear constraints at each call to dec_solve

constraint_generator is kept as a class member because it is used by
get, but we need to make sure it is cleared at each dec_solve call so
that we don't keep unecessary or redundant constraints.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -110,6 +110,9 @@ class string_constraint_generatort final
   const std::vector<string_not_contains_constraintt> &
   get_not_contains_constraints() const;
 
+  /// Clear all constraints and lemmas
+  void clear_constraints();
+
   /// Boolean symbols for the results of some string functions
   const std::vector<symbol_exprt> &get_boolean_symbols() const;
 

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -323,6 +323,13 @@ string_constraint_generatort::get_string_expr(const exprt &expr)
   return char_array_of_pointer(str.content(), str.length());
 }
 
+void string_constraint_generatort::clear_constraints()
+{
+  lemmas.clear();
+  constraints.clear();
+  not_contains_constraints.clear();
+}
+
 /// adds standard axioms about the length of the string and its content: * its
 /// length should be positive * it should not exceed max_string_length * if
 /// force_printable_characters is true then all characters should belong to the

src/solvers/refinement/string_refinement.cpp

@@ -639,6 +639,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       string_id_symbol_resolve.replace_expr(eq.rhs());
   }
 
+  // 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.clear_constraints();
   make_char_array_pointer_associations(generator, equations);
 
 #ifdef DEBUG
@@ -658,8 +661,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #endif
 
   debug() << "dec_solve: add constraints" << eom;
-  // Generator is also used by get, that's why we use a class member
-  dependencies.add_constraints(generator);
+ dependencies.add_constraints(generator);
 
 #ifdef DEBUG
   output_equations(debug(), equations, ns);