replace_symbolt with bindings

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;
 

src/util/std_expr.h

@@ -3090,12 +3090,29 @@ inline void validate_expr(const binding_exprt &binding_expr)
 inline const binding_exprt &to_binding_expr(const exprt &expr)
 {
   PRECONDITION(
-    expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda);
+    expr.id() == ID_forall || expr.id() == ID_exists ||
+    expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
   const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
   validate_expr(ret);
   return ret;
 }
 
+/// \brief Cast an exprt to a \ref binding_exprt
+///
+/// \a expr must be known to be \ref binding_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref binding_exprt
+inline binding_exprt &to_binding_expr(exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_forall || expr.id() == ID_exists ||
+    expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
+  binding_exprt &ret = static_cast<binding_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 /// \brief A let expression
 class let_exprt : public binary_exprt
 {