mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fuse join with projection avoiding double insert (but at cost of double projection)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-01-25 04:37:42 -08:00
parent 761c7d9a40
commit 37fca65517
1 changed files with 14 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/muz/rel/udoc_relation.cpp
View file

@ -1001,7 +1001,6 @@ namespace datalog {
relation_signature prod_signature;
prod_signature.append(t1.get_signature());
prod_signature.append(t2.get_signature());
udoc prod;
udoc const& d1 = t1.get_udoc();
udoc const& d2 = t2.get_udoc();
doc_manager& dm1 = t1.get_dm();
@ -1011,13 +1010,22 @@ namespace datalog {
udoc_relation* result = get(p.mk_empty(get_result_signature()));
udoc& res = result->get_udoc();
doc_manager& dm_res = result->get_dm();
prod.join(d1, d2, dm_prod, dm1, m_cols1, m_cols2);
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]));
for (unsigned i = 0; i < d1.size(); ++i) {
for (unsigned j = 0; j < d2.size(); ++j) {
doc_ref d(dm_prod, dm_prod.join(d1[i], d2[j], dm1, m_cols1, m_cols2));
if (d) {
res.insert(dm_res, dm_prod.project(dm_res, m_to_delete, *d));
IF_VERBOSE(2,
if (res.size() > 0 && 0 == res.size() % 10000) {
verbose_stream() << "result size: " << res.size()
<< " i:" << i << " j:" << j << " "
<< 100*i/d1.size() << "% complete\n";
});
}
}
}
TRACE("doc", result->display(tout););
prod.reset(dm_prod);
return result;
}
};