From 0c65c780c6c7c52c26edf6ec0b8f45ef9fb496cf Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 11 Nov 2016 14:46:30 -0800 Subject: [PATCH] Speeding up the common branches for inc(). --- src/expr/node_value.h | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 8f1df0fff..79ce8cb4f 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -298,9 +298,10 @@ public: private: /** - * RAII guard that increases the reference count if the reference count to be > 0. - * Otherwise, this does nothing. This does not just increment the reference - * count to avoid maxing out the d_rc field. This is only for low level functions. + * RAII guard that increases the reference count if the reference count to be + * > 0. Otherwise, this does nothing. This does not just increment the + * reference count to avoid maxing out the d_rc field. This is only for low + * level functions. */ class RefCountGuard { NodeValue* d_nv; @@ -422,15 +423,15 @@ inline void NodeValue::inc() { "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 ), true )) { + if (__builtin_expect((d_rc < MAX_RC - 1), true)) { ++d_rc; - if(__builtin_expect( ( d_rc == MAX_RC ), false )) { - Assert(NodeManager::currentNM() != NULL, - "No current NodeManager on incrementing of NodeValue: " - "maybe a public CVC4 interface function is missing a " - "NodeManagerScope ?"); - NodeManager::currentNM()->markRefCountMaxedOut(this); - } + } 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 CVC4 interface function is missing a " + "NodeManagerScope ?"); + NodeManager::currentNM()->markRefCountMaxedOut(this); } } -- 2.30.2