Introduce binding_exprt::instantiate

src/solvers/flattening/boolbv_quantifier.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/optional.h>
 #include <util/range.h>
 #include <util/replace_expr.h>
-#include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
 
 /// A method to detect equivalence between experts that can contain typecast
@@ -212,17 +211,11 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
   auto fresh_symbols = fresh_binding(src);
 
   // replace in where()
-  replace_symbolt replace_symbol;
-
-  for(const auto &pair : make_range(src.variables()).zip(fresh_symbols))
-    replace_symbol.insert(pair.first, pair.second);
-
-  exprt renamed_where = src.where();
-  replace_symbol(renamed_where);
+  auto where_replaced = src.instantiate(fresh_symbols);
 
   // produce new quantifier expression
   auto new_src =
-    quantifier_exprt(src.id(), std::move(fresh_symbols), renamed_where);
+    quantifier_exprt(src.id(), std::move(fresh_symbols), where_replaced);
 
   const auto res = instantiate_quantifier(src, ns);
 

src/util/mathematical_expr.cpp

@@ -51,68 +51,3 @@ lambda_exprt::lambda_exprt(const variablest &_variables, const exprt &_where)
       lambda_type(_variables, _where))
 {
 }
-
-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;
-  }
-
-  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 lambda_exprt::application(const operandst &arguments) const
-{
-  // number of arguments must match function signature
-  auto &variables = this->variables();
-  PRECONDITION(variables.size() == arguments.size());
-
-  std::map<symbol_exprt, exprt> value_map;
-
-  for(std::size_t i = 0; i < variables.size(); i++)
-  {
-    // types must match
-    PRECONDITION(variables[i].type() == arguments[i].type());
-    value_map[variables[i]] = arguments[i];
-  }
-
-  // build a subsitution map
-  std::map<irep_idt, exprt> substitutions;
-
-  for(std::size_t i = 0; i < variables.size(); i++)
-    substitutions[variables[i].get_identifier()] = arguments[i];
-
-  // now recurse downwards and substitute in 'where'
-  auto substitute_result = substitute_symbols_rec(substitutions, where());
-
-  if(substitute_result.has_value())
-    return substitute_result.value();
-  else
-    return where(); // trivial case, variables not used
-}

src/util/mathematical_expr.h

@@ -398,7 +398,10 @@ class lambda_exprt : public binding_exprt
   }
 
   // apply the function to the given arguments
-  exprt application(const operandst &) const;
+  exprt application(const operandst &arguments) const
+  {
+    return instantiate(arguments);
+  }
 };
 
 template <>

src/util/std_expr.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 #include "namespace.h"
 #include "range.h"
 
+#include <map>
+
 bool constant_exprt::value_is_zero_string() const
 {
   const std::string val=id2string(get_value());
@@ -134,3 +136,136 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
       "let bindings must be type consistent");
   }
 }
+
+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
+  auto &variables = this->variables();
+  PRECONDITION(variables.size() == values.size());
+
+  std::map<symbol_exprt, exprt> value_map;
+
+  for(std::size_t i = 0; i < variables.size(); i++)
+  {
+    // types must match
+    PRECONDITION(variables[i].type() == values[i].type());
+    value_map[variables[i]] = values[i];
+  }
+
+  // build a substitution map
+  std::map<irep_idt, exprt> substitutions;
+
+  for(std::size_t i = 0; i < variables.size(); i++)
+    substitutions[variables[i].get_identifier()] = values[i];
+
+  // now recurse downwards and substitute in 'where'
+  auto substitute_result = substitute_symbols_rec(substitutions, where());
+
+  if(substitute_result.has_value())
+    return substitute_result.value();
+  else
+    return where(); // trivial case, variables not used
+}
+
+exprt binding_exprt::instantiate(const variablest &new_variables) const
+{
+  std::vector<exprt> values;
+  values.reserve(new_variables.size());
+  for(const auto &new_variable : new_variables)
+    values.push_back(new_variable);
+  return instantiate(values);
+}

src/util/std_expr.h

@@ -2797,8 +2797,37 @@ class binding_exprt : public binary_exprt
   {
     return op1();
   }
+
+  /// substitute free occurrences of the variables in where()
+  /// by the given values
+  exprt instantiate(const exprt::operandst &) const;
+
+  /// substitute free occurrences of the variables in where()
+  /// by a set of different symbols
+  exprt instantiate(const variablest &) const;
 };
 
+inline void validate_expr(const binding_exprt &binding_expr)
+{
+  validate_operands(
+    binding_expr, 2, "Binding expressions must have two operands");
+}
+
+/// \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 const binding_exprt &to_binding_expr(const exprt &expr)
+{
+  PRECONDITION(
+    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;
+}
+
 /// \brief A let expression
 class let_exprt : public binary_exprt
 {