Merge pull request #3524 from diffblue/no-identifiers-in-domain

separate parameter identifiers from (mathematical) function signature

Author: kroening

src/solvers/smt2/smt2_parser.cpp

@@ -987,18 +987,21 @@ typet smt2_parsert::sort()
   }
 }
 
-typet smt2_parsert::function_signature_definition()
+smt2_parsert::signature_with_parameter_idst
+smt2_parsert::function_signature_definition()
 {
   if(next_token()!=OPEN)
     throw error("expected '(' at beginning of signature");
 
   if(peek()==CLOSE)
   {
+    // no parameters
     next_token(); // eat the ')'
-    return sort();
+    return signature_with_parameter_idst(sort());
   }
 
   mathematical_function_typet::domaint domain;
+  std::vector<irep_idt> parameters;
 
   while(peek()!=CLOSE)
   {
@@ -1008,14 +1011,12 @@ typet smt2_parsert::function_signature_definition()
     if(next_token()!=SYMBOL)
       throw error("expected symbol in parameter");
 
-    mathematical_function_typet::variablet var;
-    std::string id=buffer;
-    var.set_identifier(id);
-    var.type()=sort();
-    domain.push_back(var);
+    irep_idt id = buffer;
+    parameters.push_back(id);
+    domain.push_back(sort());
 
     auto &entry=id_map[id];
-    entry.type=var.type();
+    entry.type = domain.back();
     entry.definition=nil_exprt();
 
     if(next_token()!=CLOSE)
@@ -1026,7 +1027,8 @@ typet smt2_parsert::function_signature_definition()
 
   typet codomain = sort();
 
-  return mathematical_function_typet(domain, codomain);
+  return signature_with_parameter_idst(
+    mathematical_function_typet(domain, codomain), parameters);
 }
 
 typet smt2_parsert::function_signature_declaration()
@@ -1050,9 +1052,7 @@ typet smt2_parsert::function_signature_declaration()
     if(next_token()!=SYMBOL)
       throw error("expected symbol in parameter");
 
-    mathematical_function_typet::variablet var;
-    var.type()=sort();
-    domain.push_back(var);
+    domain.push_back(sort());
 
     if(next_token()!=CLOSE)
       throw error("expected ')' at end of parameter");
@@ -1161,9 +1161,9 @@ void smt2_parsert::command(const std::string &c)
     const auto body = expression();
 
     // check type of body
-    if(signature.id() == ID_mathematical_function)
+    if(signature.type.id() == ID_mathematical_function)
     {
-      const auto &f_signature = to_mathematical_function_type(signature);
+      const auto &f_signature = to_mathematical_function_type(signature.type);
       if(body.type() != f_signature.codomain())
       {
         std::ostringstream msg;
@@ -1173,19 +1173,20 @@ void smt2_parsert::command(const std::string &c)
         throw error(msg.str());
       }
     }
-    else if(body.type() != signature)
+    else if(body.type() != signature.type)
     {
       std::ostringstream msg;
       msg << "type mismatch in function definition: expected `"
-          << smt2_format(signature) << "' but got `" << smt2_format(body.type())
-          << '\'';
+          << smt2_format(signature.type) << "' but got `"
+          << smt2_format(body.type()) << '\'';
       throw error(msg.str());
     }
 
     // create the entry
-    auto &entry=id_map[id];
-    entry.type=signature;
-    entry.definition=body;
+    auto &entry = id_map[id];
+    entry.type = signature.type;
+    entry.parameters = signature.parameters;
+    entry.definition = body;
   }
   else if(c=="exit")
   {

src/solvers/smt2/smt2_parser.h

@@ -37,6 +37,7 @@ class smt2_parsert:public smt2_tokenizert
 
     typet type;
     exprt definition;
+    std::vector<irep_idt> parameters;
   };
 
   using id_mapt=std::map<irep_idt, idt>;
@@ -73,13 +74,35 @@ class smt2_parsert:public smt2_tokenizert
   irep_idt get_fresh_id(const irep_idt &);
   irep_idt rename_id(const irep_idt &) const;
 
+  struct signature_with_parameter_idst
+  {
+    typet type;
+    std::vector<irep_idt> parameters;
+
+    explicit signature_with_parameter_idst(const typet &_type) : type(_type)
+    {
+    }
+
+    signature_with_parameter_idst(
+      const typet &_type,
+      const std::vector<irep_idt> &_parameters)
+      : type(_type), parameters(_parameters)
+    {
+      PRECONDITION(
+        (_type.id() == ID_mathematical_function &&
+         to_mathematical_function_type(_type).domain().size() ==
+           _parameters.size()) ||
+        (_type.id() != ID_mathematical_function && _parameters.empty()));
+    }
+  };
+
   void ignore_command();
   exprt expression();
   exprt function_application();
   typet sort();
   exprt::operandst operands();
   typet function_signature_declaration();
-  typet function_signature_definition();
+  signature_with_parameter_idst function_signature_definition();
   exprt multi_ary(irep_idt, const exprt::operandst &);
   exprt binary_predicate(irep_idt, const exprt::operandst &);
   exprt binary(irep_idt, const exprt::operandst &);

src/solvers/smt2/smt2_solver.cpp

@@ -103,17 +103,18 @@ void smt2_solvert::expand_function_applications(exprt &expr)
       const auto f_type=
         to_mathematical_function_type(f.type);
 
-      DATA_INVARIANT(f_type.domain().size()==
-                     app.arguments().size(),
-                     "number of function parameters");
+      const auto &domain = f_type.domain();
+
+      DATA_INVARIANT(
+        domain.size() == app.arguments().size(),
+        "number of function parameters");
 
       replace_symbolt replace_symbol;
 
       std::map<irep_idt, exprt> parameter_map;
-      for(std::size_t i=0; i<f_type.domain().size(); i++)
+      for(std::size_t i = 0; i < domain.size(); i++)
       {
-        const auto &var = f_type.domain()[i];
-        const symbol_exprt s(var.get_identifier(), var.type());
+        const symbol_exprt s(f.parameters[i], domain[i]);
         replace_symbol.insert(s, app.arguments()[i]);
       }
 

src/util/mathematical_types.h

@@ -59,33 +59,8 @@ class mathematical_function_typet : public type_with_subtypest
 {
 public:
   // the domain of the function is composed of zero, one, or
-  // many variables
-  class variablet : public irept
-  {
-  public:
-    // the identifier is optional
-    irep_idt get_identifier() const
-    {
-      return get(ID_identifier);
-    }
-
-    void set_identifier(const irep_idt &identifier)
-    {
-      return set(ID_identifier, identifier);
-    }
-
-    typet &type()
-    {
-      return static_cast<typet &>(add(ID_type));
-    }
-
-    const typet &type() const
-    {
-      return static_cast<const typet &>(find(ID_type));
-    }
-  };
-
-  using domaint = std::vector<variablet>;
+  // many variables, given by their type
+  using domaint = std::vector<typet>;
 
   mathematical_function_typet(const domaint &_domain, const typet &_codomain)
     : type_with_subtypest(ID_mathematical_function)
@@ -105,11 +80,9 @@ class mathematical_function_typet : public type_with_subtypest
     return (const domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
   }
 
-  variablet &add_variable()
+  void add_variable(const typet &_type)
   {
-    auto &d = domain();
-    d.push_back(variablet());
-    return d.back();
+    domain().push_back(_type);
   }
 
   /// Return the codomain, i.e., the set of values that the function maps to