remove lambda_exprt::application

lambda_exprt uses a binding_exprt, which means that the application of a
function given as lambda expression is a special case of an instantiation.

Author: kroening

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 <>