From 2e083ab9c22efa75b31efe259fd74ac565bc65f5 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 29 Jan 2015 08:50:12 +0000 Subject: [PATCH] DoC: specialize union for the case dst=empty and/or delta=empty this avoids O(n^2) insert and becomes O(n) Signed-off-by: Nuno Lopes --- src/muz/rel/udoc_relation.cpp | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 90c3ec7c0..ffb4b6e22 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -509,13 +509,27 @@ namespace datalog { } }; 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)) { + bool deltaempty = delta ? delta->is_empty() : false; + + if (dst.is_empty()) { + for (unsigned i = 0; i < src.size(); ++i) { + dst.push_back(dm.allocate(src[i])); 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(