Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

src/muz/rel/doc.cpp

@@ -411,6 +411,81 @@ doc* doc_manager::project(doc_manager& dstm, bit_vector const& to_delete, doc co
     return r;
 }
 
+doc* doc_manager::join(const doc& d1, const doc& d2, doc_manager& dm1,
+                       const unsigned_vector& cols1,
+                       const unsigned_vector& cols2) {
+    doc_ref d(*this, allocateX());
+    tbv_ref t(m);
+    tbv& pos = d->pos();
+    utbv& neg = d->neg();
+    unsigned mid = dm1.num_tbits();
+    unsigned hi = num_tbits();
+    m.set(pos, d1.pos(), mid - 1, 0);
+    m.set(pos, d2.pos(), hi - 1, mid);
+    SASSERT(well_formed(*d));
+
+    // first fix bits
+    for (unsigned i = 0; i < cols1.size(); ++i) {
+        unsigned idx1 = cols1[i];
+        unsigned idx2 = mid + cols2[i];
+        tbit v1 = pos[idx1];
+        tbit v2 = pos[idx2];
+
+        if (v1 == BIT_x) {
+            if (v2 != BIT_x)
+                m.set(pos, idx1, v2);
+        }
+        else if (v2 == BIT_x) {
+            m.set(pos, idx2, v1);
+        }
+        else if (v1 != v2) {
+            // columns don't match
+            return 0;
+        }
+        SASSERT(well_formed(*d));
+    }
+
+    // fix equality of don't care columns
+    for (unsigned i = 0; i < cols1.size(); ++i) {
+        unsigned idx1 = cols1[i];
+        unsigned idx2 = mid + cols2[i];
+        unsigned v1 = pos[idx1];
+        unsigned v2 = pos[idx2];
+
+        if (v1 == BIT_x && v2 == BIT_x) {
+            // add to subtracted TBVs: 1xx0 and 0xx1
+            t = m.allocate(pos);
+            m.set(*t, idx1, BIT_0);
+            m.set(*t, idx2, BIT_1);
+            neg.push_back(t.detach());
+            t = m.allocate(pos);
+            m.set(*t, idx1, BIT_1);
+            m.set(*t, idx2, BIT_0);
+            neg.push_back(t.detach());
+        }
+        SASSERT(well_formed(*d));
+    }
+
+    // handle subtracted TBVs:  1010 -> 1010xxx
+    for (unsigned i = 0; i < d1.neg().size(); ++i) {
+        t = m.allocateX();
+        m.set(*t, d1.neg()[i], mid - 1, 0);
+        if (m.set_and(*t, pos))
+            neg.push_back(t.detach());
+        SASSERT(well_formed(*d));
+    }
+    for (unsigned i = 0; i < d2.neg().size(); ++i) {
+        t = m.allocateX();
+        m.set(*t, d2.neg()[i], hi - 1, mid);
+        if (m.set_and(*t, pos))
+            neg.push_back(t.detach());
+        SASSERT(well_formed(*d));
+    }
+    SASSERT(well_formed(*d));
+
+    return d.detach();
+}
+
 doc_manager::project_action_t 
 doc_manager::pick_resolvent(
     tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx) {

src/muz/rel/doc.h

@@ -91,6 +91,8 @@ public:
     bool well_formed(doc const& d) const;
     bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
     void set(doc& d, unsigned idx, tbit value);
+    doc* join(const doc& a, const doc& b, doc_manager& dm1,
+        const unsigned_vector& cols1, const unsigned_vector& cols2);
 
     void verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst);
 private:
@@ -314,6 +316,16 @@ public:
         }
     }
 
+    void join(const union_bvec& d1, const union_bvec& d2, M& dm, M& dm1,
+              const unsigned_vector& cols1, const unsigned_vector& cols2) {
+        for (unsigned i = 0; i < d1.size(); ++i) {
+            for (unsigned j = 0; j < d2.size(); ++j) {
+                if (T *d = dm.join(d1[i], d2[j], dm1, cols1, cols2))
+                    insert(dm, d);
+            }
+        }
+    }
+
 };
 
 
@@ -367,6 +379,7 @@ public:
     doc& operator*() { return *d; }
     doc* operator->() { return d; }
     doc* detach() { doc* r = d; d = 0; return r; }
+    operator bool() const { return d != 0; }
 };
 
 #endif /* _DOC_H_ */

src/muz/rel/product_set.cpp

