From d4fdf8bd4f0f27b88f971541b112bbaee9564293 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 17 Nov 2021 19:12:22 -0300 Subject: [PATCH] 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. --- src/expr/term_canonize.cpp | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp index 5ab5a4b1b..8b6201b63 100644 --- 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& 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) -- 2.30.2