Working towards handling parametric datatypes

ajreynol · Jan 23, 2025 · f4e6c7a · f4e6c7a
1 parent dbb62bd
commit f4e6c7a
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 2 deletions.
diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp
@@ -557,6 +557,10 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n)
       {
         opName << dt[index].getConstructor();
       }
+      if (dt.isParametric() && isAmbiguousDtConstructor(dt[index].getConstructor()))
+      {
+
+      }
     }
     else if (k == Kind::APPLY_SELECTOR)
     {
@@ -633,6 +637,39 @@ size_t AlfNodeConverter::getOrAssignIndexForConst(Node v)
   return id;
 }
 
+bool AlfNodeConverter::isAmbiguousDtConstructor(const Node& op)
+{
+  std::map<Node, bool>::iterator it = d_ambDt.find(op);
+  if (it!=d_ambDt.end())
+  {
+    return it->second;
+  }
+  bool ret = false;
+  TypeNode tn = op.getType();
+  Trace("alf-amb-dt") << "Ambiguous datatype constructor? " << op << " " << tn << std::endl;
+  size_t nchild = tn.getNumChildren();
+  Assert (nchild>0);
+  std::unordered_set<TypeNode> atypes;
+  for (size_t i=0; i<nchild-1; i++)
+  {
+    expr::getComponentTypes(tn[i], atypes);
+  }
+  const DType& dt = DType::datatypeOf(op);
+  std::vector<TypeNode> params = dt.getParameters();
+  for (const TypeNode& p : params)
+  {
+    if (atypes.find(p)==atypes.end())
+    {
+      Trace("alf-amb-dt") << "...yes since " << p << " not contained" << std::endl;
+      ret = true;
+      break;
+    }
+  }
+  Trace("alf-amb-dt") << "...returns " << ret << std::endl;
+  d_ambDt[op] = ret;
+  return ret;
+}
+
 bool AlfNodeConverter::isHandledSkolemId(SkolemId id)
 {
   // Note we don't handle skolems that take types as arguments yet.

diff --git a/src/proof/alf/alf_node_converter.h b/src/proof/alf/alf_node_converter.h
@@ -134,8 +134,8 @@ class AlfNodeConverter : public BaseAlfNodeConverter
    * signature.
    */
   Node maybeMkSkolemFun(Node k);
-  /** Is k a kind that is printed as an indexed operator in ALF? */
-  static bool isIndexedOperatorKind(Kind k);
+  /** Is op an ambiguous datatype constructor? */
+  bool isAmbiguousDtConstructor(const Node& op);
   /** Do we handle the given skolem id? */
   static bool isHandledSkolemId(SkolemId id);
   /** Get indices for printing the operator of n in the ALF format */
@@ -148,6 +148,8 @@ class AlfNodeConverter : public BaseAlfNodeConverter
   std::map<Node, size_t> d_constIndex;
   /** Cache for typeAsNode */
   std::map<TypeNode, Node> d_typeAsNode;
+  /** Cache for isAmbiguousDtConstructor */
+  std::map<Node, bool> d_ambDt;
 };
 
 }  // namespace proof