diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/expr/node_manager.h | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 510e6d585..a3fd50d8c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -32,6 +32,7 @@ #include <string> #include <unordered_set> +#include "base/check.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" @@ -411,14 +412,16 @@ public: /** Subscribe to NodeManager events */ void subscribeEvents(NodeManagerListener* listener) { - Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed"); + Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) + == d_listeners.end()) + << "listener already subscribed"; d_listeners.push_back(listener); } /** Unsubscribe from NodeManager events */ void unsubscribeEvents(NodeManagerListener* listener) { std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener); - Assert(elt != d_listeners.end(), "listener not subscribed"); + Assert(elt != d_listeners.end()) << "listener not subscribed"; d_listeners.erase(elt); } @@ -1177,14 +1180,14 @@ inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { } inline void NodeManager::poolInsert(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), - "NodeValue already in the pool!"); + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end()) + << "NodeValue already in the pool!"; d_nodeValuePool.insert(nv);// FIXME multithreading } inline void NodeManager::poolRemove(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), - "NodeValue is not in the pool!"); + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end()) + << "NodeValue is not in the pool!"; d_nodeValuePool.erase(nv);// FIXME multithreading } @@ -1240,8 +1243,7 @@ inline bool NodeManager::hasOperator(Kind k) { case kind::metakind::CONSTANT: return false; - default: - Unhandled(mk); + default: Unhandled() << mk; } } |