diff options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index aeea179d4..857bcc25f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -35,7 +35,7 @@ #include "expr/metakind.h" #include "expr/node_value.h" -namespace CVC5 { +namespace cvc5 { namespace api { class Solver; @@ -163,7 +163,7 @@ class NodeManager * PLUS, are APPLYs of a PLUS operator to arguments. This array * holds the set of operators for these things. A PLUS operator is * a Node with kind "BUILTIN", and if you call - * plusOperator->getConst<CVC5::Kind>(), you get kind::PLUS back. + * plusOperator->getConst<cvc5::Kind>(), you get kind::PLUS back. */ Node d_operators[kind::LAST_KIND]; @@ -660,7 +660,7 @@ class NodeManager /** * Get the (singleton) operator of an OPERATOR-kinded kind. The * returned node n will have kind BUILTIN, and calling - * n.getConst<CVC5::Kind>() will yield k. + * n.getConst<cvc5::Kind>() will yield k. */ inline TNode operatorOf(Kind k) { AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k, @@ -1203,7 +1203,7 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { d_nodeValuePool.erase(nv);// FIXME multithreading } -} // namespace CVC5 +} // namespace cvc5 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/metakind.h" @@ -1211,7 +1211,7 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { #include "expr/node_builder.h" -namespace CVC5 { +namespace cvc5 { // general expression-builders @@ -1577,6 +1577,6 @@ NodeClass NodeManager::mkConstInternal(const T& val) { return NodeClass(nv); } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__NODE_MANAGER_H */ |