diff --git a/RELEASE_NOTES b/RELEASE_NOTES index d93a13129..01f9e687e 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -11,7 +11,7 @@ Version 4.4 - Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one. -- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, and Codeplex users rsas, clockish, Heizmann. +- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, and Stackoverflow users user297886. Version 4.3.2 diff --git a/scripts/mk_util.py b/scripts/mk_util.py index fbec2cf06..0f4fdb216 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1376,6 +1376,7 @@ class MLComponent(Component): sub_dir = os.path.join('api', 'ml') mk_dir(os.path.join(BUILD_DIR, sub_dir)) api_src = get_component(API_COMPONENT).to_src_dir + out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it. for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)): out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f))) str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f)) @@ -1412,7 +1413,7 @@ class MLComponent(Component): (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'), os.path.join(sub_dir, 'z3native_stubs.c'), get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)')); - out.write('\t$(CC) $(CXXFLAGS) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' % + out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' % (OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs'))) out.write('%s: %s %s %s$(SO_EXT)' % ( @@ -1709,39 +1710,39 @@ def mk_config(): extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) if DEBUG_MODE: config.write( - 'LINK_FLAGS=/nologo /MDd /LTCG\n' - 'SLINK_FLAGS=/nologo /LDd /LTCG\n') + 'LINK_FLAGS=/nologo /MDd\n' + 'SLINK_FLAGS=/nologo /LDd\n') if not VS_X64: config.write( 'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' + 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: config.write( 'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' + 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: # Windows Release mode config.write( - 'LINK_FLAGS=/nologo /MD /LTCG\n' - 'SLINK_FLAGS=/nologo /LD /LTCG\n') + 'LINK_FLAGS=/nologo /MD\n' + 'SLINK_FLAGS=/nologo /LD\n') if TRACE: extra_opt = '%s /D _TRACE' % extra_opt if not VS_X64: config.write( 'CXXFLAGS=/nologo /c /GL /Zi /openmp /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' + 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: config.write( 'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt) config.write( - 'LINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' - 'SLINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n') + 'LINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' + 'SLINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n') # End of Windows VS config.mk if is_verbose(): diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 3a95fb730..33d7a3eab 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -39,7 +39,7 @@ def mk_dir(d): os.makedirs(d) def set_build_dir(path): - global BUILD_DIR + global BUILD_DIR, BUILD_X86_DIR, BUILD_X64_DIR BUILD_DIR = path BUILD_X86_DIR = os.path.join(path, 'x86') BUILD_X64_DIR = os.path.join(path, 'x64') diff --git a/scripts/update_api.py b/scripts/update_api.py index 889044d1f..93800237e 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -642,6 +642,7 @@ def mk_java(): java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('extern "C" {\n') java_wrapper.write('#endif\n\n') + java_wrapper.write('#ifdef __GNUC__\n#if __GNUC__ >= 4\n#define DLL_VIS __attribute__ ((visibility ("default")))\n#else\n#define DLL_VIS\n#endif\n#else\n#define DLL_VIS\n#endif\n\n') java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n') @@ -688,13 +689,13 @@ def mk_java(): java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') java_wrapper.write(' // wrappers below.\n') java_wrapper.write('}\n\n') - java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str) + java_wrapper.write('DLL_VIS JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str) java_wrapper.write('{\n') java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n') java_wrapper.write('}\n\n') java_wrapper.write('') for name, result, params in _dotnet_decls: - java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) + java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) i = 0; for param in params: java_wrapper.write(', ') diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index ae4c657bd..9110014bf 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -276,8 +276,8 @@ expr * func_interp::get_interp() const { return r; } -func_interp * func_interp::translate(ast_translation & translator) const { - func_interp * new_fi = alloc(func_interp, m_manager, m_arity); +func_interp * func_interp::translate(ast_translation & translator) const { + func_interp * new_fi = alloc(func_interp, translator.to(), m_arity); ptr_vector::const_iterator it = m_entries.begin(); ptr_vector::const_iterator end = m_entries.end(); diff --git a/src/model/model.cpp b/src/model/model.cpp index a6b9695b4..73a39a8eb 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -74,6 +74,7 @@ void model::register_decl(func_decl * d, expr * v) { void model::register_decl(func_decl * d, func_interp * fi) { SASSERT(d->get_arity() > 0); + SASSERT(&fi->m() == &m_manager); decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0); if (entry->get_data().m_value == 0) { // new entry diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 2a64c9cd5..72f1d5770 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -89,7 +89,7 @@ namespace sat { clause_vector m_learned; unsigned m_num_frozen; vector m_watches; - svector m_assignment; + char_vector m_assignment; svector m_justification; svector m_decision; svector m_mark; @@ -200,8 +200,8 @@ namespace sat { bool is_external(bool_var v) const { return m_external[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } unsigned scope_lvl() const { return m_scope_lvl; } - lbool value(literal l) const { return m_assignment[l.index()]; } - lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; } + lbool value(literal l) const { return static_cast(m_assignment[l.index()]); } + lbool value(bool_var v) const { return static_cast(m_assignment[literal(v, false).index()]); } unsigned lvl(bool_var v) const { return m_level[v]; } unsigned lvl(literal l) const { return m_level[l.var()]; } void assign(literal l, justification j) { diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index 2e94c376d..c559e2b9b 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -17,16 +17,14 @@ Revision History: --*/ #include"dyn_ack_params.h" +#include"smt_params_helper.hpp" -#if 0 -void dyn_ack_params::register_params(ini_params & p) { - p.register_int_param("dack", 0, 2, reinterpret_cast(m_dack), - "0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution."); - p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities"); - p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded"); - p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict"); - p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict)."); - p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay); -} -#endif - +void dyn_ack_params::updt_params(params_ref const & _p) { + smt_params_helper p(_p); + m_dack = static_cast(p.dack()); + m_dack_eq = p.dack_eq(); + m_dack_factor = p.dack_factor(); + m_dack_threshold = p.dack_threshold(); + m_dack_gc = p.dack_gc(); + m_dack_gc_inv_decay = p.dack_gc_inv_decay(); +} \ No newline at end of file diff --git a/src/smt/params/dyn_ack_params.h b/src/smt/params/dyn_ack_params.h index 9f7ce578c..95b5aff8a 100644 --- a/src/smt/params/dyn_ack_params.h +++ b/src/smt/params/dyn_ack_params.h @@ -19,6 +19,8 @@ Revision History: #ifndef _DYN_ACK_PARAMS_H_ #define _DYN_ACK_PARAMS_H_ +#include"params.h" + enum dyn_ack_strategy { DACK_DISABLED, DACK_ROOT, // congruence is the root of the conflict @@ -34,15 +36,17 @@ struct dyn_ack_params { double m_dack_gc_inv_decay; public: - dyn_ack_params(): + dyn_ack_params(params_ref const & p = params_ref()) : m_dack(DACK_ROOT), m_dack_eq(false), m_dack_factor(0.1), m_dack_threshold(10), m_dack_gc(2000), m_dack_gc_inv_decay(0.8) { + updt_params(p); } + void updt_params(params_ref const & _p); }; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 18619c8ec..2f8d9c1ee 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -46,6 +46,7 @@ void smt_params::updt_local_params(params_ref const & _p) { void smt_params::updt_params(params_ref const & p) { preprocessor_params::updt_params(p); + dyn_ack_params::updt_params(p); qi_params::updt_params(p); theory_arith_params::updt_params(p); theory_bv_params::updt_params(p); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 869b8cdc4..39818e621 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -45,5 +45,11 @@ def_module_params(module_name='smt', ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), ('array.weak', BOOL, False, 'weak array theory'), - ('array.extensional', BOOL, True, 'extensional array theory') + ('array.extensional', BOOL, True, 'extensional array theory'), + ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), + ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'), + ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'), + ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), + ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), + ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded') )) diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index 1490b9628..c41e4574c 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -25,13 +25,11 @@ Revision History: #define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1) void bit_vector::expand_to(unsigned new_capacity) { - unsigned * new_data = alloc_svect(unsigned, new_capacity); - memset(new_data, 0, new_capacity * sizeof(unsigned)); - if (m_capacity > 0) { - memcpy(new_data, m_data, m_capacity * sizeof(unsigned)); - dealloc_svect(m_data); + if (m_data) { + m_data = (unsigned*)memory::reallocate(m_data, new_capacity * sizeof(unsigned)); + } else { + m_data = alloc_svect(unsigned, new_capacity); } - m_data = new_data; m_capacity = new_capacity; } diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 0ccdeae9e..6738ba0aa 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -87,9 +87,7 @@ public: } ~bit_vector() { - if (m_data) { - dealloc_svect(m_data); - } + dealloc_svect(m_data); } void reset() { diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 354a11aeb..e911ff505 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -252,6 +252,24 @@ void * memory::allocate(size_t s) { return static_cast(r) + 1; // we return a pointer to the location after the extra field } +void* memory::reallocate(void *p, size_t s) { + size_t *sz_p = reinterpret_cast(p)-1; + size_t sz = *sz_p; + void *real_p = reinterpret_cast(sz_p); + s = s + sizeof(size_t); // we allocate an extra field! + + g_memory_thread_alloc_size += s - sz; + if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) { + synchronize_counters(true); + } + + void *r = realloc(real_p, s); + if (r == 0) + throw_out_of_memory(); + *(static_cast(r)) = s; + return static_cast(r) + 1; // we return a pointer to the location after the extra field +} + #else // ================================== // ================================== @@ -292,5 +310,29 @@ void * memory::allocate(size_t s) { *(static_cast(r)) = s; return static_cast(r) + 1; // we return a pointer to the location after the extra field } + +void* memory::reallocate(void *p, size_t s) { + size_t * sz_p = reinterpret_cast(p) - 1; + size_t sz = *sz_p; + void * real_p = reinterpret_cast(sz_p); + s = s + sizeof(size_t); // we allocate an extra field! + bool out_of_mem = false; + #pragma omp critical (z3_memory_manager) + { + g_memory_alloc_size += s - sz; + if (g_memory_alloc_size > g_memory_max_used_size) + g_memory_max_used_size = g_memory_alloc_size; + if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size) + out_of_mem = true; + } + if (out_of_mem) + throw_out_of_memory(); + + void *r = realloc(real_p, s); + if (r == 0) + throw_out_of_memory(); + *(static_cast(r)) = s; + return static_cast(r) + 1; // we return a pointer to the location after the extra field +} #endif diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index aaf8b2825..bd912828e 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -34,7 +34,7 @@ Revision History: # define GCC_RET_NON_NULL # endif # define ALLOC_ATTR __attribute__((malloc)) GCC_RET_NON_NULL -#elif defined(_WINDOWS) && (VisualStudioVersion >= 13) +#elif defined(_WINDOWS) # define ALLOC_ATTR __declspec(restrict) #else # define ALLOC_ATTR @@ -57,10 +57,11 @@ public: static void display_max_usage(std::ostream& os); static void display_i_max_usage(std::ostream& os); static void deallocate(void* p); - static void* allocate(size_t s) ALLOC_ATTR; + static ALLOC_ATTR void* allocate(size_t s); + static ALLOC_ATTR void* reallocate(void *p, size_t s); #if _DEBUG static void deallocate(char const* file, int line, void* p); - static void* allocate(char const* file, int line, char const* obj, size_t s) ALLOC_ATTR; + static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s); #endif static unsigned long long get_allocation_size(); static unsigned long long get_max_used_memory(); @@ -95,7 +96,7 @@ void dealloc(T * ptr) { #endif template -T * alloc_vect(unsigned sz) ALLOC_ATTR; +ALLOC_ATTR T * alloc_vect(unsigned sz); template T * alloc_vect(unsigned sz) { diff --git a/src/util/vector.h b/src/util/vector.h index 9370a4eed..dc08a63b3 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -71,18 +71,12 @@ class vector { SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; SZ new_capacity = (3 * old_capacity + 1) >> 1; SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2; - SZ size = reinterpret_cast(m_data)[SIZE_IDX]; if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { throw default_exception("Overflow encountered when expanding vector"); } - SZ * mem = reinterpret_cast(memory::allocate(new_capacity_T)); - *mem = new_capacity; - mem ++; - *mem = size; - mem++; - memcpy(mem, m_data, size * sizeof(T)); - free_memory(); - m_data = reinterpret_cast(mem); + SZ *mem = (SZ*)memory::reallocate(reinterpret_cast(m_data)-2, new_capacity_T); + *mem = new_capacity; + m_data = reinterpret_cast(mem + 2); } }