diff --git a/src/muz/ddnf/doc.cpp b/src/muz/ddnf/doc.cpp
index 2c6b4696e..27192ed26 100644
--- a/src/muz/ddnf/doc.cpp
+++ b/src/muz/ddnf/doc.cpp
@@ -66,6 +66,180 @@ doc& doc_manager::fillX(doc& src) const {
 bool doc_manager::set_and(doc& dst, doc const& src) const {
     return false;
 }
+bool doc_manager::fold_neg(doc& dst) {
+ start_over:
+    for (unsigned i = 0; i < dst.neg().size(); ++i) {
+        unsigned index;
+        unsigned count = diff_by_012(dst.pos(), dst.neg()[i], index);
+        if (count != 2) {
+            if (count == 0) {
+                return false;
+            }
+            else if (count == 3) {
+                dst.neg().erase(tbvm(), i);
+                --i;
+            }
+            else { // count == 1:
+                dst.pos().set(index, neg(dst.neg()[i][index]));
+                dst.neg().erase(tbvm(), i);
+                goto start_over;
+            }
+        }
+    }
+    return true;
+}
+
+unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& index) {
+    unsigned n = num_tbits();
+    unsigned count = 0;
+    for (unsigned i = 0; i < n; ++i) {
+        tbit b1 = pos[i];
+        tbit b2 = neg[i];
+        SASSERT(b1 != BIT_z && b2 != BIT_z);
+        if (b1 != b2) {
+            if (count == 1) return 2;
+            if (b1 == BIT_x) {
+                index = i;
+                count = 1;
+            }
+            else if (b2 != BIT_x) {
+                return 3;
+            }
+        }
+    }
+    return count;
+}
+doc* doc_manager::project(unsigned n, bool const* to_delete, doc const& src) {
+    tbv* p = tbvm().project(n, to_delete, src.pos());
+    if (src.neg().is_empty()) {
+        // build doc from p.
+        return 0;
+    }
+    ptr_vector<tbv> todo;
+#if 0
+    // tbv & ~tbv1 & ~tbv2 & ..
+    // Semantics of ~tbv1 is that it is a clause of literals.
+    //   indices where BIT_1 is set are negative.
+    //   indices where BIT_0 is set are positive.
+    // The first loop is supposed to project tbv_i directly
+    // when some safety condition is met.
+    // The second loop handles the remaining tbv_i that
+    // don't meet the safety condition.
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        if (can_project_neg(n, to_delete, src.neg()[i])) {
+            
+        }
+    }
+#endif
+#if 0
+    // REVIEW: what is the spec for this code?
+    ternary_diff_bitvector TBV(*this);
+    if (!TBV.fold_neg())
+        return false;
+    
+    std::set<ternary_bitvector*> todo;
+    cpy_bits_t cpy_bits;
+    ternary_bitvector newneg;
+    for (union_ternary_bitvector<ternary_bitvector>::iterator I = TBV.m_neg.begin(),
+             E = TBV.m_neg.end(); I != E; ++I) {
+        // check if subtract TBV should be skiped
+        for (unsigned i = 0; i < delcols.size()-1; ++i) {
+            unsigned idx = delcols[i];
+            if (I->get(idx) != TBV.m_pos.get(idx)) { // xx \ 1x
+                if (analyze_copy_bit(TBV.m_pos, *I, delcols, cpy_bits))
+                    todo.insert(&*I);
+                goto skip_row;
+            }
+        }
+        
+        newneg.reset();
+        I->project(delcols, new_size, newneg);
+        result.m_neg.add_fact(newneg);
+    skip_row:   ;
+    }
+    
+    if (!todo.empty()) {
+        for (std::set<ternary_bitvector*>::iterator I = todo.begin(),
+                 E = todo.end(); I != E; ++I) {
+            for (unsigned i = 0; i < delcols.size()-1; ++i) {
+                unsigned idx = delcols[i];
+                if ((*I)->get(idx) != TBV.m_pos.get(idx)) {
+                    cpy_bits_t::iterator II = cpy_bits.find(idx);
+                    if (II == cpy_bits.end())
+                        goto skip_bv;
+                    
+                    unsigned idx_keep = II->second.first;
+                    unsigned cpy_val = II->second.second;
+                    
+                    if (!((*I)->get(idx) & cpy_val) || (*I)->get(idx_keep) != BIT_x)
+                        goto skip_bv;
+                    
+                    (*I)->set(idx_keep, (*I)->get(idx));
+                }
+            }
+            
+            newneg.reset();
+            (*I)->project(delcols, new_size, newneg);
+            result.m_neg.add_fact(newneg);
+        skip_bv:        ;
+        }
+    }
+
+    return !result.is_empty();
+
+
+    // idx_del -> <idx_keep, val>
+    // val -> BIT_*
+    typedef std::map<unsigned, std::pair<unsigned, unsigned char> > cpy_bits_t;
+
+    static bool analyze_copy_bit(const ternary_bitvector& pos, const ternary_bitvector& neg,
+                                 const unsigned_vector& delcols, cpy_bits_t& cpy_bits) {
+      unsigned *del = delcols.c_ptr();
+      bool got_del_col = false, got_keep_col = false;
+      unsigned del_col = 0, keep_col = 0;
+
+      for (unsigned i = 0; i < pos.size(); ++i) {
+        if (pos.get(i) != neg.get(i)) {
+          if (*del == i) {
+            if (got_del_col)
+              return true;
+            del_col = i;
+            got_del_col = true;
+          } else {
+            if (got_keep_col)
+              return true;
+            keep_col = i;
+            got_keep_col = true;
+          }
+        }
+
+        if (i == *del)
+          ++del;
+      }
+
+      if (!got_del_col || !got_keep_col)
+        return true;
+      if (neg.get(keep_col) == neg.get(del_col))
+        return false;
+
+
+      unsigned char val = neg.get(del_col);
+      cpy_bits_t::iterator I = cpy_bits.find(del_col);
+      if (I == cpy_bits.end())
+          cpy_bits[del_col] = std::make_pair(keep_col, val);
+      else {
+          // FIXME: eq classes with size > 1 not supported for now
+          SASSERT(I->second.first == keep_col);
+          I->second.second |= val;
+      }
+
+      return false;
+    }
+
+#endif
+    return 0;
+}
+
 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) {
diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h
index 7196afc45..78cd5c94b 100644
--- a/src/muz/ddnf/doc.h
+++ b/src/muz/ddnf/doc.h
@@ -34,7 +34,7 @@ class doc_manager {
     tbv_manager m;
 public:
     doc_manager(unsigned n): m(n) {}
-    tbv_manager& tbv() { return m; }
+    tbv_manager& tbvm() { return m; }
     void reset();
     doc* allocate();
     doc* allocate1();
@@ -53,6 +53,7 @@ public:
     doc& fillX(doc& src) const;
     bool is_full(doc const& src) const;
     bool set_and(doc& dst, doc const& src) const;
+    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);
     void subtract(doc const& A, doc const& B, ptr_vector<doc>& result);
@@ -61,6 +62,9 @@ public:
     bool contains(doc const& a, doc const& b) const;
     std::ostream& display(std::ostream& out, doc const& b) const;
     unsigned num_tbits() const { return m.num_tbits(); }
+    doc* project(unsigned n, bool const* to_delete, doc const& src);
+private:
+    unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
 };
 
 typedef union_find<> subset_ints;
