From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 16 Nov 2021 15:59:04 +0000 (-0800)
Subject: Refactor `metakind` (#7639)
X-Git-Tag: cvc5-1.0.0~816
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7e709d60b5a9923ac56f0948dd9e3b26b4b3205;p=cvc5.git

Refactor `metakind` (#7639)

This is a first attempt of refactoring our `metakind` definitions and
declarations. The commit removes unnecessary code that was being
generated, moves code from header to source files (primarily code that
was only relevant to the source file), and gets rid of some hacks
related to circular dependencies.
---

diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
index 1d0f5dd50..857a76889 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -16,15 +16,24 @@
  * \todo document this file
  */
 
-#include "expr/metakind.h"
-
 #include <iostream>
 
+#include "expr/metakind.h"
+#include "expr/node_value.h"
+
 // clang-format off
 ${metakind_includes}
 // clang-format off
 
 namespace cvc5 {
+namespace expr {
+
+// clang-format off
+${metakind_constantMaps}
+// clang-format on
+
+}  // namespace expr
+
 namespace kind {
 
 /**
@@ -48,18 +57,49 @@ ${metakind_kinds}  // clang-format on
   return metaKinds[k + 1];
 } /* metaKindOf(k) */
 
-}  // namespace kind
-
-namespace expr {
+namespace metakind {
 
-// clang-format off
-${metakind_constantMaps}
-// clang-format on
+/**
+ * Static, compile-time mapping from CONSTANT kinds to comparison
+ * functors on NodeValue*.  The single element of this structure is:
+ *
+ *   static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y)
+ *
+ *     Compares x and y, given that they are both K-kinded (and the
+ *     meta-kind of K is CONSTANT).  If pool == true, one of x and y
+ *     (but not both) may be a "non-inlined" NodeValue.  If pool ==
+ *     false, neither x nor y may be a "non-inlined" NodeValue.
+ */
+template <Kind k, class T, bool pool>
+struct NodeValueConstCompare
+{
+  static bool compare(const ::cvc5::expr::NodeValue* x,
+                      const ::cvc5::expr::NodeValue* y)
+  {
+    if (pool)
+    {
+      if (x->d_nchildren == 1)
+      {
+        Assert(y->d_nchildren == 0);
+        return compare(y, x);
+      }
+      else if (y->d_nchildren == 1)
+      {
+        Assert(x->d_nchildren == 0);
+        return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
+      }
+    }
 
-}  // namespace expr
+    Assert(x->d_nchildren == 0);
+    Assert(y->d_nchildren == 0);
+    return x->getConst<T>() == y->getConst<T>();
+  }
 
-namespace kind {
-namespace metakind {
+  static size_t constHash(const ::cvc5::expr::NodeValue* nv)
+  {
+    return nv->getConst<T>().hash();
+  }
+};
 
 size_t NodeValueCompare::constHash(const ::cvc5::expr::NodeValue* nv)
 {
@@ -117,8 +157,8 @@ template bool NodeValueCompare::compare<true>(
 template bool NodeValueCompare::compare<false>(
     const ::cvc5::expr::NodeValue* nv1, const ::cvc5::expr::NodeValue* nv2);
 
-void NodeValueConstPrinter::toStream(std::ostream& out,
-                                     const ::cvc5::expr::NodeValue* nv)
+void nodeValueConstantToStream(std::ostream& out,
+                               const ::cvc5::expr::NodeValue* nv)
 {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
@@ -131,9 +171,6 @@ default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
-void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
-  toStream(out, n.d_nv);
-}
 
 // The reinterpret_cast of d_children to various constant payload types
 // in deleteNodeValueConstant(), below, can flag a "strict aliasing"
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 09469915f..935b65ab6 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -49,35 +49,6 @@ namespace metakind {
 template <class T>
 struct ConstantMap;
 
-/**
- * Static, compile-time information about kinds k and what type their
- * corresponding cvc5 constants are:
- *
- *   typename ConstantMapReverse<k>::T
- *
- *     Constant type for kind k.
- */
-template <Kind k>
-struct ConstantMapReverse;
-
-/**
- * Static, compile-time mapping from CONSTANT kinds to comparison
- * functors on NodeValue*.  The single element of this structure is:
- *
- *   static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y)
- *
- *     Compares x and y, given that they are both K-kinded (and the
- *     meta-kind of K is CONSTANT).  If pool == true, one of x and y
- *     (but not both) may be a "non-inlined" NodeValue.  If pool ==
- *     false, neither x nor y may be a "non-inlined" NodeValue.
- */
-template <Kind k, bool pool>
-struct NodeValueConstCompare {
-  inline static bool compare(const ::cvc5::expr::NodeValue* x,
-                             const ::cvc5::expr::NodeValue* y);
-  inline static size_t constHash(const ::cvc5::expr::NodeValue* nv);
-};/* NodeValueConstCompare<k, pool> */
-
 struct NodeValueCompare {
   template <bool pool>
   static bool compare(const ::cvc5::expr::NodeValue* nv1,
@@ -101,6 +72,32 @@ enum MetaKind_t {
   NULLARY_OPERATOR /**< nullary operator */
 };/* enum MetaKind_t */
 
+/**
+ * Write the string representation of a payload of a constant node to an output
+ * stream.
+ *
+ * @param out the stream to write to
+ * @param nv the node value representing a constant node
+ */
+void nodeValueConstantToStream(std::ostream& out,
+                               const ::cvc5::expr::NodeValue* nv);
+
+/**
+ * Cleanup to be performed when a NodeValue zombie is collected, and
+ * it has CONSTANT metakind.  This calls the destructor for the underlying
+ * C++ type representing the constant value.  See
+ * NodeManager::reclaimZombies() for more information.
+ *
+ * This doesn't support "non-inlined" NodeValues, which shouldn't need this
+ * kind of cleanup.
+ */
+void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv);
+
+/** Return the minimum arity of the given kind. */
+uint32_t getMinArityForKind(::cvc5::Kind k);
+/** Return the maximum arity of the given kind. */
+uint32_t getMaxArityForKind(::cvc5::Kind k);
+
 }  // namespace metakind
 
 // import MetaKind into the "cvc5::kind" namespace but keep the
@@ -111,13 +108,22 @@ typedef ::cvc5::kind::metakind::MetaKind_t MetaKind;
  * Get the metakind for a particular kind.
  */
 MetaKind metaKindOf(Kind k);
+
+/**
+ * Map a kind of the operator to the kind of the enclosing expression. For
+ * example, since the kind of functions is just VARIABLE, it should map
+ * VARIABLE to APPLY_UF.
+ */
+Kind operatorToKind(::cvc5::expr::NodeValue* nv);
+
 }  // namespace kind
 
 namespace expr {
 
 // Comparison predicate
 struct NodeValuePoolEq {
-  inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
+  bool operator()(const NodeValue* nv1, const NodeValue* nv2) const
+  {
     return ::cvc5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
   }
 };
@@ -125,8 +131,6 @@ struct NodeValuePoolEq {
 }  // namespace expr
 }  // namespace cvc5
 
-#include "expr/node_value.h"
-
 #endif /* CVC5__KIND__METAKIND_H */
 
 #ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP
@@ -137,80 +141,15 @@ namespace cvc5 {
 ${metakind_fwd_decls}
 // clang-format on
 
-namespace expr {
-// clang-format off
-${metakind_getConst_decls}
-// clang-format on
-}  // namespace expr
-
 namespace kind {
 namespace metakind {
 
-template <Kind k, bool pool>
-inline bool NodeValueConstCompare<k, pool>::compare(
-    const ::cvc5::expr::NodeValue* x, const ::cvc5::expr::NodeValue* y)
-{
-  typedef typename ConstantMapReverse<k>::T T;
-  if(pool) {
-    if(x->d_nchildren == 1) {
-      Assert(y->d_nchildren == 0);
-      return compare(y, x);
-    } else if(y->d_nchildren == 1) {
-      Assert(x->d_nchildren == 0);
-      return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
-    }
-  }
-
-  Assert(x->d_nchildren == 0);
-  Assert(y->d_nchildren == 0);
-  return x->getConst<T>() == y->getConst<T>();
-}
-
-template <Kind k, bool pool>
-inline size_t NodeValueConstCompare<k, pool>::constHash(
-    const ::cvc5::expr::NodeValue* nv)
-{
-  typedef typename ConstantMapReverse<k>::T T;
-  return nv->getConst<T>().hash();
-}
-
 // clang-format off
 ${metakind_constantMaps_decls}
 // clang-format on
 
-struct NodeValueConstPrinter
-{
-  static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv);
-  static void toStream(std::ostream& out, TNode n);
-};
-
-/**
- * Cleanup to be performed when a NodeValue zombie is collected, and
- * it has CONSTANT metakind.  This calls the destructor for the underlying
- * C++ type representing the constant value.  See
- * NodeManager::reclaimZombies() for more information.
- *
- * This doesn't support "non-inlined" NodeValues, which shouldn't need this
- * kind of cleanup.
- */
-void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv);
-
-/** Return the minimum arity of the given kind. */
-uint32_t getMinArityForKind(::cvc5::Kind k);
-/** Return the maximum arity of the given kind. */
-uint32_t getMaxArityForKind(::cvc5::Kind k);
-
 }  // namespace metakind
-
-/**
- * Map a kind of the operator to the kind of the enclosing expression. For
- * example, since the kind of functions is just VARIABLE, it should map
- * VARIABLE to APPLY_UF.
- */
-Kind operatorToKind(::cvc5::expr::NodeValue* nv);
-
 }  // namespace kind
-
 }  // namespace cvc5
 
 #endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index e651de433..9b3d5a776 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -254,11 +254,6 @@ $2 ${class};"
   register_metakind CONSTANT "$1" 0
 
   if [[ "${payload_seen}" != true ]]; then
-    metakind_getConst_decls="${metakind_getConst_decls}
-template <>
-${class} const& NodeValue::getConst< ${class} >() const;
-"
-
     metakind_constantMaps="${metakind_constantMaps}
 // The reinterpret_cast of d_children to \"${class} const*\"
 // flags a \"strict aliasing\" warning; it's okay, because we never access
@@ -293,16 +288,9 @@ struct ConstantMap< ${class} > {
 "
   fi
 
-  metakind_constantMaps_decls="${metakind_constantMaps_decls}
-template <>
-struct ConstantMapReverse< ::cvc5::kind::$1 > {
-  using T = ${class};
-};/* ConstantMapReverse< ::cvc5::kind::$1 > */
-"
-
   metakind_compares="${metakind_compares}
     case kind::$1:
-      return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2);
+      return NodeValueConstCompare<kind::$1, ${class}, pool>::compare(nv1, nv2);
 "
   metakind_constHashes="${metakind_constHashes}
   case kind::$1:
@@ -435,7 +423,6 @@ for var in \
     metakind_kinds \
     metakind_constantMaps \
     metakind_constantMaps_decls \
-    metakind_getConst_decls \
     metakind_compares \
     metakind_constHashes \
     metakind_constPrinters \
diff --git a/src/expr/node.h b/src/expr/node.h
index 048a05e46..afc648ed8 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -161,12 +161,6 @@ class NodeValue;
   class ExprSetDepth;
   }  // namespace expr
 
-namespace kind {
-  namespace metakind {
-    struct NodeValueConstPrinter;
-    }  // namespace metakind
-    }  // namespace kind
-
 /**
  * Encapsulation of an NodeValue pointer.  The reference count is
  * maintained in the NodeValue if ref_count is true.
@@ -211,8 +205,6 @@ class NodeTemplate {
   friend class ::cvc5::expr::attr::AttributeManager;
   friend struct ::cvc5::expr::attr::SmtAttributes;
 
-  friend struct ::cvc5::kind::metakind::NodeValueConstPrinter;
-
   /**
    * Assigns the expression value and does reference counting. No assumptions
    * are made on the expression, and should only be used if we know what we
@@ -835,6 +827,11 @@ public:
     d_nv->toStream(out, toDepth, dagThreshold, language);
   }
 
+  void constToStream(std::ostream& out) const
+  {
+    kind::metakind::nodeValueConstantToStream(out, d_nv);
+  }
+
   /**
    * IOStream manipulator to set the maximum depth of Nodes when
    * pretty-printing.  -1 means print to any depth.  E.g.:
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 46ba3d191..d50c3bc00 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -66,7 +66,7 @@ void NodeValue::printAst(std::ostream& out, int ind) const {
     out << ' ' << getId();
   } else if (getMetaKind() == kind::metakind::CONSTANT) {
     out << ' ';
-    kind::metakind::NodeValueConstPrinter::toStream(out, this);
+    kind::metakind::nodeValueConstantToStream(out, this);
   } else {
     if (nv_begin() != nv_end()) {
       for (const_nv_iterator child = nv_begin(); child != nv_end(); ++child) {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index ba30dc8fb..19f66896d 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -20,9 +20,6 @@
 
 #include "cvc5_private.h"
 
-// circular dependency
-#include "expr/metakind.h"
-
 #ifndef CVC5__EXPR__NODE_VALUE_H
 #define CVC5__EXPR__NODE_VALUE_H
 
@@ -30,6 +27,7 @@
 #include <string>
 
 #include "expr/kind.h"
+#include "expr/metakind.h"
 #include "options/language.h"
 
 namespace cvc5 {
@@ -45,13 +43,12 @@ namespace expr {
 
 namespace kind {
   namespace metakind {
-  template < ::cvc5::Kind k, bool pool>
+
+  template < ::cvc5::Kind k, class T, bool pool>
   struct NodeValueConstCompare;
 
   struct NodeValueCompare;
-  struct NodeValueConstPrinter;
 
-  void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv);
   }  // namespace metakind
   }  // namespace kind
 
@@ -68,13 +65,14 @@ class NodeValue
   friend class ::cvc5::NodeBuilder;
   friend class ::cvc5::NodeManager;
 
-  template <Kind k, bool pool>
-  friend struct ::cvc5::kind::metakind::NodeValueConstCompare;
+  template <Kind k, class T, bool pool>
+  friend struct kind::metakind::NodeValueConstCompare;
 
-  friend struct ::cvc5::kind::metakind::NodeValueCompare;
-  friend struct ::cvc5::kind::metakind::NodeValueConstPrinter;
+  friend struct kind::metakind::NodeValueCompare;
 
-  friend void ::cvc5::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
+  friend void kind::metakind::nodeValueConstantToStream(std::ostream& out,
+                                                        const NodeValue* nv);
+  friend void kind::metakind::deleteNodeValueConstant(NodeValue* nv);
 
   friend class RefCountGuard;
 
@@ -185,7 +183,7 @@ class NodeValue
 
   /** If this is a CONST_* Node, extract the constant from it.  */
   template <class T>
-  inline const T& getConst() const;
+  const T& getConst() const;
 
   static inline NodeValue& null()
   {
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index c35d55d05..9a55d8377 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -70,7 +70,7 @@ void AstPrinter::toStream(std::ostream& out,
   if(n.getMetaKind() == kind::metakind::CONSTANT) {
     // constant
     out << ' ';
-    kind::metakind::NodeValueConstPrinter::toStream(out, n);
+    n.constToStream(out);
   }
   else if (n.isClosure())
   {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 30433ec1a..fe41f2256 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -182,7 +182,7 @@ void Smt2Printer::toStream(std::ostream& out,
       default:
         // fall back on whatever operator<< does on underlying type; we
         // might luck out and be SMT-LIB v2 compliant
-        kind::metakind::NodeValueConstPrinter::toStream(out, n);
+        n.constToStream(out);
       }
       break;
     case kind::BITVECTOR_TYPE:
@@ -454,7 +454,7 @@ void Smt2Printer::toStream(std::ostream& out,
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
-      kind::metakind::NodeValueConstPrinter::toStream(out, n);
+      n.constToStream(out);
     }
 
     return;