porting fun

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

src/muz/ddnf/doc.cpp

@@ -47,6 +47,9 @@ doc* doc_manager::allocate(rational const& r) {
 doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) {
     return 0;
 }
+doc* doc_manager::allocate(doc, unsigned const* permutation) {
+    return 0;
+}
 void doc_manager::deallocate(doc* src) {
 }
 void doc_manager::copy(doc& dst, doc const& src) const {

src/muz/ddnf/doc.h

@@ -24,6 +24,8 @@ Revision History:
 #define _DOC_H_
 
 #include "tbv.h"
+#include "union_find.h"
+
 
 class doc;
 template<typename M, typename T> class union_bvec;
@@ -42,6 +44,7 @@ public:
     doc* allocate(uint64 n);
     doc* allocate(rational const& r);
     doc* allocate(uint64 n, unsigned hi, unsigned lo);
+    doc* allocate(doc, unsigned const* permutation);
     void deallocate(doc* src);        
     void copy(doc& dst, doc const& src) const;
     doc& reset(doc& src) const { return fill0(src); }
@@ -62,6 +65,15 @@ public:
 template<typename M, typename T>
 class union_bvec { 
     ptr_vector<T> m_elems; // TBD: reuse allocator of M
+
+    enum fix_bit_result_t {
+        e_row_removed, // = 1
+        e_duplicate_row, // = 2
+        e_fixed
+    };
+
+    typedef union_find<> subset_ints;
+
 public:
     unsigned size() const { return m_elems.size(); }
     T& operator[](unsigned idx) const { return *m_elems[idx]; }
@@ -81,7 +93,7 @@ public:
         }
         m_elems.reset(); 
     }    
-    void insert(M& m, T* t) {
+    bool insert(M& m, T* t) {
         unsigned sz = size(), j = 0;
         bool found = false;
         for (unsigned i = 0; i < sz; ++i, ++j) {
@@ -103,6 +115,7 @@ public:
         else {
             m_elems.push_back(t);
         }
+        return !found;
     }
     bool intersect(M& m, T& t) {
         unsigned sz = size();
@@ -145,6 +158,97 @@ public:
             negated.reset(m);
         }
     }
+    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) {
+
+#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
+            }
+        }
+    }
+
+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;
+        }
+    }
 
 };
 

src/muz/ddnf/tbv.cpp

@@ -59,10 +59,17 @@ tbv* tbv_manager::allocate(uint64 val) {
 
 tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) {
     tbv* v = allocateX();
-    SASSERT(64 >= m.num_bits() && m.num_bits() > hi && hi >= lo);
+    SASSERT(64 >= num_tbits() && num_tbits() > hi && hi >= lo);
     v->set(val, hi, lo);
     return v;
 }
+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));
+    }
+    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);

src/muz/ddnf/tbv.h

@@ -26,12 +26,13 @@ Revision History:
 
 class tbv;
 