@@ -30,7 +30,7 @@ namespace datalog {
     product_set::product_set(
         product_set_plugin& p, relation_signature const& s, 
         initial_t init, T const& t):
-        vector_relation(p, s, false, t), m_refs(0) {
+        vector_relation<bit_vector>(p, s, false, t), m_refs(0) {
         unsigned delta = 0;
         for (unsigned i = 0; i < s.size(); ++i) {
             unsigned sz = p.set_size(s[i]);

src/muz/rel/udoc_relation.cpp

@@ -314,96 +314,17 @@ namespace datalog {
         doc_manager& dm;
         doc_manager& dm1;
         doc_manager& dm2;
-        unsigned_vector m_orig_cols1;
-        unsigned_vector m_orig_cols2;
     public:
         join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt,
                 const unsigned * cols1, const unsigned * cols2) 
             : convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2),
               dm(p.dm(get_result_signature())),
               dm1(t1.get_dm()),
-              dm2(t2.get_dm()),
+              dm2(t2.get_dm()) {
-              m_orig_cols1(m_cols1),
-              m_orig_cols2(m_cols2) {
             t1.expand_column_vector(m_cols1);
             t2.expand_column_vector(m_cols2);
         }
 
-        void join(doc const& d1, doc const& d2, udoc& result) {
-            doc_ref d(dm);
-            tbv_ref t(dm.tbvm());
-            d = dm.allocateX();
-            tbv& pos = d->pos();
-            utbv& neg = d->neg();
-            unsigned mid = dm1.num_tbits();
-            unsigned hi  = dm.num_tbits();
-            dm.tbvm().set(pos,d1.pos(), mid-1, 0);
-            dm.tbvm().set(pos,d2.pos(), hi-1, mid);
-            SASSERT(dm.well_formed(*d));
-            // first fix bits
-            for (unsigned i = 0; i < m_cols1.size(); ++i) {
-                unsigned idx1 = m_cols1[i];
-                unsigned idx2 = mid + m_cols2[i];
-                tbit v1 = pos[idx1];
-                tbit v2 = pos[idx2];
-
-                if (v1 == BIT_x) {
-                    if (v2 != BIT_x)
-                        dm.tbvm().set(pos, idx1, v2);
-                } 
-                else if (v2 == BIT_x) {
-                    dm.tbvm().set(pos, idx2, v1);
-                } 
-                else if (v1 != v2) {
-                    // columns don't match
-                    return;
-                }
-                SASSERT(dm.well_formed(*d));
-            }
-            // fix equality of don't care columns
-            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];
-                
-                if (v1 == BIT_x && v2 == BIT_x) {
-                    // add to subtracted TBVs: 1xx0 and 0xx1
-                    t = dm.tbvm().allocate(pos);
-                    dm.tbvm().set(*t, idx1, BIT_0);
-                    dm.tbvm().set(*t, idx2, BIT_1);
-                    neg.push_back(t.detach());                    
-                    t = dm.tbvm().allocate(pos);
-                    dm.tbvm().set(*t, idx1, BIT_1);
-                    dm.tbvm().set(*t, idx2, BIT_0);
-                    neg.push_back(t.detach());
-                }
-                SASSERT(dm.well_formed(*d));
-            }
-
-            // handle subtracted TBVs:  1010 -> 1010xxx
-            for (unsigned i = 0; i < d1.neg().size(); ++i) {
-                t = dm.tbvm().allocate();
-                dm.tbvm().set(*t, d1.neg()[i], mid - 1, 0);
-                dm.tbvm().set(*t, d2.pos(),    hi -  1, mid);
-                if (dm.tbvm().set_and(*t, pos)) {
-                    neg.push_back(t.detach());
-                }
-                SASSERT(dm.well_formed(*d));
-            }
-            for (unsigned i = 0; i < d2.neg().size(); ++i) {
-                t = dm.tbvm().allocate();
-                dm.tbvm().set(*t, d1.pos(),    mid- 1, 0);
-                dm.tbvm().set(*t, d2.neg()[i], hi - 1, mid);
-                if (dm.tbvm().set_and(*t, pos)) {
-                    neg.push_back(t.detach());
-                }
-                SASSERT(dm.well_formed(*d));
-            }            
-            SASSERT(dm.well_formed(*d));
-            result.insert(dm, d.detach());
-        }
-
         virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) {
             udoc_relation const& r1 = get(_r1);
             udoc_relation const& r2 = get(_r2);
@@ -414,11 +335,7 @@ namespace datalog {
             udoc const& d1 = r1.get_udoc();
             udoc const& d2 = r2.get_udoc();
             udoc& r = result->get_udoc();
-            for (unsigned i = 0; i < d1.size(); ++i) {
+            r.join(d1, d2, dm, dm1, m_cols1, m_cols2);
-                for (unsigned j = 0; j < d2.size(); ++j) {
-                    join(d1[i], d2[j], r);
-                }
-            }
             TRACE("doc", result->display(tout << "result:\n"););
             IF_VERBOSE(3, result->display(verbose_stream() << "join result:\n"););
             SASSERT(r.well_formed(result->get_dm()));
@@ -1031,10 +948,7 @@ namespace datalog {
 #if 0
         udoc_plugin::join_fn   m_joiner;
 #endif
-        union_find_default_ctx union_ctx;
         bit_vector             m_to_delete; 
-        subset_ints            m_equalities;
-        unsigned_vector        m_roots;
 
     public:
         join_project_fn(
@@ -1044,32 +958,22 @@ namespace datalog {
             : convenient_relation_join_project_fn(
                 t1.get_signature(), t2.get_signature(), 
                 col_cnt, cols1, cols2,
-                removed_col_cnt, rm_cols),
+                removed_col_cnt, rm_cols)
 #if 0
-              m_joiner(t1.get_plugin(), t1, t2, col_cnt, cols1, cols2),
+              , m_joiner(t1.get_plugin(), t1, t2, col_cnt, cols1, cols2)
 #endif
-              m_equalities(union_ctx)
         {
             udoc_plugin& p = t1.get_plugin();
             unsigned num_bits1 = t1.get_num_bits();
             unsigned num_bits = num_bits1 + t2.get_num_bits();
             unsigned_vector removed_cols(removed_col_cnt, rm_cols);
-            unsigned_vector expcols1(col_cnt, cols1);
-            unsigned_vector expcols2(col_cnt, cols2);
             t1.expand_column_vector(removed_cols, &t2);
-            t1.expand_column_vector(expcols1);
+            t1.expand_column_vector(m_cols1);
-            t2.expand_column_vector(expcols2);
+            t2.expand_column_vector(m_cols2);
             m_to_delete.resize(num_bits, false);
-            for (unsigned i = 0; i < num_bits; ++i) {
-                m_equalities.mk_var();
-            }
             for (unsigned i = 0; i < removed_cols.size(); ++i) {
                 m_to_delete.set(removed_cols[i], true);
             }
-            for (unsigned i = 0; i < expcols1.size(); ++i) {
-                m_equalities.merge(expcols1[i], expcols2[i] + num_bits1);                
-            }
-            m_roots.append(expcols1);
         }
 
 
@@ -1107,13 +1011,7 @@ namespace datalog {
             udoc_relation* result = get(p.mk_empty(get_result_signature()));
             udoc& res = result->get_udoc();
             doc_manager& dm_res  = result->get_dm();            
-            for (unsigned i = 0; i < d1.size(); ++i) {
+            prod.join(d1, d2, dm_prod, dm1, m_cols1, m_cols2);
-                for (unsigned j = 0; j < d2.size(); ++j) {
-                    prod.push_back(xprod(dm_prod, dm1, dm2, d1[i], d2[j]));
-                }
-            }
-            TRACE("doc", prod.display(dm_prod, tout) << "\n";);
-            prod.merge(dm_prod, m_roots, m_equalities, m_to_delete);
             TRACE("doc", prod.display(dm_prod, tout) << "\n";);
             for (unsigned i = 0; i < prod.size(); ++i) {
                 res.insert(dm_res, dm_prod.project(dm_res, m_to_delete, prod[i]));
@@ -1122,38 +1020,6 @@ namespace datalog {
             prod.reset(dm_prod);
             return result;            
         }
-        doc* xprod(doc_manager& dm, doc_manager& dm1, doc_manager& dm2,
-                   doc const& d1, doc const& d2) {
-            tbv_manager& tbm = dm.tbvm();
-            doc_ref d(dm);
-            tbv_ref t(tbm);
-            d = dm.allocateX();
-            tbv& pos = d->pos();
-            utbv& neg = d->neg();
-            unsigned mid = dm1.num_tbits();
-            unsigned hi  = dm.num_tbits();
-            tbm.set(pos, d1.pos(), mid-1, 0);
-            tbm.set(pos, d2.pos(), hi-1, mid);
-            for (unsigned i = 0; i < d1.neg().size(); ++i) {
-                t = tbm.allocateX();
-                tbm.set(*t, d1.neg()[i], mid-1, 0);
-                VERIFY(tbm.set_and(*t, pos));
-                neg.push_back(t.detach());
-            }
-            for (unsigned i = 0; i < d2.neg().size(); ++i) {
-                t = tbm.allocateX();
-                tbm.set(*t, d2.neg()[i], hi-1, mid);
-                VERIFY(tbm.set_and(*t, pos));
-                neg.push_back(t.detach());
-            }
-            SASSERT(dm.well_formed(*d));
-            TRACE("doc", 
-                  dm1.display(tout, d1) << "\n";
-                  dm2.display(tout, d2) << "\n";
-                  dm.display(tout, *d) << "\n";);
-            return d.detach();
-        }
-
     };