From 54e3b5ee0d3d2493dbe5f75103184a8d58d71fef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Feb 2014 23:30:14 -0800 Subject: [PATCH] further tuning pb Signed-off-by: Nikolaj Bjorner --- src/math/simplex/simplex.h | 14 +++++-- src/math/simplex/simplex_def.h | 8 ++++ src/math/simplex/sparse_matrix.h | 11 ++++++ src/math/simplex/sparse_matrix_def.h | 11 +++++- src/smt/theory_pb.cpp | 55 +++++++++++++++------------- src/smt/theory_pb.h | 10 ++--- 6 files changed, 74 insertions(+), 35 deletions(-) diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index 985d6c608..0ea3bebf0 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -50,16 +50,21 @@ namespace simplex { typedef typename Ext::eps_manager eps_manager; typedef typename Ext::scoped_numeral scoped_numeral; typedef _scoped_numeral scoped_eps_numeral; - typedef typename _scoped_numeral_vector scoped_eps_numeral_vector; - typedef sparse_matrix matrix; - struct var_lt { bool operator()(var_t v1, var_t v2) const { return v1 < v2; } }; typedef heap var_heap; + struct stats { + unsigned m_num_pivots; + stats() { reset(); } + void reset() { + memset(this, sizeof(*this), 0); + } + }; + enum pivot_strategy_t { S_BLAND, S_GREATEST_ERROR, @@ -99,6 +104,7 @@ namespace simplex { uint_set m_left_basis; unsigned m_infeasible_var; unsigned_vector m_base_vars; + stats m_stats; public: simplex(): @@ -144,6 +150,8 @@ namespace simplex { row_iterator row_begin(row const& r) { return M.row_begin(r); } row_iterator row_end(row const& r) { return M.row_end(r); } + void collect_statistics(::statistics & st) const; + private: var_t select_var_to_fix(); diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 51405aef5..ab416e042 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -306,6 +306,7 @@ namespace simplex { template void simplex::pivot(var_t x_i, var_t x_j, numeral const& a_ij) { + ++m_stats.m_num_pivots; var_info& x_iI = m_vars[x_i]; var_info& x_jI = m_vars[x_j]; unsigned r_i = x_iI.m_base2row; @@ -868,6 +869,13 @@ namespace simplex { return true; } + template + void simplex::collect_statistics(::statistics & st) const { + M.collect_statistics(st); + st.update("simplex num pivots", m_stats.m_num_pivots); + } + + }; #endif diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index e3c00e511..b711c91af 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -20,6 +20,7 @@ Notes: #define _SPARSE_MATRIX_H_ #include "mpq_inf.h" +#include "statistics.h" namespace simplex { @@ -39,6 +40,14 @@ namespace simplex { private: + struct stats { + unsigned m_add_rows; + stats() { reset(); } + void reset() { + memset(this, sizeof(*this), 0); + } + }; + static const int dead_id = -1; /** @@ -126,6 +135,7 @@ namespace simplex { vector m_columns; // per var svector m_var_pos; // temporary map from variables to positions in row unsigned_vector m_var_pos_idx; // indices in m_var_pos + stats m_stats; bool well_formed_row(unsigned row_id) const; bool well_formed_column(unsigned column_id) const; @@ -238,6 +248,7 @@ namespace simplex { void display_row(std::ostream& out, row const& r); bool well_formed() const; + void collect_statistics(::statistics & st) const; }; diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index e62fc6c41..561025303 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -322,7 +322,7 @@ namespace simplex { */ template void sparse_matrix::add(row row1, numeral const& n, row row2) { - // m_stats.m_add_rows++; + m_stats.m_add_rows++; _row & r1 = m_rows[row1.id()]; _row & r2 = m_rows[row2.id()]; @@ -547,6 +547,15 @@ namespace simplex { return true; } + /** + \brief statistics + */ + template + void sparse_matrix::collect_statistics(::statistics & st) const { + st.update("simplex add rows", m_stats.m_add_rows); + } + + /** \brief display method */ diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index cd2891474..bc21ed243 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -723,6 +723,7 @@ namespace smt { st.update("pb compilations", m_stats.m_num_compiles); st.update("pb compiled clauses", m_stats.m_num_compiled_clauses); st.update("pb compiled vars", m_stats.m_num_compiled_vars); + m_simplex.collect_statistics(st); } void theory_pb::reset_eh() { @@ -979,10 +980,10 @@ namespace smt { literal l = c.lit(); lbool asgn = ctx.get_assignment(l); - if (c.max_sum() < c.k() && asgn == l_false) { + if (c.max_sum() < c.mpz_k() && asgn == l_false) { return; } - if (c.is_ge() && c.min_sum() >= c.k() && asgn == l_true) { + if (c.is_ge() && c.min_sum() >= c.mpz_k() && asgn == l_true) { return; } for (i = 0; i < c.size(); ++i) { @@ -1003,11 +1004,11 @@ namespace smt { c.m_min_sum += c.ncoeff(i); } DEBUG_CODE( - numeral sum(0); - numeral maxs(0); + scoped_mpz sum(m_mpz_mgr); + scoped_mpz maxs(m_mpz_mgr); for (unsigned i = 0; i < c.size(); ++i) { - if (ctx.get_assignment(c.lit(i)) == l_true) sum += c.coeff(i); - if (ctx.get_assignment(c.lit(i)) != l_false) maxs += c.coeff(i); + if (ctx.get_assignment(c.lit(i)) == l_true) sum += c.ncoeff(i); + if (ctx.get_assignment(c.lit(i)) != l_false) maxs += c.ncoeff(i); } CTRACE("pb", (maxs > c.max_sum()), display(tout, c, true);); SASSERT(c.min_sum() <= sum); @@ -1015,32 +1016,32 @@ namespace smt { SASSERT(maxs <= c.max_sum()); ); SASSERT(c.min_sum() <= c.max_sum()); - SASSERT(!c.min_sum().is_neg()); + SASSERT(!m_mpz_mgr.is_neg(c.min_sum())); ctx.push_trail(value_trail(c.m_nfixed)); ++c.m_nfixed; SASSERT(c.nfixed() <= c.size()); - if (c.is_ge() && c.min_sum() >= c.k() && asgn != l_true) { + if (c.is_ge() && c.min_sum() >= c.mpz_k() && asgn != l_true) { TRACE("pb", display(tout << "Set " << l << "\n", c, true);); add_assign(c, get_helpful_literals(c, false), l); } - else if (c.max_sum() < c.k() && asgn != l_false) { + else if (c.max_sum() < c.mpz_k() && asgn != l_false) { TRACE("pb", display(tout << "Set " << ~l << "\n", c, true);); add_assign(c, get_unhelpful_literals(c, true), ~l); } - else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() == c.k() && asgn != l_true) { + else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() == c.mpz_k() && asgn != l_true) { TRACE("pb", display(tout << "Set " << l << "\n", c, true);); add_assign(c, get_all_literals(c, false), l); } - else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() != c.k() && asgn != l_false) { + else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() != c.mpz_k() && asgn != l_false) { TRACE("pb", display(tout << "Set " << ~l << "\n", c, true);); add_assign(c, get_all_literals(c, false), ~l); } #if 0 - else if (c.is_eq() && c.min_sum() > c.k() && asgn != l_false) { + else if (c.is_eq() && c.min_sum() > c.mpz_k() && asgn != l_false) { TRACE("pb", display(tout << "Set " << ~l << "\n", c, true);); add_assign(c, get_all_literals(c, false), ~l); } - else if (c.is_eq() && asgn == l_true && c.min_sum() == c.k() && c.max_sum() > c.k()) { + else if (c.is_eq() && asgn == l_true && c.min_sum() == c.mpz_k() && c.max_sum() > c.mpz_k()) { literal_vector& lits = get_all_literals(c, false); lits.push_back(c.lit()); for (unsigned i = 0; i < c.size(); ++i) { @@ -1076,17 +1077,19 @@ namespace smt { // Adjust set of watched literals. // - numeral k = c.k(); - numeral coeff = c.coeff(w); - bool add_more = c.watch_sum() - coeff < k + c.max_watch(); + scoped_mpz k_coeff(m_mpz_mgr), k(m_mpz_mgr); + k = c.mpz_k(); + k_coeff = k; + k_coeff += c.ncoeff(w); + bool add_more = c.watch_sum() < k_coeff + c.max_watch(); for (unsigned i = c.watch_size(); add_more && i < c.size(); ++i) { if (ctx.get_assignment(c.lit(i)) != l_false) { add_watch(c, i); - add_more = c.watch_sum() - coeff < k + c.max_watch(); + add_more = c.watch_sum() < k_coeff + c.max_watch(); } } - if (c.watch_sum() - coeff < k) { + if (c.watch_sum() < k_coeff) { // // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0 // create clause x1 or x2 or ~L @@ -1113,9 +1116,10 @@ namespace smt { literal_vector& lits = get_unhelpful_literals(c, true); lits.push_back(c.lit()); - numeral deficit = c.watch_sum() - k; + scoped_mpz deficit(m_mpz_mgr); + deficit = c.watch_sum() - k; for (unsigned i = 0; i < c.size(); ++i) { - if (ctx.get_assignment(c.lit(i)) == l_undef && deficit < c.coeff(i)) { + if (ctx.get_assignment(c.lit(i)) == l_undef && deficit < c.ncoeff(i)) { DEBUG_CODE(validate_assign(c, lits, c.lit(i));); add_assign(c, lits, c.lit(i)); // break; @@ -1770,16 +1774,15 @@ namespace smt { void theory_pb::validate_watch(ineq const& c) const { context& ctx = get_context(); - numeral sum = numeral::zero(); - numeral max = numeral::zero(); + scoped_mpz sum(m_mpz_mgr), max(m_mpz_mgr); for (unsigned i = 0; i < c.watch_size(); ++i) { - sum += c.coeff(i); - if (c.coeff(i) > max) { - max = c.coeff(i); + sum += c.ncoeff(i); + if (max < c.ncoeff(i)) { + max = c.ncoeff(i); } } SASSERT(c.watch_sum() == sum); - SASSERT(sum >= c.k()); + SASSERT(sum >= c.mpz_k()); SASSERT(max == c.max_watch()); } diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 28257713e..5aea94999 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -142,14 +142,14 @@ namespace smt { unsigned size() const { return args().size(); } - class mpz const& watch_sum() const { return m_watch_sum; } - class mpz const& max_watch() const { return m_max_watch.get(); } + scoped_mpz const& watch_sum() const { return m_watch_sum; } + scoped_mpz const& max_watch() const { return m_max_watch; } void set_max_watch(mpz const& n) { m_max_watch = n; } unsigned watch_size() const { return m_watch_sz; } // variable watch infrastructure - class mpz const& min_sum() const { return m_min_sum; } - class mpz const& max_sum() const { return m_max_sum; } + scoped_mpz const& min_sum() const { return m_min_sum; } + scoped_mpz const& max_sum() const { return m_max_sum; } unsigned nfixed() const { return m_nfixed; } bool vwatch_initialized() const { return !m_mpz.is_zero(max_sum()); } void vwatch_reset() { m_min_sum.reset(); m_max_sum.reset(); m_nfixed = 0; } @@ -205,7 +205,7 @@ namespace smt { literal_vector m_explain_lower; // Simplex: explanations for lower bounds literal_vector m_explain_upper; // Simplex: explanations for upper bounds unsynch_mpq_inf_manager m_mpq_inf_mgr; // Simplex: manage inf_mpq numerals - unsynch_mpz_manager m_mpz_mgr; // Simplex: manager mpz numerals + mutable unsynch_mpz_manager m_mpz_mgr; // Simplex: manager mpz numerals unsigned_vector m_ineqs_trail; unsigned_vector m_ineqs_lim; literal_vector m_literals; // temporary vector