src/util/debug.h

   1 /*********************                                                        */
   2 /*! \file debug.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Debugging things.
  13  **
  14  ** Debugging things.
  15  **
  16  ** These are low-level assertions!  Generally you should use
  17  ** CVC4::Assert() instead (they throw an exception!).  See
  18  ** util/Assert.h.
  19  **/
  20
  21 #include "cvc4_private.h"
  22
  23 #ifndef CVC4__DEBUG_H
  24 #define CVC4__DEBUG_H
  25
  26 #include <cassert>
  27
  28 #ifdef CVC4_ASSERTIONS
  29 // the __builtin_expect() helps us if assert is built-in or a macro
  30 #  define cvc4assert(x) assert(__builtin_expect( ( x ), true ))
  31 #else
  32 // TODO: use a compiler annotation when assertions are off ?
  33 // (to improve optimization)
  34 #  define cvc4assert(x) /*__builtin_expect( ( x ), true )*/
  35 #endif /* CVC4_ASSERTIONS */
  36
  37 #endif /* CVC4__DEBUG_H */