diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 5df2fed80..6143f4085 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -938,12 +938,17 @@ namespace datalog { else if (m.is_not(g, e1)) { udoc sub; sub.push_back(dm.allocateX()); - apply_guard(e1, sub, equalities, discard_cols); - TRACE("doc", - result.display(dm, tout << "result0:") << "\n"; - sub.display(dm, tout << "sub:") << "\n";); + // TODO: right now we state that no columns are discarded to avoid + // silent column merging. This can be optimized if the set of merged + // columns is returned so that here we remove different columns. + bit_vector empty; + empty.resize(discard_cols.size(), false); + apply_guard(e1, sub, equalities, empty); result.subtract(dm, sub); result.simplify(dm); + TRACE("doc", + result.display(dm, tout << "result0:") << "\n"; + sub.display(dm, tout << "sub:") << "\n";); sub.reset(dm); TRACE("doc", result.display(dm, tout << "result:") << "\n";); } diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 834ce1bba..d7f83f0aa 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -376,15 +376,31 @@ public: unsigned_vector remove; remove.push_back(0); remove.push_back(2); + t1 = mk_full(sig2); + apply_filter(*t1, conds[2].get()); + apply_filter_project(*t1, remove, conds[2].get()); + apply_filter_project(*t1, remove, conds[3].get()); + t1->deallocate(); + + t1 = mk_full(sig2); + apply_filter(*t1, conds[3].get()); + apply_filter_project(*t1, remove, conds[2].get()); + apply_filter_project(*t1, remove, conds[3].get()); + t1->deallocate(); + for (unsigned i = 0; i < conds.size(); ++i) { + t1 = mk_full(sig2); apply_filter_project(*t1, remove, conds[i].get()); + t1->deallocate(); } + remove[1] = 1; for (unsigned i = 0; i < conds.size(); ++i) { + t1 = mk_full(sig2); apply_filter_project(*t1, remove, conds[i].get()); + t1->deallocate(); } - t1->deallocate(); }