adding unit tests for doc

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

src/muz/ddnf/doc.cpp

@@ -22,49 +22,81 @@ Revision History:
 
 #include "doc.h"
 void doc_manager::reset() {
+    // m.reset(); - not until docs are in small object allocator.
 }
 doc* doc_manager::allocate() {
-    return 0;
+    return alloc(doc, m.allocate());
 }
 doc* doc_manager::allocate1() {
-    return 0;
+    return alloc(doc, m.allocate1());
 }
 doc* doc_manager::allocate0() {
-    return 0;                                                
+    return alloc(doc, m.allocate0());
 }
 doc* doc_manager::allocateX() {
-    return 0;
+    return alloc(doc, m.allocateX());
 }
 doc* doc_manager::allocate(doc const& src) {
-    return 0;
+    doc* r = alloc(doc, m.allocate(src.pos()));
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        r->neg().push_back(m.allocate(src.neg()[i]));
+    }
+    return r;
 }
 doc* doc_manager::allocate(uint64 n) {
-    return 0;
+    return alloc(doc, m.allocate(n));
 }
 doc* doc_manager::allocate(rational const& r) {
-    return 0;
+    return alloc(doc, m.allocate(r));
 }
 doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) {
-    return 0;
+    return alloc(doc, m.allocate(n, hi, lo));
 }
-doc* doc_manager::allocate(doc, unsigned const* permutation) {
-    return 0;
+doc* doc_manager::allocate(doc const& src, unsigned const* permutation) {
+    doc* r = alloc(doc, m.allocate(src.pos(), permutation));
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        r->neg().push_back(m.allocate(src.neg()[i], permutation));
+    }
+    return r;
 }
 void doc_manager::deallocate(doc* src) {
+    dealloc(src);
 }
