From 9a3a1835cc8a95eb755382f25df754a6d9167702 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Sep 2014 05:52:09 -0700
Subject: [PATCH] doc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/ddnf/doc.cpp | 51 +++++++++++++++++++++++++++++++++++++++-----
 src/muz/ddnf/doc.h   |  4 +++-
 src/test/doc.cpp     | 32 ++++++++++++++++++++++++---
 3 files changed, 78 insertions(+), 9 deletions(-)

diff --git a/src/muz/ddnf/doc.cpp b/src/muz/ddnf/doc.cpp
index b9aca8bc7..ab3905acd 100644
--- a/src/muz/ddnf/doc.cpp
+++ b/src/muz/ddnf/doc.cpp
@@ -21,6 +21,15 @@ Revision History:
 --*/
 
 #include "doc.h"
+
+doc_manager::doc_manager(unsigned n): m(n) {
+    m_full = m.allocateX();
+}
+
+doc_manager::~doc_manager() {
+    m.deallocate(m_full);
+}
+
 void doc_manager::reset() {
     // m.reset(); - not until docs are in small object allocator.
 }
@@ -60,6 +69,9 @@ doc* doc_manager::allocate(doc const& src, unsigned const* permutation) {
     return r;
 }
 void doc_manager::deallocate(doc* src) {
+    if (!src) return;
+    m.deallocate(&src->pos());
+    src->neg().reset(m);
     dealloc(src);
 }
 void doc_manager::copy(doc& dst, doc const& src)  {
@@ -277,18 +289,47 @@ void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
 void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {
 }
 bool doc_manager::equals(doc const& a, doc const& b) const {
-    return false;
+    if (!m.equals(a.pos(), b.pos())) return false;
+    if (a.neg().size() != b.neg().size()) return false;
+    for (unsigned i = 0; i < a.neg().size(); ++i) {
+        if (!m.equals(a.neg()[i], b.neg()[i])) return false;
+    }
+    return true;
 }
 bool doc_manager::is_full(doc const& src) const {
-    return false;
+    return src.neg().is_empty() && m.equals(src.pos(), *m_full);
 }
 unsigned doc_manager::hash(doc const& src) const {
-    return 0;
+    unsigned r = 0;
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        r = 2*r + m.hash(src.neg()[i]);
+    }
+    return r + m.hash(src.pos());
 }
+// approximation
+// A \ (A1 u A2) contains B \ (B1 u B2)
+// if
+// A contains B
+// B1 contains A1 or A2
 bool doc_manager::contains(doc const& a, doc const& b) const {
-    return false;
+    if (!m.contains(a.pos(), b.pos())) return false;
+    for (unsigned i = 0; i < b.neg().size(); ++i) {
+        bool found = false;
+        for (unsigned j = 0; !found && j < a.neg().size(); ++j) {
+            found = m.contains(b.neg()[i],a.neg()[j]);
+        }
+        if (!found) return false;
+    }
+    return true;
 }
 std::ostream& doc_manager::display(std::ostream& out, doc const& b) const {
-    return out;
+    m.display(out, b.pos());
+    if (b.neg().is_empty()) return out;
+    out << " \\ {";
+    for (unsigned i = 0; i < b.neg().size(); ++i) {
+        m.display(out, b.neg()[i]);
+        if (i + 1 < b.neg().size()) out << ", ";
+    }    
+    return out << "}";
 }
 
diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h
index 3b24b52d1..e85d6f74a 100644
--- a/src/muz/ddnf/doc.h
+++ b/src/muz/ddnf/doc.h
@@ -32,8 +32,10 @@ template<typename M, typename T> class union_bvec;
 
 class doc_manager {
     tbv_manager m;
+    tbv*        m_full;
 public:
-    doc_manager(unsigned n): m(n) {}
+    doc_manager(unsigned num_bits);
+    ~doc_manager();
     tbv_manager& tbvm() { return m; }
     void reset();
     doc* allocate();
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index 27508bac4..9d37654af 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -73,15 +73,41 @@ static void tst_doc1(unsigned n) {
 
 class test_doc_project {
     random_gen m_ran;
+    int        m_num_vars;
 
-    void test_clauses(unsigned num_vars, unsigned num_clauses) {
+    unsigned choose_var() {
+        return m_ran(m_num_vars) + 1;
+    }
+    tbit choose_tbit() {
+        switch(m_ran(3)) {
+        case 0: return BIT_0;
+        case 1: return BIT_1;
+        default : return BIT_x;
+        }
+    }
+    void mk_clause(svector<int>& clause, tbv& t) {
+        for (int i = 0; i < m_num_vars; ++i) {
+            tbit b = choose_tbit();
+            t.set(i, b);            
+            switch (b) {
+            case BIT_0: clause.push_back(-i-1); break;
+            case BIT_1: clause.push_back(i+1); break;
+            default: break;
+            }
+        }
+    }
+
+    void test_clauses(unsigned num_clauses) {
+        
         //
     }
 
 public:    
-    void operator()(unsigned num_vars, unsigned min_clauses, unsigned max_clauses) {        
+    test_doc_project(unsigned num_vars): m_num_vars(num_vars) {}
+
+    void operator()(unsigned min_clauses, unsigned max_clauses) {        
         for (unsigned i = min_clauses; i < max_clauses; ++i) {
-            test_clauses(num_vars, i);
+            test_clauses(i);
         }    
     }
 };