SMT2 parser: use lambda for function defintions

src/solvers/smt2/smt2_parser.cpp

@@ -131,13 +131,13 @@ exprt::operandst smt2_parsert::operands()
   return result;
 }
 
-void smt2_parsert::add_unique_id(const irep_idt &id, const exprt &expr)
+void smt2_parsert::add_unique_id(irep_idt id, exprt expr)
 {
   if(!id_map
         .emplace(
           std::piecewise_construct,
           std::forward_as_tuple(id),
-          std::forward_as_tuple(idt::VARIABLE, expr))
+          std::forward_as_tuple(idt::VARIABLE, std::move(expr)))
         .second)
   {
     // id already used
@@ -1484,7 +1484,7 @@ void smt2_parsert::setup_commands()
     }
 
     // now parse body with parameter ids in place
-    const auto body = expression();
+    auto body = expression();
 
     // remove the parameter ids
     for(auto &id : signature.parameters)
@@ -1512,11 +1512,12 @@ void smt2_parsert::setup_commands()
                     << smt2_format(body.type()) << '\'';
     }
 
-    // create the entry
-    add_unique_id(id, body);
+    // if there are parameters, this is a lambda
+    if(!signature.parameters.empty())
+      body = lambda_exprt(signature.binding_variables(), body);
 
-    id_map.at(id).type = signature.type;
-    id_map.at(id).parameters = signature.parameters;
+    // create the entry
+    add_unique_id(id, std::move(body));
   };
 
   commands["exit"] = [this]() { exit = true; };

src/solvers/smt2/smt2_parser.h

@@ -49,8 +49,9 @@ class smt2_parsert
 
     kindt kind;
     typet type;
+
+    // this is a lambda when the symbol is a function
     exprt definition;
-    std::vector<irep_idt> parameters;
   };
 
   using id_mapt=std::map<irep_idt, idt>;
@@ -95,7 +96,7 @@ class smt2_parsert
 
   // add the given identifier to the id_map but
   // complain if that identifier is used already
-  void add_unique_id(const irep_idt &, const exprt &);
+  void add_unique_id(irep_idt, exprt);
 
   struct signature_with_parameter_idst
   {
@@ -133,6 +134,15 @@ class smt2_parsert
         return result;
       }
     }
+
+    // convenience helper for constructing a binding
+    binding_exprt::variablest binding_variables() const
+    {
+      binding_exprt::variablest result;
+      for(auto &pair : ids_and_types())
+        result.emplace_back(pair.first, pair.second);
+      return result;
+    }
   };
 
   // expressions

src/solvers/smt2/smt2_solver.cpp

@@ -105,17 +105,12 @@ void smt2_solvert::expand_function_applications(exprt &expr)
         // Does it have a definition? It's otherwise uninterpreted.
         if(!f.definition.is_nil())
         {
-          replace_symbolt replace_symbol;
+          exprt body = f.definition;
 
-          for(std::size_t i = 0; i < domain.size(); i++)
-          {
-            replace_symbol.insert(
-              symbol_exprt(f.parameters[i], domain[i]), app.arguments()[i]);
-          }
+          if(body.id() == ID_lambda)
+            body = to_lambda_expr(body).application(app.arguments());
 
-          exprt body = f.definition;
-          replace_symbol(body);
-          expand_function_applications(body);
+          expand_function_applications(body); // rec. call
           expr = body;
         }
       }