replace_symbolt now knows bindings

This makes replace_symbolt aware of bound symbols, which may hide the
symbols that are being replaced.

Author: kroening

src/util/replace_symbol.cpp

@@ -101,6 +101,41 @@ bool replace_symbolt::replace(exprt &dest) const
     if(!replace_symbol_expr(to_symbol_expr(dest)))
       return false;
   }
+  else if(dest.id() == ID_let)
+  {
+    auto &let_expr = to_let_expr(dest);
+
+    // first replace the assigned value expressions
+    for(auto &op : let_expr.values())
+      if(replace(op))
+        result = false;
+
+    // now set up the binding
+    auto old_bindings = bindings;
+    for(auto &variable : let_expr.variables())
+      bindings.insert(variable.get_identifier());
+
+    // now replace in the 'where' expression
+    if(!replace(let_expr.where()))
+      result = false;
+
+    bindings = std::move(old_bindings);
+  }
+  else if(
+    dest.id() == ID_array_comprehension || dest.id() == ID_exists ||
+    dest.id() == ID_forall || dest.id() == ID_lambda)
+  {
+    auto &binding_expr = to_binding_expr(dest);
+
+    auto old_bindings = bindings;
+    for(auto &binding : binding_expr.variables())
+      bindings.insert(binding.get_identifier());
+
+    if(!replace(binding_expr.where()))
+      result = false;
+
+    bindings = std::move(old_bindings);
+  }
   else
   {
     Forall_operands(it, dest)
@@ -136,7 +171,10 @@ bool replace_symbolt::have_to_replace(const exprt &dest) const
   if(dest.id()==ID_symbol)
   {
     const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
-    return replaces_symbol(identifier);
+    if(bindings.find(identifier) != bindings.end())
+      return false;
+    else
+      return replaces_symbol(identifier);
   }
 
   forall_operands(it, dest)

src/util/replace_symbol.h

@@ -17,10 +17,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr.h"
 
+#include <set>
 #include <unordered_map>
 
-/// Replace expression or type symbols by an expression or type, respectively.
-/// The resolved type of the symbol must match the type of the replacement.
+/// Replace a symbol expression by a given expression.
+/// The type of the symbol must match the type of the replacement.
+/// This class is aware of symbol hiding caused by bindings
+/// such as forall, exists, and the like.
 class replace_symbolt
 {
 public:
@@ -88,6 +91,7 @@ class replace_symbolt
 
 protected:
   expr_mapt expr_map;
+  mutable std::set<irep_idt> bindings;
 
   virtual bool replace_symbol_expr(symbol_exprt &dest) const;