Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/util/debug.h

@@ -98,6 +98,9 @@ private:
 };
 
 void finalize_debug();
+/*
+  ADD_FINALIZER('finalize_debug();')
+*/
 
 #endif /* _DEBUG_H_ */
 

src/util/mem_stat.cpp

@@ -1,56 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    mem_stat.cpp
-
-Abstract:
-
-    Memory usage statistics
-
-Author:
-
-    Leonardo de Moura (leonardo) 2006-11-09.
-
-Revision History:
-
---*/
-
-#ifdef _WINDOWS
-#include<windows.h>
-#include<cstdio>
-#include<psapi.h>
-
-double get_max_heap_size() {
-    DWORD processID = GetCurrentProcessId();
-    HANDLE hProcess;
-    PROCESS_MEMORY_COUNTERS pmc;
-    
-    hProcess = OpenProcess(PROCESS_QUERY_INFORMATION |
-                           PROCESS_VM_READ,
-                           FALSE, processID);
-    double result = -1.0;
-
-    if (NULL == hProcess) {
-        return -1.0;
-    }
-    
-    if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
-        result = static_cast<double>(pmc.PeakWorkingSetSize) / static_cast<double>(1024*1024);
-    }
-
-    CloseHandle( hProcess );
-
-    return result;
-}
-
-#else
-
-double get_max_heap_size() {
-    // not available in this platform
-    return -1.0;
-}
-
-#endif
-

src/util/mem_stat.h

@@ -1,25 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    mem_stat.h
-
-Abstract:
-
-    Memory usage statistics
-
-Author:
-
-    Leonardo de Moura (leonardo) 2006-11-09.
-
-Revision History:
-
---*/
-#ifndef _MEM_STAT_H_
-#define _MEM_STAT_H_
-
-double get_max_heap_size();
-
-#endif /* _MEM_STAT_H_ */
-

src/util/memory_manager.cpp

@@ -1,13 +1,27 @@
+#include<iostream>
 #include<stdlib.h>
+#include"trace.h"
 #include"memory_manager.h"
-#include"rational.h"
-#include"prime_generator.h"
-#include"debug.h"
+#include"error_codes.h"
+
+// The following two function are automatically generated by the mk_make.py script.
+// The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
+// For example, rational.h contains
+//      ADD_INITIALIZER('rational::initialize();')
+//      ADD_FINALIZER('rational::finalize();')
+// Thus, any executable or shared object (DLL) that depends on rational.h
+// will have an automalically generated file mem_initializer.cpp containing
+//    mem_initialize() 
+//    mem_finalize()
+// and these functions will include the statements:
+//    rational::initialize();
+//    
+//    rational::finalize();
+void mem_initialize();
+void mem_finalize();
 
 // If PROFILE_MEMORY is defined, Z3 will display the amount of memory used, and the number of synchronization steps during finalization
 // #define PROFILE_MEMORY
-void initialize_symbols();
-void finalize_symbols();
 
 out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
 }
@@ -58,8 +72,7 @@ mem_usage_report g_info;
 void memory::initialize(size_t max_size) {
     g_memory_out_of_memory  = false;
     g_memory_max_size       = max_size;
-    rational::initialize();
-    initialize_symbols();
+    mem_initialize();
 }
 
 bool memory::is_out_of_memory() {
@@ -96,14 +109,9 @@ static bool g_finalizing = false;
 
 void memory::finalize() {
     g_finalizing = true;
-    finalize_debug();
-    finalize_trace();
-    finalize_symbols();
-    rational::finalize();
-    prime_iterator::finalize();
+    mem_finalize();
 }
 
-
 unsigned long long memory::get_allocation_size() {
     long long r;
     #pragma omp critical (z3_memory_manager) 

src/util/prime_generator.h

@@ -48,6 +48,9 @@ public:
     prime_iterator(prime_generator * g = 0);
     uint64 next();
     static void finalize();
+    /*
+      ADD_FINALIZER('prime_iterator::finalize();')
+    */
 };
 
 #endif

src/util/rational.h

@@ -35,7 +35,10 @@ public:
     static void initialize();
 
     static void finalize();
-
+    /*
+      ADD_INITIALIZER('rational::initialize();')
+      ADD_FINALIZER('rational::finalize();')
+    */
     rational() {}
     
     rational(rational const & r) { m().set(m_val, r.m_val); }

src/util/symbol.h

@@ -141,6 +141,10 @@ struct symbol_eq_proc {
 
 void initialize_symbols();
 void finalize_symbols();
+/*
+  ADD_INITIALIZER('initialize_symbols();')
+  ADD_FINALIZER('finalize_symbols();')
+*/
 
 // total order on symbols... I did not overloaded '<' to avoid misunderstandings.
 // numerical symbols are smaller than non numerical symbols.

src/util/trace.h

@@ -40,6 +40,9 @@ bool is_trace_enabled(const char * tag);
 void close_trace();
 void open_trace();
 void finalize_trace();
+/*
+  ADD_FINALIZER('finalize_trace();')
+*/
 
 #define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })