src/util/debug.h

   1 /*********************                                                        */
   2 /*! \file debug.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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 */