@@ -99,6 +103,11 @@ public:
     void push_back(T* t) {
         m_elems.push_back(t);
     }
+    void erase(M& m, unsigned idx) {
+        T* t = m_elems[idx];
+        m_elems.erase(t);
+        m.deallocate(t);
+    }
     void reset(M& m) {
         for (unsigned i = 0; i < m_elems.size(); ++i) {
             m.deallocate(m_elems[i]);
@@ -193,6 +202,12 @@ public:
             negated.reset(m);
         }
     }
+    void copy(M& m, union_bvec const& other) {
+        reset(m);
+        for (unsigned i = 0; i < other.size(); ++i) {
+            push_back(m.allocate(other[i]));
+        }
+    }
     void fix_eq_bits(unsigned idx1, tbv* BV, unsigned idx2, unsigned length,
                      subset_ints& equalities, const bit_vector& discard_cols) {
         for (unsigned i = 0; i < length; ++i) {
diff --git a/src/muz/ddnf/tbv.cpp b/src/muz/ddnf/tbv.cpp
index ad6dae69e..b1e5d5344 100644
--- a/src/muz/ddnf/tbv.cpp
+++ b/src/muz/ddnf/tbv.cpp
@@ -66,10 +66,23 @@ tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) {
 tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
     tbv* r = allocate();
     for (unsigned i = 0; i < num_tbits(); ++i) {
-        r->set(permutation[i], bv.get(i));
+        r->set(permutation[i], bv[i]);
     }
     return r;
 }
+tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
+    tbv* r = allocate();
+    unsigned i, j;
+    for (i = 0, j = 0; i < n; ++i) {
+        if (!to_delete[i]) {
+            r->set(j, src[i]);
+            ++j;
+        }
+    }
+    SASSERT(num_tbits() == j);
+    return r;
+}
+
 void tbv::set(uint64 val, unsigned hi, unsigned lo) {
     for (unsigned i = 0; i < hi - lo + 1; ++i) {
         set(lo + i, (val & (1ULL << i))?BIT_1:BIT_0);
@@ -90,7 +103,7 @@ void tbv::set(rational const& r, unsigned hi, unsigned lo) {
 
 void tbv::set(tbv const& other, unsigned hi, unsigned lo) {
     for (unsigned i = 0; i < hi - lo + 1; ++i) {
-        set(lo + i, other.get(i));
+        set(lo + i, other[i]);
     }
 }
 
diff --git a/src/muz/ddnf/tbv.h b/src/muz/ddnf/tbv.h
index e8eb7b589..bbe993b21 100644
--- a/src/muz/ddnf/tbv.h
+++ b/src/muz/ddnf/tbv.h
@@ -26,10 +26,16 @@ Revision History:
 
 class tbv;
 
-#define BIT_0 0x1
-#define BIT_1 0x2
-#define BIT_x 0x3
-#define BIT_z 0x0
+enum tbit {
+    BIT_z = 0x0,
+    BIT_0 = 0x1,
+    BIT_1 = 0x2,
+    BIT_x = 0x3
+};
+
+inline tbit neg(tbit t) {
+    return (tbit)(t ^ 0x3);
+}
 
 class tbv_manager {
     friend class tbv;
@@ -63,6 +69,7 @@ public:
     bool contains(tbv const& a, tbv const& b) const;
     bool intersect(tbv const& a, tbv const& b, tbv& result);
     std::ostream& display(std::ostream& out, tbv const& b) const;
+    tbv* project(unsigned n, bool const* to_delete, tbv const& src);
 };
 
 class tbv: private fixed_bit_vector {
@@ -91,13 +98,14 @@ public:
     void set(rational const& r, unsigned hi, unsigned lo);
     void set(tbv const& other, unsigned hi, unsigned lo);
 
-    unsigned operator[](unsigned idx) const { return get(idx); }
-    void set(unsigned index, unsigned value) {
+    tbit operator[](unsigned idx) const { return (tbit)get(idx); }
+    void set(unsigned index, tbit value) {
         SASSERT(value <= 3);
         fixed_bit_vector::set(2*index,   (value & 2) != 0);
         fixed_bit_vector::set(2*index+1, (value & 1) != 0);
     }
 
+
 private:
 
     unsigned get(unsigned index) const {
diff --git a/src/muz/ddnf/udoc_relation.cpp b/src/muz/ddnf/udoc_relation.cpp
index 1425535f1..34156c2c7 100644
--- a/src/muz/ddnf/udoc_relation.cpp
+++ b/src/muz/ddnf/udoc_relation.cpp
@@ -271,8 +271,8 @@ namespace datalog {
             for (unsigned i = 0; i < m_cols1.size(); ++i) {
                 unsigned idx1 = m_cols1[i];
                 unsigned idx2 = mid + m_cols2[i];
-                unsigned v1 = pos[idx1];
-                unsigned v2 = pos[idx2];
+                tbit v1 = pos[idx1];
+                tbit v2 = pos[idx2];
 
                 if (v1 == BIT_x) {
                     if (v2 != BIT_x)
@@ -294,12 +294,12 @@ namespace datalog {
                 
                 if (v1 == BIT_x && v2 == BIT_x) {
                     // add to subtracted TBVs: 1xx0 and 0xx1
-                    tbv* r = dm.tbv().allocate(pos);
+                    tbv* r = dm.tbvm().allocate(pos);
                     r->set(idx1, BIT_0);
                     r->set(idx2, BIT_1);
                     neg.push_back(r);
                     
-                    r = dm.tbv().allocate(pos);
+                    r = dm.tbvm().allocate(pos);
                     r->set(idx1, BIT_1);
                     r->set(idx2, BIT_0);
                     neg.push_back(r);
@@ -308,13 +308,13 @@ namespace datalog {
 
             // handle subtracted TBVs:  1010 -> 1010xxx
             for (unsigned i = 0; i < d1.neg().size(); ++i) {
-                tbv* t = dm.tbv().allocate();
+                tbv* t = dm.tbvm().allocate();
                 t->set(d1.neg()[i], mid-1, 0);
                 t->set(d2.pos(), hi - 1, mid);
                 neg.push_back(t);
             }
             for (unsigned i = 0; i < d2.neg().size(); ++i) {
-                tbv* t = dm.tbv().allocate();
+                tbv* t = dm.tbvm().allocate();
                 t->set(d1.pos(), mid-1, 0);
                 t->set(d2.neg()[i], hi - 1, mid);
                 neg.push_back(t);
@@ -625,8 +625,8 @@ namespace datalog {
             unsigned v = to_var(g)->get_idx();
             unsigned idx = column_idx(v);
             doc_manager& dm1 = get_plugin().dm(1);
-            tbv_ref bit1(dm1.tbv());
-            bit1 = dm1.tbv().allocate1();
+            tbv_ref bit1(dm1.tbvm());
+            bit1 = dm1.tbvm().allocate1();
             result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols);
         }
         else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
@@ -792,9 +792,9 @@ namespace datalog {
         virtual relation_base* operator()(const relation_base & tb) {
             udoc_relation const & t = get(tb);
             udoc const& u1 = t.get_udoc();
+            doc_manager& dm = t.get_dm();
             udoc  u2;
-            // copy u1 -> u2;
-            NOT_IMPLEMENTED_YET();
+            u2.copy(dm, u1);
             u2.intersect(dm, m_udoc);
             if (m_condition && !u2.is_empty()) {
                 t.apply_guard(m_condition, u2, m_col_list);