diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a5329147b..370f0fb4c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -35,9 +35,9 @@ #include "util/resource_manager.h" using namespace std; -using namespace CVC4::expr; +using namespace CVC5::expr; -namespace CVC4 { +namespace CVC5 { thread_local NodeManager* NodeManager::s_current = NULL; @@ -87,7 +87,7 @@ struct NVReclaim { namespace attr { struct LambdaBoundVarListTag { }; -}/* CVC4::attr namespace */ + } // namespace attr // attribute that stores the canonical bound variable list for function types typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr; @@ -373,7 +373,7 @@ void NodeManager::reclaimZombies() { if(mk == kind::metakind::CONSTANT) { // Destroy (call the destructor for) the C++ type representing // the constant in this NodeValue. This is needed for - // e.g. CVC4::Rational, since it has a gmp internal + // e.g. CVC5::Rational, since it has a gmp internal // representation that mallocs memory and should be cleaned // up. (This won't delete a pointer value if used as a // constant, but then, you should probably use a smart-pointer @@ -678,7 +678,7 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes( << "malformed selector in datatype post-resolution"; // This next one's a "hard" check, performed in non-debug builds // as well; the other ones should all be guaranteed by the - // CVC4::DType class, but this actually needs to be checked. + // CVC5::DType class, but this actually needs to be checked. AlwaysAssert(!selectorType.getRangeType().isFunctionLike()) << "cannot put function-like things in datatypes"; } @@ -1170,4 +1170,4 @@ Kind NodeManager::getKindForFunction(TNode fun) return kind::UNDEFINED_KIND; } -}/* CVC4 namespace */ +} // namespace CVC5 |