+#define BIT_0 0x1
+#define BIT_1 0x2
+#define BIT_x 0x3
+#define BIT_z 0x0
+
 class tbv_manager {
     friend class tbv;
-    static const unsigned BIT_0 = 0x1;
-    static const unsigned BIT_1 = 0x2;
-    static const unsigned BIT_x = 0x3;
-    static const unsigned BIT_z = 0x0;
     fixed_bit_vector_manager m;
 public:
     tbv_manager(unsigned n): m(2*n) {}
@@ -44,6 +45,7 @@ public:
     tbv* allocate(uint64 n);
     tbv* allocate(rational const& r);
     tbv* allocate(uint64 n, unsigned hi, unsigned lo);
+    tbv* allocate(tbv const& bv, unsigned const* permutation);
 
     void deallocate(tbv* bv);
         
@@ -69,11 +71,6 @@ class tbv: private fixed_bit_vector {
 
 public:
 
-    static const unsigned BIT_0 = tbv_manager::BIT_0;
-    static const unsigned BIT_1 = tbv_manager::BIT_1;
-    static const unsigned BIT_x = tbv_manager::BIT_x;
-    static const unsigned BIT_z = tbv_manager::BIT_z;
-
     struct eq {
         tbv_manager& m;
         eq(tbv_manager& m):m(m) {}

src/muz/ddnf/udoc_relation.cpp

@@ -108,6 +108,10 @@ namespace datalog {
         return dynamic_cast<udoc_relation const&>(r);        
     }
 
+    doc_manager& udoc_plugin::dm(relation_signature const& sig) {
+        return dm(udoc_relation::num_signature_bits(bv, sig));
+    }
+
     doc_manager& udoc_plugin::dm(unsigned n) {
         doc_manager* r;
         if (!m_dms.find(n, r)) {
@@ -116,17 +120,20 @@ namespace datalog {
         }
         return *r;
     }
-    bool udoc_plugin::can_handle_signature(const relation_signature & s) {
-        NOT_IMPLEMENTED_YET();
-        return false;
+    bool udoc_plugin::can_handle_signature(const relation_signature & sig) {
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            if (!bv.is_bv_sort(sig[i]))
+                return false;
+        }
+        return true;
     }
-    relation_base * udoc_plugin::mk_empty(const relation_signature & s) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+    relation_base * udoc_plugin::mk_empty(const relation_signature & sig) {
+        return alloc(udoc_relation, *this, sig);
     }
     relation_base * udoc_plugin::mk_full(func_decl* p, const relation_signature & s) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        udoc_relation* r = get(mk_empty(s));
+        r->get_udoc().push_back(dm(s).allocateX());
+        return r;
     }
     class udoc_plugin::join_fn : public convenient_relation_join_fn {
         doc_manager& dm;
@@ -158,10 +165,10 @@ namespace datalog {
                 unsigned v1 = pos[idx1];
                 unsigned v2 = pos[idx2];
 
-                if (v1 == tbv::BIT_x) {
-                    if (v2 != tbv::BIT_x)
+                if (v1 == BIT_x) {
+                    if (v2 != BIT_x)
                         pos.set(idx1, v2);
-                } else if (v2 == tbv::BIT_x) {
+                } else if (v2 == BIT_x) {
                     pos.set(idx2, v1);
                 } else if (v1 != v2) {
                     dm.deallocate(d);
@@ -176,16 +183,16 @@ namespace datalog {
                 unsigned v1 = pos[idx1];
                 unsigned v2 = pos[idx2];
                 
-                if (v1 == tbv::BIT_x && v2 == tbv::BIT_x) {
+                if (v1 == BIT_x && v2 == BIT_x) {
                     // add to subtracted TBVs: 1xx0 and 0xx1
                     tbv* r = dm.tbv().allocate(pos);
-                    r->set(idx1, tbv::BIT_0);
-                    r->set(idx2, tbv::BIT_1);
+                    r->set(idx1, BIT_0);
+                    r->set(idx2, BIT_1);
                     neg.push_back(r);
                     
                     r = dm.tbv().allocate(pos);
-                    r->set(idx1, tbv::BIT_1);
-                    r->set(idx2, tbv::BIT_0);
+                    r->set(idx1, BIT_1);
+                    r->set(idx2, BIT_0);
                     neg.push_back(r);
                 }
             }
@@ -237,29 +244,119 @@ namespace datalog {
         NOT_IMPLEMENTED_YET();
         return 0;
     }
+
+    class udoc_plugin::rename_fn : public convenient_relation_rename_fn {
+        unsigned_vector m_permutation;
+    public:
+        rename_fn(const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) 
+            : convenient_relation_rename_fn(orig_sig, cycle_len, cycle) {
+            NOT_IMPLEMENTED_YET();
+            // compute permuation.
+        }
+
+        virtual relation_base * operator()(const relation_base & _r) {
+            udoc_relation const& r = get(_r);
+            udoc_plugin& p = r.get_plugin();            
+            relation_signature const& sig = get_result_signature();
+            udoc_relation* result = alloc(udoc_relation, p, sig);
+            udoc const& src = r.get_udoc();
+            udoc& dst = result->get_udoc();
+            doc_manager& dm = r.get_dm();
+            for (unsigned i = 0; i < src.size(); ++i) {
+                dst.push_back(dm.allocate(src[i], m_permutation.c_ptr()));
+            }
+            return result;
+        }
+    };
     relation_transformer_fn * udoc_plugin::mk_rename_fn(
-        const relation_base & t, unsigned permutation_cycle_len, 
-        const unsigned * permutation_cycle) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        const relation_base & r, 
+        unsigned cycle_len, const unsigned * permutation_cycle) {
+        if (check_kind(r)) {
+            return alloc(rename_fn, r.get_signature(), cycle_len, permutation_cycle);
+        }
+        else {
+            return 0;
+        }
+    }
+    class udoc_plugin::union_fn : public relation_union_fn {
+    public:
+        union_fn() {}
+
+        virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) {
+
+            TRACE("dl", _r.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
+
+            udoc_relation& r = get(_r);
+            udoc_relation const& src = get(_src);
+            udoc_relation* d = get(_delta);
+            udoc* d1 = 0;
+            if (d) d1 = &d->get_udoc();
+            r.get_plugin().mk_union(r.get_dm(), r.get_udoc(), src.get_udoc(), d1);
+        }
+    };
+    void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
+        for (unsigned i = 0; i < src.size(); ++i) {
+            doc* d = dm.allocate(src[i]);
+            if (dst.insert(dm, d)) {
+                if (delta) {
+                    delta->insert(dm, dm.allocate(src[i]));
+                }
+            } 
+        }
     }
     relation_union_fn * udoc_plugin::mk_union_fn(
         const relation_base & tgt, const relation_base & src, 
         const relation_base * delta) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
+            return 0;
+        }
+        return alloc(union_fn);
     }
     relation_union_fn * udoc_plugin::mk_widen_fn(
         const relation_base & tgt, const relation_base & src, 
         const relation_base * delta) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        return mk_union_fn(tgt, src, delta);
     }
+
+    class udoc_plugin::filter_identical_fn : public relation_mutator_fn {
+        unsigned_vector        m_cols;
+        unsigned               m_size;
+        bit_vector             m_empty_bv;
+        union_find_default_ctx union_ctx;
+        union_find<>           m_equalities;
+    public:
+        filter_identical_fn(const relation_base & _r, unsigned col_cnt, const unsigned *identical_cols)
+            : m_cols(col_cnt), m_equalities(union_ctx) {
+            udoc_relation const& r = get(_r);
+            doc_manager& dm = r.get_dm();
+            unsigned num_bits = dm.num_tbits();
+            m_size = r.column_num_bits(identical_cols[0]);
+            m_empty_bv.resize(r.get_num_bits(), false);
+            
+            for (unsigned i = 0; i < col_cnt; ++i) {
+                m_cols[i] = r.column_idx(identical_cols[i]);
+            }
+            
+            for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) {
+                m_equalities.mk_var();
+            }
+        }
+        
+        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);
+            }
+            TRACE("dl", tout << "final size: " << r.get_size_estimate_rows() << '\n';);
+        }
+    };
     relation_mutator_fn * udoc_plugin::mk_filter_identical_fn(
         const relation_base & t, unsigned col_cnt, 
         const unsigned * identical_cols) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        if (!check_kind(t))
