From: Andres Noetzli Date: Tue, 23 Nov 2021 16:57:28 +0000 (-0800) Subject: Make `node_value.h` not depend on `node_manager.h` (#7676) X-Git-Tag: cvc5-1.0.0~785 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=175568cab882b8aec8172691cc165049eeea1c0f;p=cvc5.git 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 b3c72c05e..bd5f8c605 100644 --- 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 d50c3bc00..3d51cbbbe 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -94,5 +94,38 @@ NodeValue::iterator > 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 b19417a66..cf24a207d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -102,7 +102,7 @@ class NodeValue return iterator >(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 NodeValue::end() const { return iterator(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 -inline T NodeValue::iterator::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 8dd27c400..95b3895ee 100644 --- 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 {