introduce binding_exprt::instantiate

This introduces a helper method to substitute variables that are bound in a
binding_exprt by a vector of given values.  The substitution algorithm
preserves sharing when no substitution is made and is aware of hiding when
nesting bindings.

Author: kroening

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/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,130 @@ 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 subsitution 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,35 @@ 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
 {