Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don't escape...

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

diff --git a/src/expr/node.h b/src/expr/node.h
index 7003aae87875d9c1e99a805c0bbc27c73cf75186..d9e88d8af5eca76eb1a7d578bcd21d6358d2fef0 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1094,7 +1094,7 @@ NodeTemplate<ref_count>& NodeTemplate<ref_count>::
 operator=(const NodeTemplate& e) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
-  if(EXPECT_TRUE( d_nv != e.d_nv )) {
+  if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
     if(ref_count) {
       // shouldn't ever fail
       Assert(d_nv->d_rc > 0,
@@ -1118,7 +1118,7 @@ NodeTemplate<ref_count>& NodeTemplate<ref_count>::
 operator=(const NodeTemplate<!ref_count>& e) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
-  if(EXPECT_TRUE( d_nv != e.d_nv )) {
+  if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
     if(ref_count) {
       // shouldn't ever fail
       Assert(d_nv->d_rc > 0, "Node reference count would be negative");

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 773828ccbcfa55c107fc3489124edd901bc06c6d..1f098b4e8b823533034f45d3548407ed84533e38 100644 (file)
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -228,7 +228,7 @@ class NodeBuilder {
    * Internally, this state is represented by d_nv pointing to NULL.
    */
   inline bool isUsed() const {
-    return EXPECT_FALSE( d_nv == NULL );
+    return __builtin_expect( ( d_nv == NULL ), false );
   }
 
   /**
@@ -259,7 +259,7 @@ class NodeBuilder {
    * heap-allocated by this class).
    */
   inline bool nvIsAllocated() const {
-    return EXPECT_FALSE( d_nv != &d_inlineNv ) && EXPECT_TRUE( d_nv != NULL );
+    return __builtin_expect( ( d_nv != &d_inlineNv ), false ) && __builtin_expect(( d_nv != NULL ), true );
   }
 
   /**
@@ -267,7 +267,7 @@ class NodeBuilder {
    * first.
    */
   inline bool nvNeedsToBeAllocated() const {
-    return EXPECT_FALSE( d_nv->d_nchildren == d_nvMaxChildren );
+    return __builtin_expect( ( d_nv->d_nchildren == d_nvMaxChildren ), false );
   }
 
   /**
@@ -279,7 +279,7 @@ class NodeBuilder {
   inline void realloc() {
     size_t newSize = 2 * size_t(d_nvMaxChildren);
     size_t hardLimit = (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
-    realloc(EXPECT_FALSE( newSize > hardLimit ) ? hardLimit : newSize);
+    realloc(__builtin_expect( ( newSize > hardLimit ), false ) ? hardLimit : newSize);
   }
 
   /**
@@ -297,7 +297,7 @@ class NodeBuilder {
    * double-decremented on destruction/clear.  Otherwise, do nothing.
    */
   inline void allocateNvIfNecessaryForAppend() {
-    if(EXPECT_FALSE( nvNeedsToBeAllocated() )) {
+    if(__builtin_expect( ( nvNeedsToBeAllocated() ), false )) {
       realloc();
     }
   }
@@ -331,8 +331,8 @@ class NodeBuilder {
    * @throws bad_alloc if the reallocation fails
    */
   void crop() {
-    if(EXPECT_FALSE( nvIsAllocated() ) &&
-       EXPECT_TRUE( d_nvMaxChildren > d_nv->d_nchildren )) {
+    if(__builtin_expect( ( nvIsAllocated() ), false ) &&
+       __builtin_expect( ( d_nvMaxChildren > d_nv->d_nchildren ), true )) {
       // Ensure d_nv is not modified on allocation failure
       expr::NodeValue* newBlock = (expr::NodeValue*)
         std::realloc(d_nv,
@@ -419,9 +419,9 @@ public:
   }
 
   inline ~NodeBuilder() {
-    if(EXPECT_FALSE( nvIsAllocated() )) {
+    if(__builtin_expect( ( nvIsAllocated() ), false )) {
       dealloc();
-    } else if(EXPECT_FALSE( !isUsed() )) {
+    } else if(__builtin_expect( ( !isUsed() ), false )) {
       decrRefCounts();
     }
   }
@@ -578,7 +578,7 @@ public:
     // NodeBuilder construction or at the last clear()), but we do
     // now.  That means we appended a Kind with operator<<(Kind),
     // which now (lazily) we'll collapse.
-    if(EXPECT_FALSE( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND )) {
+    if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
       Node n2 = operator Node();
       clear();
       append(n2);
@@ -600,7 +600,7 @@ public:
     // NodeBuilder construction or at the last clear()), but we do
     // now.  That means we appended a Kind with operator<<(Kind),
     // which now (lazily) we'll collapse.
-    if(EXPECT_FALSE( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND )) {
+    if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
       Node n2 = operator Node();
       clear();
       append(n2);
@@ -619,7 +619,7 @@ public:
     // NodeBuilder construction or at the last clear()), but we do
     // now.  That means we appended a Kind with operator<<(Kind),
     // which now (lazily) we'll collapse.
-    if(EXPECT_FALSE( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND )) {
+    if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
       Node n2 = operator Node();
       clear();
       append(n2);
@@ -756,9 +756,9 @@ template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::clear(Kind k) {
   Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind");
 
-  if(EXPECT_FALSE( nvIsAllocated() )) {
+  if(__builtin_expect( ( nvIsAllocated() ), false )) {
     dealloc();
-  } else if(EXPECT_FALSE( !isUsed() )) {
+  } else if(__builtin_expect( ( !isUsed() ), false )) {
     decrRefCounts();
   } else {
     setUnused();
@@ -783,7 +783,7 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
           "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
           toSize, (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
 
-  if(EXPECT_FALSE( nvIsAllocated() )) {
+  if(__builtin_expect( ( nvIsAllocated() ), false )) {
     // Ensure d_nv is not modified on allocation failure
     expr::NodeValue* newBlock = (expr::NodeValue*)
       std::realloc(d_nv, sizeof(expr::NodeValue) +
@@ -992,7 +992,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   // NodeManager pool of Nodes.  See implementation notes at the top
   // of this file.
 
-  if(EXPECT_TRUE( ! nvIsAllocated() )) {
+  if(__builtin_expect( ( ! nvIsAllocated() ), true )) {
     /** Case 1.  d_nv points to d_inlineNv: it is the backing store
      ** allocated "inline" in this NodeBuilder. **/
 
@@ -1177,7 +1177,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
   // NodeManager pool of Nodes.  See implementation notes at the top
   // of this file.
 
-  if(EXPECT_TRUE( ! nvIsAllocated() )) {
+  if(__builtin_expect( ( ! nvIsAllocated() ), true )) {
     /** Case 1.  d_nv points to d_inlineNv: it is the backing store
      ** allocated "inline" in this NodeBuilder. **/
 

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 13fdc6a7f14b6580606cadca0f0bca0b365a15be..56ac70c1e28dbb4bbbc27b57c5a68f9567922c62 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -299,7 +299,7 @@ private:
     RefCountGuard(const NodeValue* nv) :
       d_nv(const_cast<NodeValue*>(nv)) {
       // inc()
-      if(EXPECT_TRUE( d_nv->d_rc < MAX_RC )) {
+      if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) {
         ++d_nv->d_rc;
       }
     }
@@ -309,7 +309,7 @@ private:
       // E.g., this can happen when debugging code calls the print
       // routines below.  As RefCountGuards are scoped on the stack,
       // this should be fine---but not in multithreaded contexts!
-      if(EXPECT_TRUE( d_nv->d_rc < MAX_RC )) {
+      if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) {
         --d_nv->d_rc;
       }
     }
@@ -400,16 +400,16 @@ inline void NodeValue::inc() {
          "NodeValue is currently being deleted "
          "and increment is being called on it. Don't Do That!");
   // FIXME multithreading
-  if(EXPECT_TRUE( d_rc < MAX_RC )) {
+  if(__builtin_expect( ( d_rc < MAX_RC ), true )) {
     ++d_rc;
   }
 }
 
 inline void NodeValue::dec() {
   // FIXME multithreading
-  if(EXPECT_TRUE( d_rc < MAX_RC )) {
+  if(__builtin_expect( ( d_rc < MAX_RC ), true )) {
     --d_rc;
-    if(EXPECT_FALSE( d_rc == 0 )) {
+    if(__builtin_expect( ( d_rc == 0 ), false )) {
       Assert(NodeManager::currentNM() != NULL,
              "No current NodeManager on destruction of NodeValue: "
              "maybe a public CVC4 interface function is missing a NodeManagerScope ?");

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 1d4c330fac4df41890019709a3c97648ed1896d9..2fc38022435fc31396b5fd5fde674a12aec1f6eb 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -300,7 +300,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
   Assert(!t0.isNull());
   Assert(!t1.isNull());
 
-  if(EXPECT_TRUE(t0 == t1)) {
+  if(__builtin_expect( (t0 == t1), true )) {
     return t0;
   } else { // t0 != t1
     if(t0.getKind()== kind::TYPE_CONSTANT) {

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 35d630a91dcc15cfaabc8a2d458aca62c4f8f9c3..061e73fc92826d8b07b7502df5bf2b2d27d6641d 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -770,7 +770,7 @@ inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   Assert(typeNode.d_nv != NULL,
          "Expecting a non-NULL expression value on RHS!");
-  if(EXPECT_TRUE( d_nv != typeNode.d_nv )) {
+  if(__builtin_expect( ( d_nv != typeNode.d_nv ), true )) {
     d_nv->dec();
     d_nv = typeNode.d_nv;
     d_nv->inc();

diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index b8c30aeef1cf813c4b66d65e692a8f05b6c14f47..b7431ce1ca9c77bae600e10b95e7c2faae8fbb51 100644 (file)
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -68,7 +68,4 @@
 #  define CVC4_WARN_UNUSED_RESULT
 #endif /* __GNUC__ */
 
-#define EXPECT_TRUE(x) __builtin_expect( (x), true )
-#define EXPECT_FALSE(x) __builtin_expect( (x), false )
-
 #endif /* __CVC4_PUBLIC_H */

diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 88a7c64632aee6a57bb05500d9272c595bf7573e..112d9b0edc37b2dcc0276378315d225d1c97893a 100644 (file)
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -241,7 +241,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) {
   }
 
   /* Initialize the buffer on our first call. */
-  if( EXPECT_FALSE(buffer->empty == ANTLR3_TRUE) ) {
+  if( __builtin_expect( (buffer->empty == ANTLR3_TRUE), false ) ) {
     assert( buffer->tokenBuffer != NULL );
     buffer->tokenBuffer[ 0 ] = nextToken(buffer);
     buffer->maxIndex = 0;

diff --git a/src/util/cvc4_assert.cpp b/src/util/cvc4_assert.cpp
index eb7b81a392086dfb660070164df9808bb353b6b9..08e2867f6ffca14ab37581525db1ca72d664abfc 100644 (file)
--- a/src/util/cvc4_assert.cpp
+++ b/src/util/cvc4_assert.cpp
@@ -136,7 +136,7 @@ void debugAssertionFailed(const AssertionException& thisException,
                           const char* propagatingException) {
   static CVC4_THREADLOCAL(bool) alreadyFired = false;
 
-  if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) {
+  if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
     throw thisException;
   }
 

diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h
index c070fc38993bf74b56239d17820acd84978189b3..7d359a56bff8c4b7b817adc8b275cbdfa72dbd4b 100644 (file)
--- a/src/util/cvc4_assert.h
+++ b/src/util/cvc4_assert.h
@@ -252,7 +252,7 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 // details of the exception
 #  define AlwaysAssert(cond, msg...)                                    \
     do {                                                                \
-      if(EXPECT_FALSE( ! (cond) )) {                                    \
+      if(__builtin_expect( ( ! (cond) ), false )) {                                    \
         /* save the last assertion failure */                           \
         const char* lastException = ::CVC4::s_debugLastException;       \
         ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
@@ -265,7 +265,7 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 // will terminate() if thrown during stack unwinding.
 #  define AlwaysAssert(cond, msg...)                                    \
      do {                                                               \
-       if(EXPECT_FALSE( ! (cond) )) {                                   \
+       if(__builtin_expect( ( ! (cond) ), false )) {                                   \
          throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
        }                                                                \
      } while(0)
@@ -283,13 +283,13 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
   throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
 #define CheckArgument(cond, arg, msg...)         \
   do { \
-    if(EXPECT_FALSE( ! (cond) )) { \
+    if(__builtin_expect( ( ! (cond) ), false )) { \
       throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
     } \
   } while(0)
 #define AlwaysAssertArgument(cond, arg, msg...)  \
   do { \
-    if(EXPECT_FALSE( ! (cond) )) { \
+    if(__builtin_expect( ( ! (cond) ), false )) { \
       throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
     } \
   } while(0)
@@ -299,9 +299,9 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 #  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
 #  define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg)
 #else /* ! CVC4_ASSERTIONS */
-#  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
-#  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
-#  define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
+#  define Assert(cond, msg...) /*__builtin_expect( ( cond ), true )*/
+#  define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
+#  define DebugCheckArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
 #endif /* CVC4_ASSERTIONS */
 
 }/* CVC4 namespace */

diff --git a/src/util/debug.h b/src/util/debug.h
index 3e7c4d8be7a84f369046669ba96dfbfb4213983e..97c176f02b624d7711c69404061aa2cd74b08a18 100644 (file)
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -27,11 +27,11 @@
 
 #ifdef CVC4_ASSERTIONS
 // the __builtin_expect() helps us if assert is built-in or a macro
-#  define cvc4assert(x) assert(EXPECT_TRUE( x ))
+#  define cvc4assert(x) assert(__builtin_expect( ( x ), true ))
 #else
 // TODO: use a compiler annotation when assertions are off ?
 // (to improve optimization)
-#  define cvc4assert(x) /*EXPECT_TRUE( x )*/
+#  define cvc4assert(x) /*__builtin_expect( ( x ), true )*/
 #endif /* CVC4_ASSERTIONS */
 
 #endif /* __CVC4__DEBUG_H */

diff --git a/src/util/exception.h b/src/util/exception.h
index 082a50ef272103159d9097ded837fc8d13b12803..cd4b763ef5d6966659e9dcf65801e47c7ab5bbe4 100644 (file)
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -138,13 +138,13 @@ namespace CVC4 {
 #ifndef CheckArgument
 template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
 template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
 template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
 template <class T> inline void CheckArgument(bool cond, const T& arg) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
@@ -153,13 +153,13 @@ template <class T> inline void CheckArgument(bool cond, const T& arg) {
 #ifndef DebugCheckArgument
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }