From 6cf76f2113b5ea8442156c3e4097f378f82446a5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 29 Feb 2016 20:23:20 -0800
Subject: [PATCH] remove references to _DEBUG use Z3DEBUG instead

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/automata/symbolic_automata_def.h | 23 ++++++++++++-----------
 src/muz/rel/dl_base.h                     |  4 ----
 src/util/memory_manager.cpp               |  2 +-
 src/util/memory_manager.h                 |  2 +-
 4 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index db6172d49..213a4b2f9 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -75,23 +75,24 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
         return 0;
     }
     
-    block final_block(fa->final_states());
-    block non_final_block(fa->non_final_states());
-    vector<block> blocks;
+    vector<block> pblocks;
+    unsigned_vector blocks;
+    pblocks.push_back(block(fa->final_states()));     // 0 |-> final states
+    pblocks.push_back(block(fa->non_final_states());  // 1 |-> non-final states
     for (unsigned i = 0; i < fa->num_states(); ++i) {
-        if (fa->is_final_state(i)) {
-            blocks.push_back(final_block);
+        if (fa->is_final_state(i)) {            
+            blocks.push_back(0);
         }
         else {
-            blocks.push_back(non_final_block);
+            blocks.push_back(1);
         }
     }
     vector<block> W;
     if (final_block.size() > non_final_block.size()) {
-        W.push_back(non_final_block);
+        W.push_back(1);
     }
     else {
-        W.push_back(final_block);
+        W.push_back(0);
     }
     
 #if 0
@@ -111,7 +112,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
             fa->get_moves_to(q, mvs);
             for (unsigned i = 0; i < mvs.size(); ++i) {
                 unsigned src = mvs[i].src();
-                if (blocks[src].size() > 1) {
+                if (pblocks[src].size() > 1) {
                     T* t = mvs[i]();
                     if (gamma.find(src, t1)) {
                         t = m_ba.mk_or(t, t1);
@@ -121,10 +122,10 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
                 }
             }
         }
-        hashtable<block*> relevant;
+        uint_set relevant;
         u_map<T*>::iterator end = gamma.end();
         for (u_map<T*>::iterator it = gamma.begin(); it != end; ++it) {
-            relevant.insert(blocks[it->m_key]);
+            relevant.insert(it->m_key);
         }
         
     }
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 781c8539d..1c7a81444 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -435,11 +435,7 @@ namespace datalog {
             void destroy() {
                 SASSERT(this);
                 this->~base_ancestor();
-#if _DEBUG
-                memory::deallocate(__FILE__, __LINE__, this);
-#else
                 memory::deallocate(this);
-#endif
             }
         public:
             /**
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 91d27ed27..76069ce44 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -198,7 +198,7 @@ void memory::display_i_max_usage(std::ostream & os) {
               << "\n";
 }
 
-#if _DEBUG
+#if Z3DEBUG
 void memory::deallocate(char const * file, int line, void * p) {
     deallocate(p);
     TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";););
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index b6831faa7..aac61ea2a 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -60,7 +60,7 @@ public:
     static void deallocate(void* p);
     static ALLOC_ATTR void* allocate(size_t s);
     static ALLOC_ATTR void* reallocate(void *p, size_t s);
-#if _DEBUG
+#if Z3DEBUG
     static void deallocate(char const* file, int line, void* p);
     static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
 #endif