diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/index.cpp | 21 | ||||
-rw-r--r-- | src/util/index.h | 34 |
3 files changed, 31 insertions, 25 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index cd6f0e11c..877525de7 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -34,6 +34,7 @@ libutil_la_SOURCES = \ floatingpoint.h \ gmp_util.h \ hash.h \ + index.cpp \ index.h \ maybe.h \ ntuple.h \ diff --git a/src/util/index.cpp b/src/util/index.cpp new file mode 100644 index 000000000..bd15e2d80 --- /dev/null +++ b/src/util/index.cpp @@ -0,0 +1,21 @@ +#include "util/index.h" + +#include <cstddef> +#include <limits> + +namespace CVC4 { + +static_assert(sizeof(Index) <= sizeof(size_t), + "Index cannot be larger than size_t"); +static_assert(!std::numeric_limits<Index>::is_signed, + "Index must be unsigned"); + +/* 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. + */ +}/* CVC4 namespace */ 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 */ |