testing projection

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

src/muz/ddnf/doc.cpp

@@ -52,6 +52,9 @@ doc* doc_manager::allocate(doc const& src) {
     }
     return r;
 }
+doc* doc_manager::allocate(tbv* t) {
+    return alloc(doc, t);
+}
 doc* doc_manager::allocate(tbv const& src) {
     return allocate(m.allocate(src));
 }
@@ -317,6 +320,8 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
     for (unsigned i = 0; i < n; ++i) {
         if (to_delete[i] && (*bits)[i] == BIT_z) {
             new_todo.reset();
+            pos.reset();
+            neg.reset();
             for (unsigned j = 0; j < todo.size(); ++j) {
                 tbv& t = *todo[j];
                 switch(t[i]) {

src/muz/ddnf/tbv.cpp

@@ -19,12 +19,17 @@ Revision History:
 --*/
 
 #include "tbv.h"
+#include "hashtable.h"
+
+static ptr_addr_hashtable<tbv> allocated_tbvs;
 
 void tbv_manager::reset() {
     m.reset();
 }
 tbv* tbv_manager::allocate() {
-    return reinterpret_cast<tbv*>(m.allocate());
+    tbv* r = reinterpret_cast<tbv*>(m.allocate());
+    allocated_tbvs.insert(r);
+    return r;
 }
 tbv* tbv_manager::allocate1() {
     tbv* v = allocate();
@@ -42,7 +47,9 @@ tbv* tbv_manager::allocateX() {
     return v;
 }
 tbv* tbv_manager::allocate(tbv const& bv) {
-    return reinterpret_cast<tbv*>(m.allocate(bv));
+    tbv* r = allocate();
+    copy(*r, bv);
+    return r;
 }
 tbv* tbv_manager::allocate(uint64 val) {
     tbv* v = allocate0();
@@ -124,6 +131,11 @@ tbv* tbv_manager::allocate(rational const& r) {
     return v;
 }
 void tbv_manager::deallocate(tbv* bv) {
+    if (!allocated_tbvs.contains(bv)) {
+        std::cout << "double deallocate: " << bv << "\n";
+        UNREACHABLE();
+    }
+    allocated_tbvs.erase(bv);
     m.deallocate(bv);
 }    
 void tbv_manager::copy(tbv& dst, tbv const& src) const {

src/test/doc.cpp

@@ -74,17 +74,25 @@ static void tst_doc1(unsigned n) {
     m.display(std::cout, *d1) << "\n";
 
 
-#if 0
     svector<bool> to_delete(n, false);
     to_delete[1] = true;
     to_delete[3] = true;
     doc_manager m1(n-2);
-    doc_ref d1_1(m1, m1.project(n, to_delete.c_ptr(), *d0));
+    doc_ref d1_1(m1, m.project(m1, n, to_delete.c_ptr(), *d1));
     doc_ref d1_2(m1, m1.allocate1());
     m.display(std::cout, *d1) << " -> ";
     m1.display(std::cout, *d1_1) << "\n";
     SASSERT(m1.equals(*d1_1,*d1_2));
-#endif
+    m.set(*d1,2,BIT_x);
+    m.set(*d1,4,BIT_x);
+    d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
+    m.display(std::cout, *d1) << " -> ";
+    m1.display(std::cout, *d1_1) << "\n";
+    d1->neg().push_back(m.tbvm().allocate1());
+    SASSERT(m.well_formed(*d1));
+    d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
+    m.display(std::cout, *d1) << " -> ";
+    m1.display(std::cout, *d1_1) << "\n";    
 }
 
 
@@ -120,6 +128,13 @@ class test_doc_project {
         result = mk_or(m, clause.size(), clause.c_ptr());
     }
 
+    void project(doc const& d, doc_manager& m2, bool const* to_delete) {
+        doc_ref result(m2);
+        dm.display(std::cout, d) << " -> ";
+        result = dm.project(m2, m_vars.size(), to_delete, d);
+        m2.display(std::cout, *result) << "\n";
+    } 
+
     void test_clauses(unsigned num_clauses) {
         doc_ref d(dm, dm.allocateX());
         expr_ref_vector fmls(m);
@@ -132,8 +147,15 @@ class test_doc_project {
             fmls.push_back(clause);
         }
         fml = mk_and(m, fmls.size(), fmls.c_ptr());
-        dm.display(std::cout, *d) << "\n";
-        std::cout << fml << "\n";
+        svector<bool> to_delete(m_vars.size(), false);
+        unsigned num_bits = 1;
+        for (unsigned i = 1; i < to_delete.size(); ++i) {
+            to_delete[i] = (m_ran(2) == 0);
+            if (!to_delete[i]) ++num_bits;
+        }
+        doc_manager m2(num_bits);
+        project(*d, m2, to_delete.c_ptr());
+        // std::cout << fml << "\n";
         //
     }
 

src/test/tbv.cpp

@@ -24,6 +24,16 @@ static void tst1(unsigned num_bits) {
     VERIFY(m.intersect(*bX,*b0,*bN));
     SASSERT(m.equals(*b0, *bN));
     VERIFY(!m.intersect(*b0,*b1,*bN));
+    m.fill1(*b1);
+    svector<bool> to_delete(num_bits, false);
+    tbv_manager m2(num_bits-2);
+    to_delete[1] = true;
+    to_delete[3] = true;
+    (*b1).set(2, BIT_0);
+    (*b1).set(4, BIT_x);
+    tbv_ref b2(m2, m2.project(num_bits, to_delete.c_ptr(), *b1));
+    m.display(std::cout, *b1) << " -> ";
+    m2.display(std::cout, *b2) << "\n";
     m.deallocate(b0);
     m.deallocate(b1);
     m.deallocate(bX);