-void doc_manager::copy(doc& dst, doc const& src) const {
+void doc_manager::copy(doc& dst, doc const& src)  {
+    m.copy(dst.pos(), src.pos());
+    unsigned n = std::min(src.neg().size(), dst.neg().size());
+    for (unsigned i = 0; i < n; ++i) {
+        m.copy(dst.neg()[i], src.neg()[i]);
+    }
+    for (unsigned i = n; i < dst.neg().size(); ++i) {
+        dst.neg().erase(m, dst.neg().size()-1);
+    }
+    for (unsigned i = n; i < src.neg().size(); ++i) {
+        dst.neg().push_back(m.allocate(src.neg()[i]));
+    }
 }
-doc& doc_manager::fill0(doc& src) const {
+doc& doc_manager::fill0(doc& src) {
+    src.neg().reset(m);
+    m.fill0(src.pos());
     return src;
 }
-doc& doc_manager::fill1(doc& src) const {
+doc& doc_manager::fill1(doc& src) {
+    src.neg().reset(m);
+    m.fill1(src.pos());
     return src;
 }
-doc& doc_manager::fillX(doc& src) const {
+doc& doc_manager::fillX(doc& src) {
+    src.neg().reset(m);
+    m.fillX(src.pos());
     return src;
 }
-bool doc_manager::set_and(doc& dst, doc const& src) const {
-    return false;
+bool doc_manager::set_and(doc& dst, doc const& src)  {
+    // (A \ B) & (C \ D) = (A & C) \ (B u D)
+    if (!m.set_and(dst.pos(), src.pos())) return false;
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        dst.neg().insert(m, m.allocate(src.neg()[i]));
+    }
+    return (src.neg().is_empty() || fold_neg(dst));
 }
 bool doc_manager::fold_neg(doc& dst) {
  start_over:

src/muz/ddnf/doc.h

@@ -44,15 +44,15 @@ public:
     doc* allocate(uint64 n);
     doc* allocate(rational const& r);
     doc* allocate(uint64 n, unsigned hi, unsigned lo);
-    doc* allocate(doc, unsigned const* permutation);
+    doc* allocate(doc const& src, unsigned const* permutation);
     void deallocate(doc* src);        
-    void copy(doc& dst, doc const& src) const;
-    doc& reset(doc& src) const { return fill0(src); }
-    doc& fill0(doc& src) const;
-    doc& fill1(doc& src) const;
-    doc& fillX(doc& src) const;
+    void copy(doc& dst, doc const& src);
+    doc& reset(doc& src) { return fill0(src); }
+    doc& fill0(doc& src);
+    doc& fill1(doc& src);
+    doc& fillX(doc& src);
     bool is_full(doc const& src) const;
-    bool set_and(doc& dst, doc const& src) const;
+    bool set_and(doc& dst, doc const& src);
     bool fold_neg(doc& dst);
     bool intersect(doc const& A, doc const& B, doc& result) const;
     void complement(doc const& src, ptr_vector<doc>& result);
@@ -328,6 +328,7 @@ public:
         }
     };
 
+    doc(tbv* t): m_pos(t) {}
     tbv& pos() { return *m_pos; }
     utbv& neg() { return m_neg; }
     tbv const& pos() const { return *m_pos; }
@@ -349,6 +350,7 @@ public:
     doc_ref& operator=(doc* d2) {
         if (d) dm.deallocate(d);
         d = d2;
+        return *this;
     }
     doc& operator*() { return *d; }
     doc* operator->() { return d; }

src/test/doc.cpp

@@ -0,0 +1,93 @@
+#include "doc.h"
+
+static void tst_doc1(unsigned n) {
+    doc_manager m(n);
+    
+    m.allocate();
+    m.reset();
+
+    doc_ref d(m, m.allocate());
+    doc_ref d1(m, m.allocate1());
+    doc_ref d0(m, m.allocate0());
+    doc_ref dX(m, m.allocateX());
+    doc_ref dXc(m, m.allocate(*dX));
+    doc_ref d10(m, m.allocate(10));
+    doc_ref d20(m, m.allocate(rational(20)));
+    unsigned hi = 3, lo = 1;
+    SASSERT(hi <= n);
+    doc_ref d111X(m, m.allocate(0xFF, hi, lo));
+    m.copy(*d, *d10);
+    SASSERT(m.equals(*d, *d10));
+    m.reset(*d);
+    SASSERT(!m.equals(*d, *d10));
+    m.fill0(*d10);
+    SASSERT(m.equals(*d, *d10));
+    m.fill1(*d);
+    d10 = m.allocate(10);
+    SASSERT(!m.equals(*d, *d10));
+    SASSERT(m.equals(*d, *d1));
+    m.fillX(*d);
+    SASSERT(m.equals(*d, *dX));
+    SASSERT(m.is_full(*dX));
+    SASSERT(!m.is_full(*d1));
+
+    VERIFY(m.set_and(*dX,*dX));
+    SASSERT(m.equals(*dXc,*dX));
+    VERIFY(m.set_and(*dX,*d1));
+    SASSERT(!m.equals(*dXc,*dX));
+    SASSERT(m.equals(*dX,*d1));
+    VERIFY(m.fold_neg(*dX));
+    ptr_vector<doc> result;
+    //    VERIFY(!m.intersect(*d1,*d0, result));    
+    m.subtract(*d1,*d0, result);
+    SASSERT(result.empty());
+    SASSERT(m.contains(*dX,*d1));
+    SASSERT(m.contains(*dX,*d0));
+    SASSERT(!m.contains(*d0,*d1));
+    SASSERT(!m.contains(*d1,*d0));
+
+
+    d1->neg().push_back(m.tbvm().allocate0());
+    m.display(std::cout, *d1) << " -> ";
+    VERIFY(m.fold_neg(*d1));
+    m.display(std::cout, *d1) << "\n";
+
+
+    svector<bool> to_delete(n);
+    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_2(m1, m1.allocate1());
+    m.display(std::cout, *d1) << " -> ";
+    m1.display(std::cout, *d1_1) << "\n";
+    SASSERT(m1.equals(*d1_1,*d1_2));
+    
+}
+
+
+// generate "all" clauses over num_vars
+// create XXXX \ clauses
+// project 0, 1, 2, 3 variables
+// check that result is the same as QE over those clauses.
+
+class test_doc_project {
+    random_gen m_ran;
+
+    void test_clauses(unsigned num_vars, unsigned num_clauses) {
+        //
+    }
+
+public:    
+    void operator()(unsigned num_vars, unsigned min_clauses, unsigned max_clauses) {        
+        for (unsigned i = min_clauses; i < max_clauses; ++i) {
+            test_clauses(num_vars, i);
+        }    
+    }
+};
+
+void tst_doc() {
+    tst_doc1(5);
+    tst_doc1(10);
+    tst_doc1(70);
+}

src/test/main.cpp

@@ -142,6 +142,7 @@ int main(int argc, char ** argv) {
     TST(bit_vector);
     TST(fixed_bit_vector);
     TST(tbv);
+    TST(doc);
     TST(string_buffer);
     TST(map);
     TST(diff_logic);

src/test/sorting_network.cpp

@@ -7,6 +7,7 @@
 #include "smt_kernel.h"
 #include "model_smt2_pp.h"
 #include "smt_params.h"
+#include "ast_util.h"
 
 
 
@@ -171,7 +172,7 @@ struct ast_ext2 {
         return trail(m.mk_fresh_const("x", m.mk_bool_sort()));
     }
     void mk_clause(unsigned n, literal const* lits) {
-        m_clauses.push_back(m.mk_or_reduced(n, lits));
+        m_clauses.push_back(mk_or(m, n, lits));
     }
 };