Moving to static_assert now that c++11 is available.

7 files changed, 52 insertions, 45 deletions

diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp
index 4bfee50fc..72c560dff 100644
--- a/examples/hashsmt/sha1.hpp
+++ b/examples/hashsmt/sha1.hpp
@@ -30,9 +30,9 @@
 // Note: this implementation does not handle message longer than
 //       2^32 bytes.
 
-#pragma once 
+#ifndef __CVC4__EXAMPLES__HASHSMT__SHA1_H
+#define __CVC4__EXAMPLES__HASHSMT__SHA1_H
 
-#include <boost/static_assert.hpp>
 #include <cstddef>
 
 #include "word.h"
@@ -45,8 +45,10 @@ namespace std {
 
 namespace hashsmt {
 
-BOOST_STATIC_ASSERT(sizeof(unsigned char)*8 == 8);
-BOOST_STATIC_ASSERT(sizeof(unsigned int)*8 == 32);
+static_assert(sizeof(unsigned char)*8 == 8,
+              "Unexpected size for unsigned char");
+static_assert(sizeof(unsigned int)*8 == 32,
+              "Unexpected size for unsigned int");
 
 inline cvc4_uint32 left_rotate(cvc4_uint32 x, std::size_t n)
 {
@@ -224,3 +226,4 @@ inline void sha1::get_digest(digest_type digest)
 
 } // namespace hashsmt
 
+#endif /* __CVC4__EXAMPLES__HASHSMT__SHA1_H */
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index f53d60cf9..ef8f661fa 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -33,7 +33,6 @@
 
 #include "cvc4_private.h"
 
-#include <boost/static_assert.hpp>
 #include <deque>
 #include <ext/hash_map>
 #include <utility>
@@ -383,9 +382,8 @@ public:
   }
 };/* class CDInsertHashMap<> */
 
-
 template <class Data, class HashFcn>
-class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
+class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj {
   /* CDInsertHashMap is challenging to get working with TNode.
    * Consider using CDHashMap<TNode,...> instead.
    *
@@ -397,7 +395,8 @@ class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
    * hashed. Getting the order right with a guarantee is too hard.
    */
 
-  BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+  static_assert(sizeof(Data) == 0,
+                "Cannot create a CDInsertHashMap with TNode keys");
 };
 
 }/* CVC4::context namespace */
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 7cee41b91..3dab675c3 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -20,7 +20,6 @@
 #ifndef __CVC4__CONTEXT__CDLIST_H
 #define __CVC4__CONTEXT__CDLIST_H
 
-#include <boost/static_assert.hpp>
 #include <iterator>
 #include <memory>
 #include <string>
@@ -417,21 +416,21 @@ public:
   }
 };/* class CDList<> */
 
-
 template <class T, class CleanUp>
-class CDList <T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
+class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
   /* CDList is incompatible for use with a ContextMemoryAllocator.
    * Consider using CDChunkList<T> instead.
    *
    * Explanation:
-   * If ContextMemoryAllocator is used and d_list grows at a deeper context level
-   * the reallocated will be reallocated in a context memory region that can be
-   * destroyed on pop. To support this, a full copy of d_list would have to be made.
-   * As this is unacceptable for performance in other situations, we do not do
-   * this.
+   * If ContextMemoryAllocator is used and d_list grows at a deeper context
+   * level the reallocated will be reallocated in a context memory region that
+   * can be destroyed on pop. To support this, a full copy of d_list would have
+   * to be made. As this is unacceptable for performance in other situations, we
+   * do not do this.
    */
 
-  BOOST_STATIC_ASSERT(sizeof(T) == 0);
+  static_assert(sizeof(T) == 0,
+                "Cannot create a CDList with a ContextMemoryAllocator.");
 };
 
 }/* CVC4::context namespace */
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index 9f364eac5..0d265271d 100644
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -44,7 +44,6 @@
 
 #pragma once
 
-#include <boost/static_assert.hpp>
 #include <ext/hash_map>
 #include <deque>
 #include <utility>
@@ -551,7 +550,7 @@ public:
 };/* class CDTrailHashMap<> */
 
 template <class Data, class HashFcn>
-class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
+class CDTrailHashMap<TNode, Data, HashFcn> : public ContextObj {
   /* CDTrailHashMap is challenging to get working with TNode.
    * Consider using CDHashMap<TNode,...> instead.
    *
@@ -563,7 +562,8 @@ class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
    * hashed. Getting the order right with a guarantee is too hard.
    */
 
-  BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+  static_assert(sizeof(Data) == 0,
+                "Cannot create a CDTrailHashMap with TNode keys");
 };
 
 }/* CVC4::context namespace */
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 */