unit test merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz/ddnf/doc.cpp

@@ -190,7 +190,10 @@ void doc_manager::set(doc& d, unsigned idx, tbit value) {
 // merge range from [lo:lo+length-1] with each index in equivalence class.
 // under assumption of equalities and columns that are discarded.
 //
-bool doc_manager::merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols) {
+bool doc_manager::merge(
+    doc& d, unsigned lo, unsigned length, 
+    subset_ints& equalities, bit_vector const& discard_cols) {
+    std::cout << "merge\n";
     for (unsigned i = 0; i < length; ++i) {
         unsigned idx = lo + i;
         if (!merge(d, lo + i, equalities, discard_cols)) return false;
@@ -242,10 +245,12 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vecto
         do {
             if (!discard_cols.get(idx) && idx != root1) {
                 tbv* t = tbvm().allocate(d.pos());
+                std::cout << "insert " << t << "\n";
                 t->set(idx, BIT_0);
                 t->set(root1, BIT_1);
                 d.neg().insert(tbvm(), t);
                 t = tbvm().allocate(d.pos());
+                std::cout << "insert " << t << "\n";
                 t->set(idx, BIT_1);
                 t->set(root1, BIT_0);
                 d.neg().insert(tbvm(), t);                
@@ -314,7 +319,8 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
     if (todo.empty()) {
         return r;
     }
-    ptr_vector<tbv> pos, neg, new_todo;
+    ptr_vector<tbv> new_todo;
+    utbv pos, neg;
     tbv_ref t1(tbvm()), t2(tbvm());
     for (unsigned i = 0; i < n; ++i) {
         if (to_delete[i] && (*bits)[i] != BIT_x) {
@@ -323,50 +329,49 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
                       tbvm().display(tout, *todo[j]) << " ";
                   }
                   tout << "\n";);
-            new_todo.reset();
+            SASSERT(pos.is_empty());
-            pos.reset();
+            SASSERT(neg.is_empty());
-            neg.reset();
+            SASSERT(new_todo.empty());
-            for (unsigned j = 0; j < todo.size(); ++j) {
+            while (!todo.empty()) {
-                tbv& t = *todo[j];
+                tbv* t = todo.back();
-                switch(t[i]) {
+                todo.pop_back();
-                case BIT_x: new_todo.push_back(&t); break;
+                switch((*t)[i]) {
-                case BIT_0: neg.push_back(&t); break;
+                case BIT_x: new_todo.push_back(t); break;
-                case BIT_1: pos.push_back(&t); break;
+                case BIT_0: neg.push_back(t); break;
+                case BIT_1: pos.push_back(t); break;
                 default: UNREACHABLE(); break;                    
                 }
             }
-            if (pos.empty() || neg.empty()) {
+            if (pos.is_empty() || neg.is_empty()) {
                 std::swap(new_todo, todo);
+                pos.reset(tbvm());
+                neg.reset(tbvm());
                 continue;
             }
             TRACE("doc",
                   tout << "pos: ";
                   for (unsigned i = 0; i < pos.size(); ++i) {
-                      tbvm().display(tout, *pos[i]) << " ";
+                      tbvm().display(tout, pos[i]) << " ";
                   }
                   tout << "\nneg: ";
                   for (unsigned i = 0; i < neg.size(); ++i) {
-                      tbvm().display(tout, *neg[i]) << " ";
+                      tbvm().display(tout, neg[i]) << " ";
                   }
                   tout << "\n";
                   );
                   
             for (unsigned j = 0; j < pos.size(); ++j) {
                 for (unsigned k = 0; k < neg.size(); ++k) {
-                    t1 = tbvm().allocate(*pos[j]);
+                    t1 = tbvm().allocate(pos[j]);
                     (*t1).set(i, BIT_x);
-                    if (tbvm().set_and(*t1, *neg[k])) {
+                    if (tbvm().set_and(*t1, neg[k])) {
                         (*t1).set(i, BIT_x);
                         new_todo.push_back(t1.detach());
                     }
                 }                
             }
-            for (unsigned i = 0; i < pos.size(); ++i) {
+            pos.reset(tbvm());
-                tbvm().deallocate(pos[i]);
+            neg.reset(tbvm());
-            }
-            for (unsigned i = 0; i < neg.size(); ++i) {
-                tbvm().deallocate(neg[i]);
-            }
             std::swap(todo, new_todo);
         }
     }

src/muz/ddnf/doc.h

@@ -131,12 +131,14 @@ public:
                 m.deallocate(m_elems[i]);
                 --j;
             }
-            else if (m.contains(*m_elems[i], *t)) {
+            else {
-                found = true;
+                if (m.contains(*m_elems[i], *t)) {
-            }
+                    found = true;
-            else if (i != j) {                
+                }
-                m_elems[j] = m_elems[i];
+                if (i != j) {                
-            }                
+                    m_elems[j] = m_elems[i];
+                }       
+            }         
         }
         if (j != sz) m_elems.resize(j);
         if (found) {

src/muz/ddnf/tbv.cpp

@@ -22,8 +22,11 @@ Revision History:
 #include "hashtable.h"
 
 
+//#define _DEBUG_MEM 1
+#define _DEBUG_MEM 0
+
 tbv_manager::~tbv_manager() {    
-#if 0
+#if _DEBUG_MEM
     ptr_vector<tbv>::iterator it = allocated_tbvs.begin(), end = allocated_tbvs.end();
     for (; it != end; ++it) {
         std::cout << "dangling: " << (*it) << "\n";
@@ -36,8 +39,10 @@ void tbv_manager::reset() {
 }
 tbv* tbv_manager::allocate() {
     tbv* r = reinterpret_cast<tbv*>(m.allocate());
-    //std::cout << allocated_tbvs.size() << " " << r << "\n";
+#if _DEBUG_MEM
-    //allocated_tbvs.insert(r);
+    std::cout << allocated_tbvs.size() << " " << r << "\n";
+    allocated_tbvs.insert(r);
+#endif
     return r;
 }
 tbv* tbv_manager::allocate1() {
@@ -140,11 +145,12 @@ tbv* tbv_manager::allocate(rational const& r) {
     return v;
 }
 void tbv_manager::deallocate(tbv* bv) {
-#if 0
+#if _DEBUG_MEM
     if (!allocated_tbvs.contains(bv)) {
         std::cout << "double deallocate: " << bv << "\n";
         UNREACHABLE();
     }
+    std::cout << "deallocate: " << bv << "\n";
     allocated_tbvs.erase(bv);
 #endif
     m.deallocate(bv);

src/muz/ddnf/tbv.h

@@ -40,7 +40,7 @@ inline tbit neg(tbit t) {
 class tbv_manager {
     friend class tbv;
     fixed_bit_vector_manager m;
-    //    ptr_vector<tbv> allocated_tbvs;
+    ptr_vector<tbv> allocated_tbvs;
 public:
     tbv_manager(unsigned n): m(2*n) {}
     ~tbv_manager();

src/test/doc.cpp

@@ -100,7 +100,7 @@ static void tst_doc1(unsigned n) {
 // project 0, 1, 2, 3 variables
 // check that result is the same as QE over those clauses.
 
-class test_doc_project {
+class test_doc_cls {
     random_gen      m_ran;
     ast_manager     m;
     doc_manager     dm;
@@ -179,7 +179,7 @@ class test_doc_project {
               );        
     } 
 
-    void test_clauses(unsigned num_clauses) {
+    void test_project(unsigned num_clauses) {
         doc_ref d(dm, dm.allocateX());
         expr_ref_vector fmls(m);
         th_rewriter rw(m);
@@ -222,26 +222,74 @@ class test_doc_project {
         SASSERT(res == l_false);
     }
 
+    void test_merge(unsigned num_clauses) {
+        doc_ref d(dm, dm.allocateX());
+        expr_ref_vector fmls(m);
+        th_rewriter rw(m);
+        unsigned N = m_vars.size();
+        expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m);
+        for (unsigned i = 0; i < num_clauses; ++i) {
+            tbv* t = dm.tbvm().allocate();
+            fmls.push_back(m.mk_not(mk_conj(*t)));
+            d->neg().push_back(t);
+        }
+        fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
+        svector<bool> to_merge(N, false), to_delete(N, false);
+        bit_vector discard_cols;
+        discard_cols.resize(N, false);
+        unsigned num_bits = 1;
+        union_find_default_ctx union_ctx;
+        subset_ints equalities(union_ctx);
+        unsigned lo = N;
+        equalities.mk_var();
+        for (unsigned i = 1; i < N; ++i) {
+            to_merge[i] = (m_ran(2) == 0);
+            if (!to_merge[i]) ++num_bits; else lo = i;
+            equalities.mk_var();
+        }
+        if (lo == N) return;
+        for (unsigned i = 0; i < N; ++i) {
+            if (to_merge[i] && i != lo) {
+                equalities.merge(i, lo);
+            }
+        }
+        fml1 = to_formula(*d, dm, to_delete.c_ptr());
+        if (dm.merge(*d, lo, 1, equalities, discard_cols)) {
+            fml2 = to_formula(*d, dm, to_delete.c_ptr());
+            std::cout << fml1 << "\n";
+            std::cout << fml2 << "\n";
+        }
+        // ...
+    }
+
 public:    
-    test_doc_project(unsigned num_vars): dm(num_vars), m_vars(m) {
+    test_doc_cls(unsigned num_vars): dm(num_vars), m_vars(m) {
         reg_decl_plugins(m);
         for (unsigned i = 0; i < num_vars; ++i) {
             m_vars.push_back(m.mk_fresh_const("b", m.mk_bool_sort()));
         }
     }
 
-    void operator()(unsigned num_rounds, unsigned num_clauses) {        
+    void test_project(unsigned num_rounds, unsigned num_clauses) {        
         for (unsigned i = 0; i < num_rounds; ++i) {
-            test_clauses(num_clauses);
+            test_project(num_clauses);
+        }    
+    }
+
+    void test_merge(unsigned num_rounds, unsigned num_clauses) {
+        for (unsigned i = 0; i < num_rounds; ++i) {
+            test_merge(num_clauses);
         }    
     }
 };
 
+
 void tst_doc() {
     tst_doc1(5);
     tst_doc1(10);
     tst_doc1(70);
 
-    test_doc_project tp(4);    
+    test_doc_cls tp(4);    
-    tp(200,7);
+    tp.test_merge(200,7);
+    tp.test_project(200,7);
 }