Make `node_value.h` not depend on `node_manager.h` (#7676)

This commit breaks a circular dependency by making `node_value.h` not
depend on `node_manager.h`. As a result, we can remove the hack-y
include of `node_manager.h` in the middle of the `node_value.h` file.

diff --git a/src/expr/node.h b/src/expr/node.h
index b3c72c05e875deb08128d92bd0262c8aa77c0c6f..bd5f8c605f66de8b390a5da9252a38647d32e72e 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -15,9 +15,6 @@
 
 #include "cvc5_private.h"
 
-// circular dependency
-#include "expr/node_value.h"
-
 #ifndef CVC5__NODE_H
 #define CVC5__NODE_H
 
@@ -34,6 +31,7 @@
 #include "base/output.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
+#include "expr/node_value.h"
 #include "options/io_utils.h"
 #include "options/language.h"
 #include "util/hash.h"

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index d50c3bc00038effbe2d2025191417af5a017bff3..3d51cbbbe6581de4cbe7c073259e457f607a2085 100644 (file)
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -94,5 +94,38 @@ NodeValue::iterator<NodeTemplate<false> > operator+(
   return i + p;
 }
 
+std::ostream& operator<<(std::ostream& out, const NodeValue& nv)
+{
+  nv.toStream(out,
+              options::ioutils::getNodeDepth(out),
+              options::ioutils::getDagThresh(out),
+              options::ioutils::getOutputLang(out));
+  return out;
+}
+
+void NodeValue::markRefCountMaxedOut()
+{
+  Assert(NodeManager::currentNM() != nullptr)
+      << "No current NodeManager on incrementing of NodeValue: "
+         "maybe a public cvc5 interface function is missing a "
+         "NodeManagerScope ?";
+  NodeManager::currentNM()->markRefCountMaxedOut(this);
+}
+
+void NodeValue::markForDeletion()
+{
+  Assert(NodeManager::currentNM() != nullptr)
+      << "No current NodeManager on destruction of NodeValue: "
+         "maybe a public cvc5 interface function is missing a "
+         "NodeManagerScope ?";
+  NodeManager::currentNM()->markForDeletion(this);
+}
+
+bool NodeValue::isBeingDeleted() const
+{
+  return NodeManager::currentNM() != NULL
+         && NodeManager::currentNM()->isCurrentlyDeleting(this);
+}
+
 }  // namespace expr
 }  // namespace cvc5

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index b19417a6611145e471cd54eb1edb62b25e4b3868..cf24a207d77f918d227a884b381f8564a24d5d78 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -102,7 +102,7 @@ class NodeValue
       return iterator<NodeTemplate<true> >(d_i);
     }
 
-    inline T operator*() const;
+    T operator*() const { return T(*d_i); }
 
     bool operator==(const iterator& i) const { return d_i == i.d_i; }
 
@@ -295,8 +295,38 @@ class NodeValue
   /** Private constructor for the null value. */
   NodeValue(int);
 
-  void inc();
-  void dec();
+  void inc()
+  {
+    Assert(!isBeingDeleted())
+        << "NodeValue is currently being deleted "
+           "and increment is being called on it. Don't Do That!";
+    // FIXME multithreading
+    if (__builtin_expect((d_rc < MAX_RC - 1), true))
+    {
+      ++d_rc;
+    }
+    else if (__builtin_expect((d_rc == MAX_RC - 1), false))
+    {
+      ++d_rc;
+      markRefCountMaxedOut();
+    }
+  }
+
+  void dec()
+  {
+    // FIXME multithreading
+    if (__builtin_expect((d_rc < MAX_RC), true))
+    {
+      --d_rc;
+      if (__builtin_expect((d_rc == 0), false))
+      {
+        markForDeletion();
+      }
+    }
+  }
+
+  void markRefCountMaxedOut();
+  void markForDeletion();
 
   /** Decrement ref counts of children */
   inline void decrRefCounts();
@@ -389,16 +419,7 @@ struct NodeValueIDEquality {
   }
 };
 
-
-inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
-
-}  // namespace expr
-}  // namespace cvc5
-
-#include "expr/node_manager.h"
-
-namespace cvc5 {
-namespace expr {
+std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 
 inline NodeValue::NodeValue(int) :
   d_id(0),
@@ -413,37 +434,6 @@ inline void NodeValue::decrRefCounts() {
   }
 }
 
-inline void NodeValue::inc() {
-  Assert(!isBeingDeleted())
-      << "NodeValue is currently being deleted "
-         "and increment is being called on it. Don't Do That!";
-  // FIXME multithreading
-  if (__builtin_expect((d_rc < MAX_RC - 1), true)) {
-    ++d_rc;
-  } else if (__builtin_expect((d_rc == MAX_RC - 1), false)) {
-    ++d_rc;
-    Assert(NodeManager::currentNM() != NULL)
-        << "No current NodeManager on incrementing of NodeValue: "
-           "maybe a public cvc5 interface function is missing a "
-           "NodeManagerScope ?";
-    NodeManager::currentNM()->markRefCountMaxedOut(this);
-  }
-}
-
-inline void NodeValue::dec() {
-  // FIXME multithreading
-  if(__builtin_expect( ( d_rc < MAX_RC ), true )) {
-    --d_rc;
-    if(__builtin_expect( ( d_rc == 0 ), false )) {
-      Assert(NodeManager::currentNM() != NULL)
-          << "No current NodeManager on destruction of NodeValue: "
-             "maybe a public cvc5 interface function is missing a "
-             "NodeManagerScope ?";
-      NodeManager::currentNM()->markForDeletion(this);
-    }
-  }
-}
-
 inline NodeValue::nv_iterator NodeValue::nv_begin() {
   return d_children;
 }
@@ -474,11 +464,6 @@ inline NodeValue::iterator<T> NodeValue::end() const {
   return iterator<T>(d_children + d_nchildren);
 }
 
-inline bool NodeValue::isBeingDeleted() const {
-  return NodeManager::currentNM() != NULL &&
-    NodeManager::currentNM()->isCurrentlyDeleting(this);
-}
-
 inline NodeValue* NodeValue::getOperator() const {
   Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
   return d_children[0];
@@ -496,26 +481,4 @@ inline NodeValue* NodeValue::getChild(int i) const {
 }  // namespace expr
 }  // namespace cvc5
 
-#include "expr/node.h"
-
-namespace cvc5 {
-namespace expr {
-
-template <typename T>
-inline T NodeValue::iterator<T>::operator*() const {
-  return T(*d_i);
-}
-
-inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
-  nv.toStream(out,
-              options::ioutils::getNodeDepth(out),
-              options::ioutils::getDagThresh(out),
-              options::ioutils::getOutputLang(out));
-  return out;
-}
-
-}  // namespace expr
-
-}  // namespace cvc5
-
 #endif /* CVC5__EXPR__NODE_VALUE_H */

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 8dd27c400f805d2318371c09dec02fba0bc48873..95b3895eee500596a8c65df1cb363d3dab921b22 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -15,8 +15,7 @@
 
 #include "cvc5_private.h"
 
-// circular dependency
-#include "expr/node_value.h"
+#include "expr/node.h"
 
 #ifndef CVC5__TYPE_NODE_H
 #define CVC5__TYPE_NODE_H
@@ -29,6 +28,7 @@
 #include "base/check.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
+#include "expr/node_value.h"
 #include "util/cardinality_class.h"
 
 namespace cvc5 {