+            return 0;
+        return alloc(filter_identical_fn, t, col_cnt, identical_cols);
     }
     relation_mutator_fn * udoc_plugin::mk_filter_equal_fn(
         const relation_base & t, const relation_element & value, unsigned col) {

src/muz/ddnf/udoc_relation.h

@@ -30,7 +30,7 @@ namespace datalog {
     class udoc_relation;
     
     class udoc_relation : public relation_base {
-        friend class udoc_relation;
+        friend class udoc_plugin;
         doc_manager&    dm;
         udoc            m_elems;
         unsigned_vector m_column_info;
@@ -53,6 +53,7 @@ namespace datalog {
         doc_manager& get_dm() const { return dm; }
         udoc const& get_udoc() const { return m_elems; }
         udoc& get_udoc() { return m_elems; }
+        unsigned get_num_records() const { return m_elems.size(); }
         unsigned get_num_bits() const { return m_column_info.back(); }
         unsigned get_num_cols() const { return m_column_info.size()-1; }
         unsigned column_idx(unsigned col) const { return m_column_info[col]; }
@@ -79,7 +80,7 @@ namespace datalog {
         static udoc_relation& get(relation_base& r);
         static udoc_relation* get(relation_base* r);
         static udoc_relation const & get(relation_base const& r);   
-
+        void mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta);
     public:
         udoc_plugin(relation_manager& rm);
         ~udoc_plugin();