diff options
Diffstat (limited to 'src/expr/node.h')
| -rw-r--r-- | src/expr/node.h | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 9e485ae78..291c2e538 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -41,7 +41,7 @@ #include "util/hash.h" #include "util/utility.h" -namespace CVC4 { +namespace CVC5 { class TypeNode; class NodeManager; @@ -138,16 +138,16 @@ class NodeValue; namespace attr { class AttributeManager; struct SmtAttributes; - }/* CVC4::expr::attr namespace */ + } // namespace attr class ExprSetDepth; -}/* CVC4::expr namespace */ + } // namespace expr namespace kind { namespace metakind { struct NodeValueConstPrinter; - }/* CVC4::kind::metakind namespace */ -}/* CVC4::kind namespace */ + } // namespace metakind + } // namespace kind // for hash_maps, hash_sets.. struct NodeHashFunction { @@ -199,10 +199,10 @@ class NodeTemplate { template <unsigned nchild_thresh> friend class NodeBuilder; - friend class ::CVC4::expr::attr::AttributeManager; - friend struct ::CVC4::expr::attr::SmtAttributes; + friend class ::CVC5::expr::attr::AttributeManager; + friend struct ::CVC5::expr::attr::SmtAttributes; - friend struct ::CVC4::kind::metakind::NodeValueConstPrinter; + friend struct ::CVC5::kind::metakind::NodeValueConstPrinter; /** * Assigns the expression value and does reference counting. No assumptions @@ -951,12 +951,12 @@ std::ostream& operator<<( return out; } -}/* CVC4 namespace */ +} // namespace CVC5 //#include "expr/attribute.h" #include "expr/node_manager.h" -namespace CVC4 { +namespace CVC5 { inline size_t NodeHashFunction::operator()(Node node) const { return node.getId(); @@ -986,7 +986,7 @@ template <class AttrKind> inline typename AttrKind::value_type NodeTemplate<ref_count>:: getAttribute(const AttrKind&) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC4::NodeManager associated to this thread.\n" + << "There is no current CVC5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -999,7 +999,7 @@ template <class AttrKind> inline bool NodeTemplate<ref_count>:: hasAttribute(const AttrKind&) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC4::NodeManager associated to this thread.\n" + << "There is no current CVC5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1012,7 +1012,7 @@ template <class AttrKind> inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC4::NodeManager associated to this thread.\n" + << "There is no current CVC5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1025,7 +1025,7 @@ template <class AttrKind> inline void NodeTemplate<ref_count>:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC4::NodeManager associated to this thread.\n" + << "There is no current CVC5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1225,7 +1225,7 @@ template <bool ref_count> NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC4::NodeManager associated to this thread.\n" + << "There is no current CVC5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1255,7 +1255,7 @@ template <bool ref_count> TypeNode NodeTemplate<ref_count>::getType(bool check) const { Assert(NodeManager::currentNM() != NULL) - << "There is no current CVC4::NodeManager associated to this thread.\n" + << "There is no current CVC5::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1491,6 +1491,6 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& } #endif /* CVC4_DEBUG */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__NODE_H */ |