Extend global has_subexpr to take a predicate as has_subtype does

Author: tautschnig

src/solvers/refinement/string_refinement_util.cpp

@@ -53,11 +53,8 @@ bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
 
 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
 {
-  const auto it = std::find_if(
-    expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT
-      return is_char_array_type(e.type(), ns);
-    });
-  return it != expr.depth_end();
+  return has_subexpr(
+    expr, [&](const exprt &e) { return is_char_array_type(e.type(), ns); });
 }
 
 sparse_arrayt::sparse_arrayt(const with_exprt &expr)

src/util/expr_util.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "expr_util.h"
 
 #include "expr.h"
+#include "expr_iterator.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "std_expr.h"
@@ -120,16 +121,19 @@ exprt boolean_negate(const exprt &src)
     return not_exprt(src);
 }
 
-bool has_subexpr(const exprt &src, const irep_idt &id)
+bool has_subexpr(
+  const exprt &expr,
+  const std::function<bool(const exprt &)> &pred)
 {
-  if(src.id()==id)
-    return true;
+  const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
+  return it != expr.depth_end();
 
-  forall_operands(it, src)
-    if(has_subexpr(*it, id))
-      return true;
+}
 
-  return false;
+bool has_subexpr(const exprt &src, const irep_idt &id)
+{
+  return has_subexpr(
+    src, [&](const exprt &subexpr) { return subexpr.id() == id; });
 }
 
 bool has_subtype(

src/util/expr_util.h

@@ -43,6 +43,9 @@ exprt is_not_zero(const exprt &, const namespacet &ns);
 /// and swapping false and true
 exprt boolean_negate(const exprt &);
 
+/// returns true if the expression has a subexpression that satisfies pred
+bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
+
 /// returns true if the expression has a subexpression with given ID
 bool has_subexpr(const exprt &, const irep_idt &);