// 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"
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)
{
} // namespace hashsmt
+#endif /* __CVC4__EXAMPLES__HASHSMT__SHA1_H */
#include "cvc4_private.h"
-#include <boost/static_assert.hpp>
#include <deque>
#include <ext/hash_map>
#include <utility>
}
};/* 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.
*
* 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 */
#ifndef __CVC4__CONTEXT__CDLIST_H
#define __CVC4__CONTEXT__CDLIST_H
-#include <boost/static_assert.hpp>
#include <iterator>
#include <memory>
#include <string>
}
};/* 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 */
#pragma once
-#include <boost/static_assert.hpp>
#include <ext/hash_map>
#include <deque>
#include <utility>
};/* 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.
*
* 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 */
floatingpoint.h \
gmp_util.h \
hash.h \
+ index.cpp \
index.h \
maybe.h \
ntuple.h \
--- /dev/null
+#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 */
** 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 */
projects / cvc5.git / commitdiff