From: Tim King Date: Mon, 17 Jul 2017 05:13:10 +0000 (-0700) Subject: Moving to static_assert now that c++11 is available. X-Git-Tag: cvc5-1.0.0~5717 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=949e19cbc2881996e5c5eed613f4506264482039;p=cvc5.git Moving to static_assert now that c++11 is available. --- 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 #include #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 #include #include #include @@ -383,9 +382,8 @@ public: } };/* class CDInsertHashMap<> */ - template -class CDInsertHashMap : public ContextObj { +class CDInsertHashMap : public ContextObj { /* CDInsertHashMap is challenging to get working with TNode. * Consider using CDHashMap instead. * @@ -397,7 +395,8 @@ class CDInsertHashMap : 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 #include #include #include @@ -417,21 +416,21 @@ public: } };/* class CDList<> */ - template -class CDList > : public ContextObj { +class CDList > : public ContextObj { /* CDList is incompatible for use with a ContextMemoryAllocator. * Consider using CDChunkList 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 #include #include #include @@ -551,7 +550,7 @@ public: };/* class CDTrailHashMap<> */ template -class CDTrailHashMap : public ContextObj { +class CDTrailHashMap : public ContextObj { /* CDTrailHashMap is challenging to get working with TNode. * Consider using CDHashMap instead. * @@ -563,7 +562,8 @@ class CDTrailHashMap : 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 +#include + +namespace CVC4 { + +static_assert(sizeof(Index) <= sizeof(size_t), + "Index cannot be larger than size_t"); +static_assert(!std::numeric_limits::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 -#include -#include +#include 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::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 */