Only add constraints on test function dependencies

romainbrenguier · romainbrenguier · commit b2ca93723b89 · 2018-03-19T17:01:30.000Z
Instead of adding all constraints corresponding to a string function
call, we look at which strings may be used in a testing function (such
as endsWith, equals, compare, etc...). We only add constraints for these
function calls, since the other operation can not matter for the
satisfiability problem.
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
@@ -17,6 +17,7 @@
 #include <util/graph.h>
 #include <util/magic.h>
 #include <util/make_unique.h>
+#include <unordered_set>
 #include "string_refinement_util.h"
 
 bool is_char_type(const typet &type)
@@ -397,10 +398,26 @@ void string_dependenciest::output_dot(std::ostream &stream) const
 void string_dependenciest::add_constraints(
   string_constraint_generatort &generator)
 {
+  std::unordered_set<nodet, node_hash> test_dependencies;
   for(const auto &builtin : builtin_function_nodes)
   {
     if(builtin.data->maybe_testing_function())
+      test_dependencies.insert(nodet(builtin));
+  }
+
+  get_reachable(
+    test_dependencies,
+    [&](
+      const nodet &n,
+      const std::function<void(const nodet &)> &f) { // NOLINT
+      for_each_successor(n, f);
+    });
+
+  for(const auto &node : test_dependencies)
+  {
+    if(node.kind == node.BUILTIN)
     {
+      const auto &builtin = builtin_function_nodes[node.index];
       const exprt return_value = builtin.data->add_constraints(generator);
       generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
     }
