Improve naming in term canonization when handling HO variables (#7660)

Previously all higher-order variables would me named with "-" followed by the index, since the method did not account for functional types (which are printed as with (-> ...)). This commit changes it so that it takes the return type, which will always be atomic, thus giving more meaningful names to the canonical variables.

diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp
index 5ab5a4b1b97beed76ce55d6fa4ffcbc0c2b5ab11..8b6201b633c8b11beb1addc1cf8a776f9ae48fef 100644 (file)
--- a/src/expr/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -104,15 +104,22 @@ Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc)
   std::vector<Node>& tvars = d_cn_free_var[key];
   while (tvars.size() <= i)
   {
-    std::stringstream oss;
-    oss << tn;
-    std::string typ_name = oss.str();
-    while (typ_name[0] == '(')
+    std::stringstream os;
+    if (tn.isFunction())
     {
-      typ_name.erase(typ_name.begin());
+      os << "f" << i;
+    }
+    else
+    {
+      std::stringstream oss;
+      oss << tn;
+      std::string typ_name = oss.str();
+      while (typ_name[0] == '(')
+      {
+        typ_name.erase(typ_name.begin());
+      }
+      os << typ_name[0] << i;
     }
-    std::stringstream os;
-    os << typ_name[0] << i;
     Node x = nm->mkBoundVar(os.str().c_str(), tn);
     d_fvIndex[x] = tvars.size();
     tvars.push_back(x);
@@ -165,7 +172,7 @@ Node TermCanonize::getCanonicalTerm(
     var_count[key]++;
     Node fv = getCanonicalFreeVar(tn, vn, tc);
     visited[n] = fv;
-    Trace("canon-term-debug") << "...allocate variable." << std::endl;
+    Trace("canon-term-debug") << "...allocate variable " << fv << std::endl;
     return fv;
   }
   else if (n.getNumChildren() > 0)