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 def75fe4661d2730027ebb81b19df43af2375cea..fcbf6cea04e7e3177ab67dad734408dd13c8205b 100644 (file)
--- 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 5d2861af2d017eee89a85e1123a61eabae6b0a33..497c94fd58d33ca925831e41b04adf24c596d565 100644 (file)
--- 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 */