mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
port over std_vector and std-allocator functionality from monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
aaa587398e
commit
6559e5fb32
|
@ -128,6 +128,29 @@ void dealloc_svect(T * ptr) {
|
|||
memory::deallocate(ptr);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
struct std_allocator {
|
||||
using value_type = T;
|
||||
// the constructors must be provided according to cpp docs
|
||||
std_allocator() = default;
|
||||
template <class U> constexpr std_allocator(const std_allocator<U>&) noexcept {}
|
||||
|
||||
|
||||
T* allocate(std::size_t n) {
|
||||
return static_cast<T*>(memory::allocate(n * sizeof(T)));
|
||||
}
|
||||
|
||||
void deallocate(T* p, std::size_t n) {
|
||||
memory::deallocate(p);
|
||||
}
|
||||
};
|
||||
|
||||
// the comparison operators must be provided according to cpp docs
|
||||
template <class T, class U>
|
||||
bool operator==(const std_allocator<T>&, const std_allocator<U>&) { return true; }
|
||||
template <class T, class U>
|
||||
bool operator!=(const std_allocator<T>&, const std_allocator<U>&) { return false; }
|
||||
|
||||
struct mem_stat {
|
||||
};
|
||||
|
||||
|
|
|
@ -33,6 +33,7 @@ Revision History:
|
|||
#include "util/memory_manager.h"
|
||||
#include "util/hash.h"
|
||||
#include "util/z3_exception.h"
|
||||
#include <vector>
|
||||
|
||||
// disable warning for constant 'if' expressions.
|
||||
// these are used heavily in templates.
|
||||
|
@ -40,6 +41,8 @@ Revision History:
|
|||
#pragma warning(disable:4127)
|
||||
#endif
|
||||
|
||||
template <typename T>
|
||||
using std_vector = std::vector<T, std_allocator<T>>;
|
||||
|
||||
#if 0
|
||||
|
||||
|
|
Loading…
Reference in a new issue