From e1e27f2c26474a15607e3aa92691e25949c3064f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Oct 2014 10:17:20 -0700 Subject: [PATCH] optimize the merge function Signed-off-by: Nikolaj Bjorner --- src/muz/rel/doc.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index e87143482..76098b0d3 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -255,8 +255,20 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints const& equalities, while (idx != root); } else { + bool all_x = true; + if (!d.neg().is_empty()) { + idx = root; + do { + for (unsigned i = 0; all_x && i < d.neg().size(); ++i) { + all_x = (BIT_x == d.neg()[i][idx]); + } + idx = equalities.next(idx); + } + while (idx != root && all_x); + } + idx = root; do { - if (/*!discard_cols.get(idx) &&*/ idx != root1) { + if ((!discard_cols.get(idx) || !all_x) && idx != root1) { tbv* t = m.allocate(d.pos()); m.set(*t, idx, BIT_0); m.set(*t, root1, BIT_1);