handle fix_eq functionality

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

src/muz/ddnf/doc.cpp

@@ -105,11 +105,31 @@ doc& doc_manager::fillX(doc& src) {
 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 < dst.neg().size(); ++i) {
+        if (!m.set_and(dst.neg()[i], dst.pos())) {
+            dst.neg().erase(m, i);
+            --i;
+        }
+    }
+    tbv_ref t(m);
     for (unsigned i = 0; i < src.neg().size(); ++i) {
-        dst.neg().insert(m, m.allocate(src.neg()[i]));
+        t = m.allocate(src.neg()[i]);
+        if (m.set_and(*t, dst.pos())) {
+            dst.neg().insert(m, t.detach());
+        }
     }
     return (src.neg().is_empty() || fold_neg(dst));
 }
+
+bool doc_manager::well_formed(doc const& d) const {
+    if (!m.is_well_formed(d.pos())) return false;
+    for (unsigned i = 0; i < d.neg().size(); ++i) {
+        if (!m.is_well_formed(d.neg()[i])) return false;
+        if (!m.contains(d.pos(), d.neg()[i])) return false;
+    }
+    return true;
+}
+
 bool doc_manager::fold_neg(doc& dst) {
  start_over:
     for (unsigned i = 0; i < dst.neg().size(); ++i) {
@@ -153,6 +173,85 @@ unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& inde
     }
     return count;
 }
+
+void doc_manager::set(doc& d, unsigned idx, tbit value) {
+    d.pos().set(idx, value);
+    for (unsigned i = 0; i < d.neg().size(); ++i) {
+        d.neg()[i].set(idx, 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) {
+    for (unsigned i = 0; i < length; ++i) {
+        unsigned idx = lo + i;
+        if (!merge(d, lo + i, equalities, discard_cols)) return false;
+    }
+    return true;
+}
+bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols) {
+    unsigned root = equalities.find(idx);
+    idx = root;
+    unsigned num_x = 0;
+    unsigned root1;
+    tbit value = BIT_x;
+    do {
+        switch (d[idx]) {
+        case BIT_0:
+            if (value == BIT_1) return false;
+            value = BIT_0;
+            break;
+        case BIT_1:
+            if (value == BIT_0) return false;
+            value = BIT_1;
+            break;
+        case BIT_x:
+            if (!discard_cols.get(idx)) {
+                ++num_x;
+                root1 = idx;
+            }
+            break;
+        default:
+            break;
+        }
+        idx = equalities.next(idx);
+    }
+    while (idx != root);
+
+    if (num_x == 0) {
+        // nothing to do.
+    }
+    else if (value != BIT_x) {
+        do {
+            if (d[idx] == BIT_x) {
+                set(d, idx, value);
+            }
+            idx = equalities.next(idx);
+        }
+        while (idx != root);
+    }
+    else {
+        do {
+            if (!discard_cols.get(idx) && idx != root1) {
+                tbv* t = tbvm().allocate(d.pos());
+                t->set(idx, BIT_0);
+                t->set(root1, BIT_1);
+                d.neg().insert(tbvm(), t);
+                t = tbvm().allocate(d.pos());
+                t->set(idx, BIT_1);
+                t->set(root1, BIT_0);
+                d.neg().insert(tbvm(), t);                
+            }
+            idx = equalities.next(idx);
+        }
+        while (idx != root);
+    }
+    return true;
+}
+
 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()) {

src/muz/ddnf/doc.h

@@ -29,6 +29,7 @@ Revision History:
 
 class doc;
 template<typename M, typename T> class union_bvec;
+typedef union_find<> subset_ints;
 
 class doc_manager {
     tbv_manager m;
@@ -65,11 +66,14 @@ public:
     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);
+    bool well_formed(doc const& d) const;
+    bool merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols);
+    void set(doc& d, unsigned idx, tbit value);
 private:
     unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
+    bool merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols);
 };
 
-typedef union_find<> subset_ints;
 
 // union of tbv*, union of doc*
 template<typename M, typename T>
@@ -210,98 +214,31 @@ public:
             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) {
-            unsigned k = 0;
-            for (unsigned j = 0; j < size(); ++j, ++k) {
-                NOT_IMPLEMENTED_YET();
 
-#if 0
-                T *eqBV = BV ? const_cast<T*>(BV) : &*I;
-                bool discard_col = discard_cols.get(idx1+i) || (!BV && discard_cols.get(idx2+i));
-                
-                switch (fix_single_bit(*I, idx1+i, eqBV, idx2+i, equalities, discard_col)) {
-                case 1:
-                    // remove row
-                    I = m_bitvectors.erase(I);
-                    break;
-                    
-                case 2: {
-                    // don't care column equality. try subtraction first.
-                    union_ternary_bitvector diff(I->size()), result(I->size());
-                    T BV(I->size(), true);
-                    BV.set(idx1+i, BIT_0);
-                    BV.set(idx2+i, BIT_1);
-                    diff.add_new_fact(BV);
-                    
-                    BV.set(idx1+i, BIT_1);
-                    BV.set(idx2+i, BIT_0);
-                    diff.add_new_fact(BV);
-                    
-                    I->subtract(diff, result);
-                    *I = *result.begin();
-                    ++I;
-                    break;
-                }
-
-                default:
-                    if (I->is_empty()) {
-                        I = m_bitvectors.erase(I);
-                    } else {
-                        // bits fixed
-                        ++I;
-                    }
-                }
-#endif
+    void merge(M& m, unsigned lo, unsigned length, subset_ints & equalities, bit_vector const& discard_cols) {
+        for (unsigned i = 0; i < size(); ++i) {
+            if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) {
+                erase(m, i);
+                --i;
             }
         }
     }
 
+    void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) {
+        union_find_default_ctx union_ctx;
+        subset_ints equalities(union_ctx);
+        for (unsigned i = 0; i < discard_cols.size(); ++i) {
+            equalities.mk_var();
+        }
+        for (unsigned j = 0; j < length; ++j) {
+            equalities.merge(lo1 + j, lo2 + j);
+        }
+        merge(m, lo1, length, equalities, discard_cols);
+    }
+
+
 private:
 
