mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

DoC: specialize union for the case dst=empty and/or delta=empty

Browse source 
this avoids O(n^2) insert and becomes O(n)

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-01-29 08:50:12 +00:00
parent 1701af9dc9
commit 2e083ab9c2
1 changed files with 19 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -509,13 +509,27 @@ namespace datalog {
} }
}; };
void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) { void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
for (unsigned i = 0; i < src.size(); ++i) { bool deltaempty = delta ? delta->is_empty() : false;
doc* d = dm.allocate(src[i]);
if (dst.insert(dm, d)) { if (dst.is_empty()) {
for (unsigned i = 0; i < src.size(); ++i) {
dst.push_back(dm.allocate(src[i]));
if (delta) { if (delta) {
delta->insert(dm, dm.allocate(src[i])); if (deltaempty)
delta->push_back(dm.allocate(src[i]));
else
delta->insert(dm, dm.allocate(src[i]));
} }
} }
} else {
for (unsigned i = 0; i < src.size(); ++i) {
if (dst.insert(dm, dm.allocate(src[i])) && delta) {
if (deltaempty)
delta->push_back(dm.allocate(src[i]));
else
delta->insert(dm, dm.allocate(src[i]));
}
}
} }
} }
relation_union_fn * udoc_plugin::mk_union_fn( relation_union_fn * udoc_plugin::mk_union_fn(