Add constraints from the string dependencies

We add constraints directly from the constructed graph instead of going
through all the equations.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -105,6 +105,7 @@ class string_constraint_generatort final
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
   const std::vector<exprt> &get_lemmas() const;
+  void add_lemma(const exprt &);
   const std::vector<string_constraintt> &get_constraints() const;
   const std::vector<string_not_contains_constraintt> &
   get_not_contains_constraints() const;

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -39,6 +39,11 @@ const std::vector<exprt> &string_constraint_generatort::get_lemmas() const
   return lemmas;
 }
 
+void string_constraint_generatort::add_lemma(const exprt &expr)
+{
+  lemmas.push_back(expr);
+}
+
 const std::vector<string_constraintt> &
 string_constraint_generatort::get_constraints() const
 {

src/solvers/refinement/string_refinement.cpp

@@ -251,41 +251,6 @@ static std::vector<exprt> generate_instantiations(
   return lemmas;
 }
 
-/// Remove functions applications and create the necessary axioms.
-/// \param expr: an expression possibly containing function applications
-/// \param generator: generator for the string constraints
-/// \return an expression containing no function application
-static void substitute_function_applications(
-  exprt &expr,
-  string_constraint_generatort &generator)
-{
-  for(auto it = expr.depth_begin(), itend = expr.depth_end();
-      it != itend;) // No ++it
-  {
-    if(it->id() == ID_function_application)
-    {
-      it.mutate() =
-        generator.add_axioms_for_function_application(
-          to_function_application_expr(expr));
-      it.next_sibling_or_parent();
-    }
-    else
-      ++it;
-  }
-}
-
-/// Remove functions applications and create the necessary axioms.
-/// \param equations: vector of equations
-/// \param generator: generator for the string constraints
-/// \return vector of equations where function application have been replaced
-static void substitute_function_applications_in_equations(
-  std::vector<equal_exprt> &equations,
-  string_constraint_generatort &generator)
-{
-  for(auto &eq : equations)
-    substitute_function_applications(eq.rhs(), generator);
-}
-
 /// Fill the array_pointer correspondence and replace the right hand sides of
 /// the corresponding equations
 static void make_char_array_pointer_associations(
@@ -680,17 +645,22 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   output_equations(debug(), equations, ns);
 #endif
 
-  debug() << "dec_solve: compute dependency graph:" << eom;
-  for(const equal_exprt &eq : equations)
-    add_node(dependencies, eq, generator.array_pool);
+  debug() << "dec_solve: compute dependency graph and remove function "
+          << "applications captured by the dependencies:" << eom;
+  const auto new_equation_end = std::remove_if(
+    equations.begin(), equations.end(), [&](const equal_exprt &eq) { // NOLINT
+      return add_node(dependencies, eq, generator.array_pool);
+    });
+  equations.erase(new_equation_end, equations.end());
 
 #ifdef DEBUG
   dependencies.output_dot(debug());
 #endif
 
-  debug() << "dec_solve: Replace function applications" << eom;
+  debug() << "dec_solve: add constraints" << eom;
   // Generator is also used by get, that's why we use a class member
-  substitute_function_applications_in_equations(equations, generator);
+  dependencies.add_constraints(generator);
+
 #ifdef DEBUG
   output_equations(debug(), equations, ns);
 #endif

src/solvers/refinement/string_refinement_util.cpp

@@ -419,5 +419,8 @@ void string_dependenciest::add_constraints(
   string_constraint_generatort &generator)
 {
   for(const auto &builtin : builtin_function_nodes)
-    builtin->add_constraints(generator);
+  {
+    const exprt return_value = builtin->add_constraints(generator);
+    generator.add_lemma(equal_exprt(return_value, builtin->return_code));
+  }
 }