applying functions that aren't symbols

SMT-LIB 3 will bring function applications for terms that aren't symbols
(e.g., lamba, choice).

This commit removes the restriction that the function in a function
application has to be a symbol.  The expression is still required to have
function type.

Author: Daniel Kroening

src/solvers/smt2/smt2_solver.cpp

@@ -81,39 +81,42 @@ void smt2_solvert::expand_function_applications(exprt &expr)
   {
     auto &app=to_function_application_expr(expr);
 
-    // look it up
-    irep_idt identifier=app.function().get_identifier();
-    auto f_it=id_map.find(identifier);
-
-    if(f_it!=id_map.end())
+    if(app.function().id() == ID_symbol)
     {
-      const auto &f=f_it->second;
+      // look up the symbol
+      auto identifier = to_symbol_expr(app.function()).get_identifier();
+      auto f_it = id_map.find(identifier);
 
-      DATA_INVARIANT(f.type.id()==ID_mathematical_function,
-        "type of function symbol must be mathematical_function_type");
+      if(f_it != id_map.end())
+      {
+        const auto &f = f_it->second;
 
-      const auto f_type=
-        to_mathematical_function_type(f.type);
+        DATA_INVARIANT(
+          f.type.id() == ID_mathematical_function,
+          "type of function symbol must be mathematical_function_type");
 
-      const auto &domain = f_type.domain();
+        const auto f_type = to_mathematical_function_type(f.type);
 
-      DATA_INVARIANT(
-        domain.size() == app.arguments().size(),
-        "number of function parameters");
+        const auto &domain = f_type.domain();
 
-      replace_symbolt replace_symbol;
+        DATA_INVARIANT(
+          domain.size() == app.arguments().size(),
+          "number of function parameters");
 
-      std::map<irep_idt, exprt> parameter_map;
-      for(std::size_t i = 0; i < domain.size(); i++)
-      {
-        const symbol_exprt s(f.parameters[i], domain[i]);
-        replace_symbol.insert(s, app.arguments()[i]);
-      }
+        replace_symbolt replace_symbol;
 
-      exprt body=f.definition;
-      replace_symbol(body);
-      expand_function_applications(body);
-      expr=body;
+        std::map<irep_idt, exprt> parameter_map;
+        for(std::size_t i = 0; i < domain.size(); i++)
+        {
+          const symbol_exprt s(f.parameters[i], domain[i]);
+          replace_symbol.insert(s, app.arguments()[i]);
+        }
+
+        exprt body = f.definition;
+        replace_symbol(body);
+        expand_function_applications(body);
+        expr = body;
+      }
     }
   }
 }

src/solvers/strings/string_builtin_function.h

@@ -484,7 +484,9 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
 
   std::string name() const override
   {
-    return id2string(function_application.function().get_identifier());
+    PRECONDITION(function_application.function().id() == ID_symbol);
+    return id2string(
+      to_symbol_expr(function_application.function()).get_identifier());
   }
   std::vector<array_string_exprt> string_arguments() const override
   {

src/util/mathematical_expr.cpp

@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include "mathematical_types.h"
 
 function_application_exprt::function_application_exprt(
-  const symbol_exprt &_function,
+  const exprt &_function,
   argumentst _arguments)
   : binary_exprt(
       _function,

src/util/mathematical_expr.h

@@ -211,18 +211,16 @@ class function_application_exprt : public binary_exprt
   {
   }
 
-  function_application_exprt(
-    const symbol_exprt &_function,
-    argumentst _arguments);
+  function_application_exprt(const exprt &_function, argumentst _arguments);
 
-  symbol_exprt &function()
+  exprt &function()
   {
-    return static_cast<symbol_exprt &>(op0());
+    return op0();
   }
 
-  const symbol_exprt &function() const
+  const exprt &function() const
   {
-    return static_cast<const symbol_exprt &>(op0());
+    return op0();
   }
 
   argumentst &arguments()