Merge branch 'master' into cleanup-regexp

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 */