find_symbols: support restriction to non-bound symbols

Adds a new symbol kind to distinguish bound from unbound ones.

Author: tautschnig

src/util/find_symbols.cpp

@@ -43,20 +43,53 @@ bool has_symbol(
 static bool find_symbols(
   symbol_kindt,
   const typet &,
-  std::function<bool(const symbol_exprt &)>);
+  std::function<bool(const symbol_exprt &)>,
+  std::unordered_set<irep_idt> &bindings);
 
 static bool find_symbols(
   symbol_kindt kind,
   const exprt &src,
-  std::function<bool(const symbol_exprt &)> op)
+  std::function<bool(const symbol_exprt &)> op,
+  std::unordered_set<irep_idt> &bindings)
 {
+  if(kind == symbol_kindt::F_EXPR_NOT_BOUND)
+  {
+    if(src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
+    {
+      const auto &binding_expr = to_binding_expr(src);
+      std::unordered_set<irep_idt> new_bindings{bindings};
+      for(const auto &v : binding_expr.variables())
+        new_bindings.insert(v.get_identifier());
+
+      if(!find_symbols(kind, binding_expr.where(), op, new_bindings))
+        return false;
+
+      return find_symbols(kind, binding_expr.type(), op, bindings);
+    }
+    else if(src.id() == ID_let)
+    {
+      const auto &let_expr = to_let_expr(src);
+      std::unordered_set<irep_idt> new_bindings{bindings};
+      for(const auto &v : let_expr.variables())
+        new_bindings.insert(v.get_identifier());
+
+      if(!find_symbols(kind, let_expr.where(), op, new_bindings))
+        return false;
+
+      if(!find_symbols(kind, let_expr.op1(), op, new_bindings))
+        return false;
+
+      return find_symbols(kind, let_expr.type(), op, bindings);
+    }
+  }
+
   forall_operands(it, src)
   {
-    if(!find_symbols(kind, *it, op))
+    if(!find_symbols(kind, *it, op, bindings))
       return false;
   }
 
-  if(!find_symbols(kind, src.type(), op))
+  if(!find_symbols(kind, src.type(), op, bindings))
     return false;
 
   if(
@@ -83,7 +116,8 @@ static bool find_symbols(
 
   if(
     c_sizeof_type.is_not_nil() &&
-    !find_symbols(kind, static_cast<const typet &>(c_sizeof_type), op))
+    !find_symbols(
+      kind, static_cast<const typet &>(c_sizeof_type), op, bindings))
   {
     return false;
   }
@@ -92,7 +126,7 @@ static bool find_symbols(
 
   if(
     va_arg_type.is_not_nil() &&
-    !find_symbols(kind, static_cast<const typet &>(va_arg_type), op))
+    !find_symbols(kind, static_cast<const typet &>(va_arg_type), op, bindings))
   {
     return false;
   }
@@ -103,20 +137,21 @@ static bool find_symbols(
 static bool find_symbols(
   symbol_kindt kind,
   const typet &src,
-  std::function<bool(const symbol_exprt &)> op)
+  std::function<bool(const symbol_exprt &)> op,
+  std::unordered_set<irep_idt> &bindings)
 {
   if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
   {
     if(
       src.has_subtype() &&
-      !find_symbols(kind, to_type_with_subtype(src).subtype(), op))
+      !find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings))
     {
       return false;
     }
 
     for(const typet &subtype : to_type_with_subtypes(src).subtypes())
     {
-      if(!find_symbols(kind, subtype, op))
+      if(!find_symbols(kind, subtype, op, bindings))
         return false;
     }
 
@@ -137,26 +172,26 @@ static bool find_symbols(
 
     for(const auto &c : struct_union_type.components())
     {
-      if(!find_symbols(kind, c, op))
+      if(!find_symbols(kind, c, op, bindings))
         return false;
     }
   }
   else if(src.id()==ID_code)
   {
     const code_typet &code_type=to_code_type(src);
-    if(!find_symbols(kind, code_type.return_type(), op))
+    if(!find_symbols(kind, code_type.return_type(), op, bindings))
       return false;
 
     for(const auto &p : code_type.parameters())
     {
-      if(!find_symbols(kind, p, op))
+      if(!find_symbols(kind, p, op, bindings))
         return false;
     }
   }
   else if(src.id()==ID_array)
   {
     // do the size -- the subtype is already done
-    if(!find_symbols(kind, to_array_type(src).size(), op))
+    if(!find_symbols(kind, to_array_type(src).size(), op, bindings))
       return false;
   }
   else if(
@@ -183,6 +218,24 @@ static bool find_symbols(
   return true;
 }
 
+static bool find_symbols(
+  symbol_kindt kind,
+  const typet &type,
+  std::function<bool(const symbol_exprt &)> op)
+{
+  std::unordered_set<irep_idt> bindings;
+  return find_symbols(kind, type, op, bindings);
+}
+
+static bool find_symbols(
+  symbol_kindt kind,
+  const exprt &src,
+  std::function<bool(const symbol_exprt &)> op)
+{
+  std::unordered_set<irep_idt> bindings;
+  return find_symbols(kind, src, op, bindings);
+}
+
 void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
 {
   find_symbols(

src/util/find_symbols.h

@@ -37,6 +37,8 @@ enum class symbol_kindt
   F_EXPR_NEXT,
   /// Current or next-state symbol expressions.
   F_EXPR_BOTH,
+  /// Symbol expressions, but excluding bindings.
+  F_EXPR_NOT_BOUND,
   /// All of the above.
   F_ALL
 };