From 1787fa82965414ae9d5fd6cb0be5c0bc2571f095 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Dec 2016 20:54:09 -0800 Subject: [PATCH] remove redundant disjunction in compilation of at-most-1 constraints, log mutexes Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 1 + src/smt/theory_pb.cpp | 2 +- src/util/sorting_network.h | 61 +++++++++++++++++--------------------- 3 files changed, 30 insertions(+), 34 deletions(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 21537a570..f31009bbf 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -206,6 +206,7 @@ namespace opt { rational w = weights[i]; weight = w - weight; m_lower += weight*rational(i); + IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";); sum2 += weight*rational(i+1); new_soft.insert(soft, weight); for (; i > 0 && weights[i-1] == w; --i) {} diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index a2f8ceba9..5dd870b48 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -518,7 +518,7 @@ namespace smt { ++log; n *= 2; } - unsigned th = args.size()*log; + unsigned th = args.size()*log*log; c->m_compilation_threshold = th; IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threshold to " << th << ")\n";); TRACE("pb", tout << "compilation threshold: " << th << "\n";); diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index 2c819db04..b0efbd346 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -164,11 +164,27 @@ Notes: struct stats { unsigned m_num_compiled_vars; unsigned m_num_compiled_clauses; + unsigned m_num_clause_vars; void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } }; stats m_stats; + struct scoped_stats { + stats& m_stats; + stats m_save; + unsigned m_k, m_n; + scoped_stats(stats& st, unsigned k, unsigned n): m_stats(st), m_save(st), m_k(k), m_n(n) {} + ~scoped_stats() { + IF_VERBOSE(1, + verbose_stream() << "k: " << m_k << " n: " << m_n; + verbose_stream() << " clauses: " << m_stats.m_num_compiled_clauses - m_save.m_num_compiled_clauses; + verbose_stream() << " vars: " << m_stats.m_num_clause_vars - m_save.m_num_clause_vars; + verbose_stream() << " clauses: " << m_stats.m_num_compiled_clauses; + verbose_stream() << " vars: " << m_stats.m_num_clause_vars << "\n";); + } + }; + psort_nw(psort_expr& c): ctx(c) {} literal ge(bool full, unsigned k, unsigned n, literal const* xs) { @@ -186,6 +202,7 @@ Notes: else { SASSERT(2*k <= n); m_t = full?GE_FULL:GE; + // scoped_stats _ss(m_stats, k, n); psort_nw::card(k, n, xs, out); return out[k-1]; } @@ -202,11 +219,13 @@ Notes: } else if (k == 1) { literal_vector ors; - return mk_at_most_1(full, n, xs, ors); + // scoped_stats _ss(m_stats, k, n); + return mk_at_most_1(full, n, xs, ors, false); } else { SASSERT(2*k <= n); m_t = full?LE_FULL:LE; + // scoped_stats _ss(m_stats, k, n); card(k + 1, n, xs, out); return ctx.mk_not(out[k]); } @@ -222,9 +241,11 @@ Notes: return eq(full, k, n, in.c_ptr()); } else if (k == 1) { + // scoped_stats _ss(m_stats, k, n); return mk_exactly_1(full, n, xs); } else { + // scoped_stats _ss(m_stats, k, n); SASSERT(2*k <= n); m_t = EQ; card(k+1, n, xs, out); @@ -304,7 +325,7 @@ Notes: literal mk_exactly_1(bool full, unsigned n, literal const* xs) { literal_vector ors; - literal r1 = mk_at_most_1(full, n, xs, ors); + literal r1 = mk_at_most_1(full, n, xs, ors, true); if (full) { r1 = mk_and(r1, mk_or(ors)); @@ -315,8 +336,7 @@ Notes: return r1; } -#if 1 - literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors) { + literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors, bool use_ors) { TRACE("pb", tout << (full?"full":"partial") << " "; for (unsigned i = 0; i < n; ++i) tout << xs[i] << " "; tout << "\n";); @@ -336,7 +356,9 @@ Notes: for (unsigned i = 0; i < n; i += inc_size) { unsigned inc = std::min(n - i, inc_size); mk_at_most_1_small(full, inc, in.c_ptr() + i, result, ands); - ors.push_back(mk_or(inc, in.c_ptr() + i)); + if (use_ors || n > inc_size) { + ors.push_back(mk_or(inc, in.c_ptr() + i)); + } } if (n <= inc_size) { break; @@ -349,35 +371,7 @@ Notes: } return result; } -#else - literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors) { - TRACE("pb", tout << (full?"full":"partial") << " "; - for (unsigned i = 0; i < n; ++i) tout << xs[i] << " "; - tout << "\n";); - literal_vector in(n, xs); - unsigned inc_size = 4; - literal_vector ands; - while (!in.empty()) { - ors.reset(); - unsigned i = 0; - unsigned n = in.size(); - if (n + 1 == inc_size) ++inc_size; - for (; i < n; i += inc_size) { - unsigned inc = std::min(inc_size, n - i); - ands.push_back(mk_at_most_1_small(inc, in.c_ptr() + i)); - ors.push_back(mk_or(inc, in.c_ptr() + i)); - } - if (n <= inc_size) { - break; - } - in.reset(); - in.append(ors); - } - return mk_and(ands); - } - -#endif void mk_at_most_1_small(bool full, unsigned n, literal const* xs, literal result, literal_vector& ands) { SASSERT(n > 0); if (n == 1) { @@ -562,6 +556,7 @@ Notes: } void add_clause(unsigned n, literal const* ls) { m_stats.m_num_compiled_clauses++; + m_stats.m_num_clause_vars += n; literal_vector tmp(n, ls); TRACE("pb", for (unsigned i = 0; i < n; ++i) tout << ls[i] << " "; tout << "\n";); ctx.mk_clause(n, tmp.c_ptr());