From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 18 Apr 2022 21:29:24 +0000 (-0500)
Subject: Distinguish name variants for types in LFSC node converter (#8624)
X-Git-Tag: cvc5-1.0.1~251
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ed000bbe930890df67da1999aa76ed0d815e850;p=cvc5.git

Distinguish name variants for types in LFSC node converter (#8624)

This PR ensures we distinguish names for cases where types and terms are given the same name.

In particular, this generalizes the getNameForUserNameOf to work with node identifiers instead of Node, so that TypeNode can also use this method for assigning unique names.

It also adds preliminary support for uninterpreted sort constructors in the LFSC node converter.

This fixes 4 more LFSC failures on our regressions.
---

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index def75fe46..fcbf6cea0 100644
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -575,12 +575,18 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
       std::stringstream ss;
       options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
       tn.toStream(ss);
-      if (tn.isUninterpretedSort() || (tn.isDatatype() && !tn.isTuple()))
+      if (tn.isUninterpretedSortConstructor())
       {
-        std::stringstream sss;
-        sss << LfscNodeConverter::getNameForUserName(ss.str());
-        tnn = getSymbolInternal(k, d_sortType, sss.str(), false);
-        cur = nm->mkSort(sss.str());
+        std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
+        tnn = getSymbolInternal(k, d_sortType, s, false);
+        cur =
+            nm->mkSortConstructor(s, tn.getUninterpretedSortConstructorArity());
+      }
+      else if (tn.isUninterpretedSort() || (tn.isDatatype() && !tn.isTuple()))
+      {
+        std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
+        tnn = getSymbolInternal(k, d_sortType, s, false);
+        cur = nm->mkSort(s);
       }
       else
       {
@@ -621,7 +627,8 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
       d_declTypes.insert(tn.getUninterpretedSortConstructor());
       TypeNode ftype = nm->mkFunctionType(types, d_sortType);
       std::string name;
-      tn.getAttribute(expr::VarNameAttr(), name);
+      tn.getUninterpretedSortConstructor().getAttribute(expr::VarNameAttr(),
+                                                        name);
       op = getSymbolInternal(k, ftype, name, false);
     }
     else
@@ -699,9 +706,16 @@ std::string LfscNodeConverter::getNameForUserNameOf(Node v)
 {
   std::string name;
   v.getAttribute(expr::VarNameAttr(), name);
-  std::vector<Node>& syms = d_userSymbolList[name];
+  return getNameForUserNameOfInternal(v.getId(), name);
+}
+
+std::string LfscNodeConverter::getNameForUserNameOfInternal(
+    uint64_t id, const std::string& name)
+{
+  std::vector<uint64_t>& syms = d_userSymbolList[name];
   size_t variant = 0;
-  std::vector<Node>::iterator itr = std::find(syms.begin(), syms.end(), v);
+  std::vector<uint64_t>::iterator itr =
+      std::find(syms.begin(), syms.end(), id);
   if (itr != syms.cend())
   {
     variant = std::distance(syms.begin(), itr);
@@ -709,7 +723,7 @@ std::string LfscNodeConverter::getNameForUserNameOf(Node v)
   else
   {
     variant = syms.size();
-    syms.push_back(v);
+    syms.push_back(id);
   }
   return getNameForUserName(name, variant);
 }
diff --git a/src/proof/lfsc/lfsc_node_converter.h b/src/proof/lfsc/lfsc_node_converter.h
index 5d2861af2..497c94fd5 100644
--- a/src/proof/lfsc/lfsc_node_converter.h
+++ b/src/proof/lfsc/lfsc_node_converter.h
@@ -121,6 +121,9 @@ class LfscNodeConverter : public NodeConverter
   const std::unordered_set<TypeNode>& getDeclaredTypes() const;
 
  private:
+  /** get name for a Node/TypeNode whose id is id and whose name is name */
+  std::string getNameForUserNameOfInternal(uint64_t id,
+                                           const std::string& name);
   /** Should we traverse n? */
   bool shouldTraverse(Node n) override;
   /**
@@ -169,9 +172,10 @@ class LfscNodeConverter : public NodeConverter
   std::unordered_set<Node> d_symbols;
   /**
    * Mapping from user symbols to the (list of) symbols with that name. This
-   * is used to resolve symbol overloading, which is forbidden in LFSC.
+   * is used to resolve symbol overloading, which is forbidden in LFSC. We use
+   * Node identifiers, since this map is used for both Node and TypeNode.
    */
-  std::map<std::string, std::vector<Node> > d_userSymbolList;
+  std::map<std::string, std::vector<uint64_t> > d_userSymbolList;
   /** symbols to builtin kinds*/
   std::map<Node, Kind> d_symbolToBuiltinKind;
   /** arrow type constructor */