-    fix_bit_result_t fix_single_bit(tbv& bv, unsigned idx, unsigned value, const subset_ints& equalities) {
-        unsigned root = equalities.find(idx);
-        idx = root;
-        do {
-            unsigned bitval = bv.get(idx);
-            if (bitval == tbv::BIT_x) {
-                bv.set(idx, value);
-            } 
-            else if (bitval != value) {
-                return e_row_removed;
-            }
-            idx = equalities.next(idx);
-        } 
-        while (idx != root);
-        return e_fixed;
-    }
-
-    fix_bit_result_t fix_single_bit(tbv & BV1, unsigned idx1, tbv & BV2, unsigned idx2,
-                                  subset_ints& equalities, bool discard_col) {
-        unsigned A = BV1.get(idx1);
-        unsigned B = BV2.get(idx2);
-        
-        if (A == tbv::BIT_x) {
-            if (B == tbv::BIT_x) {
-                // Both are don't cares.
-                if (!discard_col)
-                    return e_duplicate_row;
-                equalities.merge(idx1, idx2);
-                return e_fixed;
-            } else {
-                // only A is don't care.
-                return fix_single_bit(BV1, idx1, B, equalities);
-            }
-        } else if (B == tbv::BIT_x) {
-            // Only B is don't care.
-            return fix_single_bit(BV2, idx2, A, equalities);
-        } else if (A == B) {
-            return e_fixed;
-        } else {
-            return e_row_removed;
-        }
-    }
 
 };
 
@@ -335,7 +272,7 @@ public:
     utbv& neg() { return m_neg; }
     tbv const& pos() const { return *m_pos; }
     utbv const& neg() const { return m_neg; }
-        
+    tbit operator[](unsigned idx) const { return pos()[idx]; }        
 };
 
 typedef union_bvec<doc_manager, doc> udoc;

src/muz/ddnf/tbv.cpp

@@ -150,8 +150,12 @@ tbv& tbv_manager::set_or(tbv& dst,  tbv const& src) const {
 }
 bool tbv_manager::set_and(tbv& dst,  tbv const& src) const {
     m.set_and(dst, src); 
+    return is_well_formed(dst);
+}
+
+bool tbv_manager::is_well_formed(tbv const& dst) const {
     for (unsigned i = 0; i < num_tbits(); ++i) {
-        if (dst.get(i) == BIT_z) return false;
+        if (dst[i] == BIT_z) return false;
     }
     return true;
 }

src/muz/ddnf/tbv.h

@@ -70,6 +70,7 @@ public:
     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);
+    bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
 };
 
 class tbv: private fixed_bit_vector {
@@ -130,6 +131,7 @@ public:
     }
     tbv& operator*() { return *d; }
     tbv* get() { return d; }
+    tbv* detach() { tbv* result = d; d = 0; return result; }
 };
 
 

src/muz/ddnf/udoc_relation.cpp

@@ -461,14 +461,18 @@ namespace datalog {
             for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) {
                 m_equalities.mk_var();
             }
+            for (unsigned i = 1; i < col_cnt; ++i) {
+                for (unsigned j = 0; j < m_size; ++j) {
+                    m_equalities.merge(m_cols[0]+j ,m_cols[i]+j);
+                }
+            }
         }
         
         virtual void operator()(relation_base & _r) {
             udoc_relation& r = get(_r);
             udoc& d = r.get_udoc();
-            for (unsigned i = 1; i < m_cols.size(); ++i) {
-                d.fix_eq_bits(m_cols[0], 0, m_cols[i], m_size, m_equalities, m_empty_bv);
-            }
+            doc_manager& dm = r.get_dm();
+            d.merge(dm, m_cols[0], m_size, m_equalities, m_empty_bv);
             TRACE("dl", tout << "final size: " << r.get_size_estimate_rows() << '\n';);
         }
     };
@@ -624,10 +628,10 @@ namespace datalog {
             SASSERT(m.is_bool(g));
             unsigned v = to_var(g)->get_idx();
             unsigned idx = column_idx(v);
-            doc_manager& dm1 = get_plugin().dm(1);
-            tbv_ref bit1(dm1.tbvm());
-            bit1 = dm1.tbvm().allocate1();
-            result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols);
+            doc_ref d(dm);
+            d = dm.allocateX();
+            dm.set(*d, idx, BIT_1);
+            result.intersect(dm, *d);
         }
         else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
             unsigned hi, lo;
@@ -650,7 +654,7 @@ namespace datalog {
                 unsigned idx1 = column_idx(v1->get_idx());
                 unsigned idx2 = column_idx(v2->get_idx());
                 unsigned length = column_num_bits(v1->get_idx());
-                result.fix_eq_bits(idx1, 0, idx2, length, equalities, discard_cols);
+                result.merge(dm, idx1, idx2, length, discard_cols);
             }   
             else {
                 goto failure_case;