extract substitute_symbols(...) into separate file

1) The substitute_symbols_rec(...) function in std_expr.cpp is extracted
into a separate file and is made available to external users as
substitute_symbols(...).

2) substitute_symbols is now aware of array_comprehension expressions.

Author: kroening

src/util/Makefile

@@ -93,6 +93,7 @@ SRC = arith_tools.cpp \
       string_hash.cpp \
       string_utils.cpp \
       structured_data.cpp \
+      substitute_symbols.cpp \
       symbol.cpp \
       symbol_table_base.cpp \
       symbol_table.cpp \

src/util/std_expr.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include "namespace.h"
 #include "pointer_expr.h"
 #include "range.h"
+#include "substitute_symbols.h"
 
 #include <map>
 
@@ -165,100 +166,6 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
   }
 }
 
-static optionalt<exprt> substitute_symbols_rec(
-  const std::map<irep_idt, exprt> &substitutions,
-  exprt src)
-{
-  if(src.id() == ID_symbol)
-  {
-    auto s_it = substitutions.find(to_symbol_expr(src).get_identifier());
-    if(s_it == substitutions.end())
-      return {};
-    else
-      return s_it->second;
-  }
-  else if(
-    src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
-  {
-    const auto &binding_expr = to_binding_expr(src);
-
-    // bindings may be nested,
-    // which may hide some of our substitutions
-    auto new_substitutions = substitutions;
-    for(const auto &variable : binding_expr.variables())
-      new_substitutions.erase(variable.get_identifier());
-
-    auto op_result =
-      substitute_symbols_rec(new_substitutions, binding_expr.where());
-    if(op_result.has_value())
-      return binding_exprt(
-        src.id(),
-        binding_expr.variables(),
-        op_result.value(),
-        binding_expr.type());
-    else
-      return {};
-  }
-  else if(src.id() == ID_let)
-  {
-    auto new_let_expr = to_let_expr(src); // copy
-    const auto &binding_expr = to_let_expr(src).binding();
-
-    // bindings may be nested,
-    // which may hide some of our substitutions
-    auto new_substitutions = substitutions;
-    for(const auto &variable : binding_expr.variables())
-      new_substitutions.erase(variable.get_identifier());
-
-    bool op_changed = false;
-
-    for(auto &op : new_let_expr.values())
-    {
-      auto op_result = substitute_symbols_rec(new_substitutions, op);
-
-      if(op_result.has_value())
-      {
-        op = op_result.value();
-        op_changed = true;
-      }
-    }
-
-    auto op_result =
-      substitute_symbols_rec(new_substitutions, binding_expr.where());
-    if(op_result.has_value())
-    {
-      new_let_expr.where() = op_result.value();
-      op_changed = true;
-    }
-
-    if(op_changed)
-      return std::move(new_let_expr);
-    else
-      return {};
-  }
-
-  if(!src.has_operands())
-    return {};
-
-  bool op_changed = false;
-
-  for(auto &op : src.operands())
-  {
-    auto op_result = substitute_symbols_rec(substitutions, op);
-
-    if(op_result.has_value())
-    {
-      op = op_result.value();
-      op_changed = true;
-    }
-  }
-
-  if(op_changed)
-    return src;
-  else
-    return {};
-}
-
 exprt binding_exprt::instantiate(const operandst &values) const
 {
   // number of values must match the number of bound variables
@@ -281,7 +188,7 @@ exprt binding_exprt::instantiate(const operandst &values) const
     substitutions[variables[i].get_identifier()] = values[i];
 
   // now recurse downwards and substitute in 'where'
-  auto substitute_result = substitute_symbols_rec(substitutions, where());
+  auto substitute_result = substitute_symbols(substitutions, where());
 
   if(substitute_result.has_value())
     return substitute_result.value();

src/util/std_expr.h

@@ -3090,7 +3090,8 @@ 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_array_comprehension || expr.id() == ID_forall ||
+    expr.id() == ID_exists || expr.id() == ID_lambda);
   const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
   validate_expr(ret);
   return ret;

src/util/substitute_symbols.cpp

@@ -0,0 +1,115 @@
+/*******************************************************************\
+
+Module: Symbol Substitution
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file util/substitute_symbols.cpp
+/// Symbol Substitution
+
+#include "substitute_symbols.h"
+
+#include "std_expr.h"
+
+static optionalt<exprt> substitute_symbols_rec(
+  const std::map<irep_idt, exprt> &substitutions,
+  exprt src)
+{
+  if(src.id() == ID_symbol)
+  {
+    auto s_it = substitutions.find(to_symbol_expr(src).get_identifier());
+    if(s_it == substitutions.end())
+      return {};
+    else
+      return s_it->second;
+  }
+  else if(
+    src.id() == ID_array_comprehension || src.id() == ID_forall ||
+    src.id() == ID_exists || src.id() == ID_lambda)
+  {
+    const auto &binding_expr = to_binding_expr(src);
+
+    // bindings may be nested,
+    // which may hide some of our substitutions
+    auto new_substitutions = substitutions;
+    for(const auto &variable : binding_expr.variables())
+      new_substitutions.erase(variable.get_identifier());
+
+    auto op_result =
+      substitute_symbols_rec(new_substitutions, binding_expr.where());
+    if(op_result.has_value())
+    {
+      auto new_binding_expr = binding_expr; // copy
+      new_binding_expr.where() = std::move(op_result.value());
+      return std::move(new_binding_expr);
+    }
+    else
+      return {};
+  }
+  else if(src.id() == ID_let)
+  {
+    auto new_let_expr = to_let_expr(src); // copy
+    const auto &binding_expr = to_let_expr(src).binding();
+
+    // bindings may be nested,
+    // which may hide some of our substitutions
+    auto new_substitutions = substitutions;
+    for(const auto &variable : binding_expr.variables())
+      new_substitutions.erase(variable.get_identifier());
+
+    bool op_changed = false;
+
+    for(auto &op : new_let_expr.values())
+    {
+      auto op_result = substitute_symbols_rec(new_substitutions, op);
+
+      if(op_result.has_value())
+      {
+        op = op_result.value();
+        op_changed = true;
+      }
+    }
+
+    auto op_result =
+      substitute_symbols_rec(new_substitutions, binding_expr.where());
+    if(op_result.has_value())
+    {
+      new_let_expr.where() = op_result.value();
+      op_changed = true;
+    }
+
+    if(op_changed)
+      return std::move(new_let_expr);
+    else
+      return {};
+  }
+
+  if(!src.has_operands())
+    return {};
+
+  bool op_changed = false;
+
+  for(auto &op : src.operands())
+  {
+    auto op_result = substitute_symbols_rec(substitutions, op);
+
+    if(op_result.has_value())
+    {
+      op = op_result.value();
+      op_changed = true;
+    }
+  }
+
+  if(op_changed)
+    return src;
+  else
+    return {};
+}
+
+optionalt<exprt>
+substitute_symbols(const std::map<irep_idt, exprt> &substitutions, exprt src)
+{
+  return substitute_symbols_rec(substitutions, src);
+}

src/util/substitute_symbols.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Symbol Substitution
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_SUBSTITUTE_SYMBOLS_H
+#define CPROVER_UTIL_SUBSTITUTE_SYMBOLS_H
+
+/// \file util/substitute_symbols.h
+/// Symbol Substitution
+
+#include "expr.h"
+
+#include <map>
+
+/// Substitute free occurrences of the variables given
+/// by their identifiers in the keys of the map in the
+/// given expression. Only symbol_exprt expressions are
+/// substituted.
+/// \returns expression after substitution,
+/// or {} when no substitution took place
+optionalt<exprt>
+substitute_symbols(const std::map<irep_idt, exprt> &substitutions, exprt);
+
+#endif // CPROVER_UTIL_SUBSTITUTE_SYMBOLS_H