diff options
Diffstat (limited to 'src/util/index.h')
-rw-r--r-- | src/util/index.h | 34 |
1 files changed, 9 insertions, 25 deletions
diff --git a/src/util/index.h b/src/util/index.h index a8910a696..7329e3f8d 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -9,39 +9,23 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Standardized type for efficient array indexing. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Standardized type for efficient array indexing. **/ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__INDEX_H +#define __CVC4__INDEX_H -#include <stdint.h> -#include <boost/static_assert.hpp> -#include <limits> +#include <cstdint> namespace CVC4 { -/** - * Index is an unsigned integer used for array indexing. - * - * This gives a standardized type for independent pieces of code to use as an agreement. - */ -typedef uint32_t Index; - -BOOST_STATIC_ASSERT(sizeof(Index) <= sizeof(size_t)); -BOOST_STATIC_ASSERT(!std::numeric_limits<Index>::is_signed); - -/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)? - * - * size_t is a more appropriate choice than uint32_t as the choice is dictated by - * uniqueness in arrays and vectors. These correspond to size_t. - * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticeably - * slower. (Limited testing suggests a ~1/16 of running time.) - * (Interestingly, uint_fast32_t also has a sizeof == 8 on x86_64. Filthy Liars!) - */ +/** Index is a standardized unsigned integer used for efficient indexing. */ +using Index = uint32_t; }/* CVC4 namespace */ + +#endif /* __CVC4__INDEX_H */ |