From 5427964c54ced9c3b4dfd0eff854005ee9be5bb3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Jun 2014 14:08:55 -0700 Subject: [PATCH] use approximate hitting set implementation Signed-off-by: Nikolaj Bjorner --- src/opt/hitting_sets.cpp | 250 +++++++++++++++++++++++++++++++---- src/opt/hitting_sets.h | 10 +- src/opt/weighted_maxsat.cpp | 145 +++++--------------- src/sat/sat_asymm_branch.cpp | 2 +- src/sat/sat_asymm_branch.h | 2 +- src/sat/sat_cleaner.cpp | 2 +- src/sat/sat_cleaner.h | 2 +- src/sat/sat_probing.cpp | 2 +- src/sat/sat_probing.h | 2 +- src/sat/sat_scc.cpp | 2 +- src/sat/sat_scc.h | 2 +- src/sat/sat_simplifier.cpp | 2 +- src/sat/sat_simplifier.h | 2 +- src/sat/sat_solver.cpp | 2 +- src/sat/sat_solver.h | 2 +- 15 files changed, 273 insertions(+), 156 deletions(-) diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp index 7ef2eadc6..62b36961b 100644 --- a/src/opt/hitting_sets.cpp +++ b/src/opt/hitting_sets.cpp @@ -22,6 +22,7 @@ Notes: #include "simplex.h" #include "sparse_matrix_def.h" #include "simplex_def.h" +#include "sat_solver.h" typedef simplex::simplex Simplex; typedef simplex::sparse_matrix sparse_matrix; @@ -38,15 +39,26 @@ namespace opt { rational m_max_weight; rational m_denominator; vector m_S; + vector m_T; svector m_value; + svector m_value_saved; unsigned_vector m_value_trail; unsigned_vector m_value_lim; - vector m_use_list; + vector m_tuse_list; + vector m_fuse_list; unsynch_mpz_manager m; Simplex m_simplex; unsigned m_weights_var; - imp():m_cancel(false) {} + params_ref m_params; + sat::solver m_solver; + svector m_vars; + + imp(): + m_cancel(false), + m_max_weight(0), + m_weights_var(0), + m_solver(m_params,0) {} ~imp() {} void add_weight(rational const& w) { @@ -57,28 +69,56 @@ namespace opt { m_simplex.set_upper(var, mpq_inf(mpq(1),mpq(0))); m_weights.push_back(w); m_value.push_back(l_undef); - m_use_list.push_back(unsigned_vector()); + m_tuse_list.push_back(unsigned_vector()); + m_fuse_list.push_back(unsigned_vector()); m_max_weight += w; + m_vars.push_back(m_solver.mk_var()); } - void add_set(unsigned sz, unsigned const* S) { - if (sz == 0) { - return; - } + void add_exists_false(unsigned sz, unsigned const* S) { + SASSERT(sz > 0); for (unsigned i = 0; i < sz; ++i) { - m_use_list[S[i]].push_back(m_S.size()); + m_fuse_list[S[i]].push_back(m_T.size()); + } + init_weights(); + m_T.push_back(unsigned_vector(sz, S)); + add_simplex_row(false, sz, S); + // Add clause to SAT solver: + svector lits; + for (unsigned i = 0; i < sz; ++i) { + lits.push_back(sat::literal(m_vars[S[i]], true)); + } + m_solver.mk_clause(lits.size(), lits.c_ptr()); + } + + void add_exists_true(unsigned sz, unsigned const* S) { + SASSERT(sz > 0); + for (unsigned i = 0; i < sz; ++i) { + m_tuse_list[S[i]].push_back(m_S.size()); } init_weights(); m_S.push_back(unsigned_vector(sz, S)); - add_simplex_row(sz, S); + add_simplex_row(true, sz, S); + + // Add clause to SAT solver + svector lits; + for (unsigned i = 0; i < sz; ++i) { + lits.push_back(sat::literal(m_vars[S[i]], false)); + } + m_solver.mk_clause(lits.size(), lits.c_ptr()); } - bool compute_lower() { + lbool compute_lower() { m_lower.reset(); - return L1() && L2() && L3(); + if (L1() && L2() && L3()) { + return l_true; + } + else { + return l_undef; + } } - bool compute_upper() { + lbool compute_upper() { m_upper = m_max_weight; return U1(); } @@ -91,18 +131,30 @@ namespace opt { return m_upper/m_denominator; } + void set_upper(rational const& r) { + m_max_weight = r; + } + + bool get_value(unsigned idx) { + return + idx < m_value_saved.size() && + m_value_saved[idx] == l_true; + } + void set_cancel(bool f) { m_cancel = f; m_simplex.set_cancel(f); + m_solver.set_cancel(f); } void collect_statistics(::statistics& st) const { m_simplex.collect_statistics(st); + m_solver.collect_statistics(st); } void reset() { m_lower.reset(); - m_upper = m_max_weight; + m_upper = m_max_weight; } void init_weights() { @@ -135,6 +187,25 @@ namespace opt { m_simplex.add_row(m_weights_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr()); } + void display(std::ostream& out) const { + for (unsigned i = 0; i < m_weights.size(); ++i) { + out << i << ": " << m_value_saved[i]<< " " << m_weights[i] << "\n"; + } + for (unsigned i = 0; i < m_S.size(); ++i) { + display(out << "+ ", m_S[i]); + } + for (unsigned i = 0; i < m_T.size(); ++i) { + display(out << "- ", m_T[i]); + } + } + + void display(std::ostream& out, set const& S) const { + for (unsigned i = 0; i < S.size(); ++i) { + out << S[i] << " "; + } + out << "\n"; + } + struct scoped_select { imp& s; unsigned sz; @@ -164,9 +235,67 @@ namespace opt { } }; + lbool U1() { + scoped_select _sc(*this); + while (true) { + if (!compute_U1()) return l_undef; + unsigned i = 0, j = 0; + set_undef_to_false(); + if (values_satisfy_Ts(i)) { + return l_true; + } + + // + // pick some unsatisfied clause from m_T, + // and set the value of the most expensive + // literal to true. + // + + IF_VERBOSE(1, verbose_stream() << "(hs.refining exclusion set " << i << "\n";); + set const& T = m_T[i]; + rational max_value(0); + j = 0; + for (i = 0; i < T.size(); ++i) { + SASSERT(m_value_saved[T[i]] == l_true); + if (max_value < m_weights[T[i]]) { + max_value = m_weights[T[i]]; + j = T[i]; + } + } + IF_VERBOSE(1, verbose_stream() << "(hs.unselect " << j << ")\n";); + unselect(j); + for (i = 0; i < m_S.size(); ++i) { + set const& S = m_S[i]; + for (j = 0; j < S.size(); ++j) { + if (l_false != selected(S[j])) break; + } + if (j == S.size()) { + IF_VERBOSE(1, verbose_stream() << "approximation failed, fall back to SAT\n";); + return compute_U2(); + } + } + TRACE("opt", display(tout);); + } + } + + lbool compute_U2() { + lbool is_sat = m_solver.check(); + if (is_sat == l_true) { + sat::model const& model = m_solver.get_model(); + m_value_saved.reset(); + m_upper.reset(); + for (unsigned i = 0; i < m_vars.size(); ++i) { + m_value_saved.push_back(model[m_vars[i]]); + if (model[m_vars[i]] == l_true) { + m_upper += m_weights[i]; + } + } + } + return is_sat; + } // compute upper bound for hitting set. - bool U1() { + bool compute_U1() { rational w(0); scoped_select _sc(*this); @@ -177,7 +306,7 @@ namespace opt { // // Sort indices. - // The least literals are those where -score/w is minimized. + // The least literals are those where score/w is maximized. // unsigned_vector indices; for (unsigned i = 0; i < m_value.size(); ++i) { @@ -194,8 +323,11 @@ namespace opt { select(idx); w += m_weights[idx]; } - if (w < m_upper) { - m_upper = w; + m_upper = w; + m_value_saved.reset(); + m_value_saved.append(m_value); + if (m_upper > m_max_weight) { + IF_VERBOSE(0, verbose_stream() << "got worse upper bound\n";); } return !m_cancel; } @@ -209,19 +341,23 @@ namespace opt { set const& S = m_S[i]; if (!has_selected(S)) { for (unsigned j = 0; j < S.size(); ++j) { - scores[S[j]]++; + if (selected(S[j]) != l_false) { + scores[S[j]]++; + } } } } } void update_scores(unsigned_vector& scores, unsigned v) { - unsigned_vector const& v_uses = m_use_list[v]; + unsigned_vector const& v_uses = m_tuse_list[v]; for (unsigned i = 0; i < v_uses.size(); ++i) { set const& S = m_S[v_uses[i]]; if (!has_selected(S)) { for (unsigned j = 0; j < S.size(); ++j) { - --scores[S[j]]; + if (selected(S[j]) != l_false) { + --scores[S[j]]; + } } } } @@ -300,20 +436,26 @@ namespace opt { return true; } - void add_simplex_row(unsigned sz, unsigned const* S) { + void add_simplex_row(bool is_some_true, unsigned sz, unsigned const* S) { unsigned_vector vars; scoped_mpz_vector coeffs(m); for (unsigned i = 0; i < sz; ++i) { vars.push_back(S[i]); coeffs.push_back(mpz(1)); } - unsigned base_var = m_S.size() + m_weights.size(); + unsigned base_var = m_T.size() + m_S.size() + m_weights.size(); m_simplex.ensure_var(base_var); vars.push_back(base_var); coeffs.push_back(mpz(-1)); // S - base_var = 0 - // base_var >= 1 - m_simplex.set_lower(base_var, mpq_inf(mpq(1),mpq(0))); + if (is_some_true) { + // base_var >= 1 + m_simplex.set_lower(base_var, mpq_inf(mpq(1),mpq(0))); + } + else { + // base_var <= sz-1 + m_simplex.set_upper(base_var, mpq_inf(mpq(sz-1),mpq(0))); + } m_simplex.add_row(base_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr()); } @@ -334,7 +476,6 @@ namespace opt { return result; } - lbool selected(unsigned j) const { return m_value[j]; } @@ -343,10 +484,58 @@ namespace opt { m_value[j] = l_true; m_value_trail.push_back(j); } + + void unselect(unsigned j) { + m_value[j] = l_false; + m_value_trail.push_back(j); + } + + bool have_selected(lbool val, vector const& Sets, unsigned& i) { + for (i = 0; i < Sets.size(); ++i) { + if (!has_selected(val, Sets[i])) return false; + } + return true; + } + + void set_undef_to_false() { + for (unsigned i = 0; i < m_value_saved.size(); ++i) { + if (m_value_saved[i] == l_undef) { + m_value_saved[i] = l_false; + } + } + } + + bool values_satisfy_Ts(unsigned& i) { + unsigned j = 0; + for (i = 0; i < m_T.size(); ++i) { + set const& T = m_T[i]; + for (j = 0; j < T.size(); ++j) { + if (m_value_saved[T[j]] == l_false) { + break; + } + } + if (T.size() == j) { + break; + } + } + return i == m_T.size(); + } bool has_selected(set const& S) { + return has_selected(l_true, S); + } + + bool has_unselected(set const& S) { + return has_selected(l_false, S); + } + + bool has_unset(set const& S) { + return has_selected(l_undef, S); + } + + bool has_selected(lbool val, set const& S) { for (unsigned i = 0; i < S.size(); ++i) { - if (l_true == selected(S[i])) { + if (val == selected(S[i])) { return true; } } @@ -357,11 +546,14 @@ namespace opt { hitting_sets::hitting_sets() { m_imp = alloc(imp); } hitting_sets::~hitting_sets() { dealloc(m_imp); } void hitting_sets::add_weight(rational const& w) { m_imp->add_weight(w); } - void hitting_sets::add_set(unsigned sz, unsigned const* elems) { m_imp->add_set(sz, elems); } - bool hitting_sets::compute_lower() { return m_imp->compute_lower(); } - bool hitting_sets::compute_upper() { return m_imp->compute_upper(); } + void hitting_sets::add_exists_true(unsigned sz, unsigned const* elems) { m_imp->add_exists_true(sz, elems); } + void hitting_sets::add_exists_false(unsigned sz, unsigned const* elems) { m_imp->add_exists_false(sz, elems); } + lbool hitting_sets::compute_lower() { return m_imp->compute_lower(); } + lbool hitting_sets::compute_upper() { return m_imp->compute_upper(); } rational hitting_sets::get_lower() { return m_imp->get_lower(); } rational hitting_sets::get_upper() { return m_imp->get_upper(); } + void hitting_sets::set_upper(rational const& r) { return m_imp->set_upper(r); } + bool hitting_sets::get_value(unsigned idx) { return m_imp->get_value(idx); } void hitting_sets::set_cancel(bool f) { m_imp->set_cancel(f); } void hitting_sets::collect_statistics(::statistics& st) const { m_imp->collect_statistics(st); } void hitting_sets::reset() { m_imp->reset(); } diff --git a/src/opt/hitting_sets.h b/src/opt/hitting_sets.h index bea5559f9..58de8c518 100644 --- a/src/opt/hitting_sets.h +++ b/src/opt/hitting_sets.h @@ -21,6 +21,7 @@ Notes: #include "rational.h" #include "statistics.h" +#include "lbool.h" namespace opt { @@ -31,11 +32,14 @@ namespace opt { hitting_sets(); ~hitting_sets(); void add_weight(rational const& w); - void add_set(unsigned sz, unsigned const* elems); - bool compute_lower(); - bool compute_upper(); + void add_exists_true(unsigned sz, unsigned const* elems); + void add_exists_false(unsigned sz, unsigned const* elems); + lbool compute_lower(); + lbool compute_upper(); + void set_upper(rational const& r); rational get_lower(); rational get_upper(); + bool get_value(unsigned idx); void set_cancel(bool f); void collect_statistics(::statistics& st) const; void reset(); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 12a922b01..bdac382f9 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -613,11 +613,8 @@ namespace opt { double m_disjoint_cores_time; }; - scoped_ptr maxs; - hitting_sets m_hs; + hitting_sets m_hs; expr_ref_vector m_aux; // auxiliary (indicator) variables. - expr_ref_vector m_iaux; // auxiliary integer (indicator) variables. - expr_ref_vector m_naux; // negation of auxiliary variables. obj_map m_aux2index; // expr |-> index unsigned_vector m_core_activity; // number of times soft constraint is used in a core. svector m_seed; // clause selected in current model. @@ -630,12 +627,9 @@ namespace opt { public: - hsmax(solver* s, ast_manager& m, maxsmt_solver_base* maxs): + hsmax(solver* s, ast_manager& m): maxsmt_solver_base(s, m), - maxs(maxs), m_aux(m), - m_iaux(m), - m_naux(m), pb(m), a(m), m_at_lower_bound(false) { @@ -644,7 +638,7 @@ namespace opt { virtual void set_cancel(bool f) { maxsmt_solver_base::set_cancel(f); - maxs->set_cancel(f); + m_hs.set_cancel(f); } virtual void updt_params(params_ref& p) { @@ -653,7 +647,7 @@ namespace opt { virtual void collect_statistics(statistics& st) const { maxsmt_solver_base::collect_statistics(st); - maxs->s().collect_statistics(st); + m_hs.collect_statistics(st); st.update("hsmax-num-iterations", m_stats.m_num_iterations); st.update("hsmax-num-core-reductions-n", m_stats.m_num_core_reductions_failure); st.update("hsmax-num-core-reductions-y", m_stats.m_num_core_reductions_success); @@ -694,14 +688,14 @@ namespace opt { break; case l_false: TRACE("opt", tout << "no more seeds\n";); - m_lower = m_upper; - return l_true; + m_lower = m_upper; + return l_true; case l_undef: return l_undef; } break; } - case l_false: + case l_false: TRACE("opt", tout << "no more cores\n";); m_lower = m_upper; return l_true; @@ -721,8 +715,6 @@ namespace opt { m_asms.reset(); m_seed.reset(); m_aux.reset(); - m_iaux.reset(); - m_naux.reset(); m_aux_active.reset(); m_aux2index.reset(); m_core_activity.reset(); @@ -730,9 +722,6 @@ namespace opt { bool tt = is_true(m_model, m_soft[i].get()); m_seed.push_back(tt); m_aux. push_back(mk_fresh(m.mk_bool_sort())); - m_iaux.push_back(mk_fresh(a.mk_int())); - expr* iaux = m_iaux.back(); - m_naux.push_back(m.mk_not(m_aux.back())); m_aux_active.push_back(false); m_core_activity.push_back(0); m_aux2index.insert(m_aux.back(), i); @@ -741,7 +730,6 @@ namespace opt { ensure_active(i); } } - maxs->init_soft(m_weights, m_aux); for (unsigned i = 0; i < m_weights.size(); ++i) { m_hs.add_weight(m_weights[i]); @@ -901,11 +889,8 @@ namespace opt { } // - // retrieve the next seed that satisfies state of maxs. - // state of maxs must be satisfiable before optimization is called. - // - // find a satisfying assignment to maxs state, that - // minimizes objective function. + // retrieve the next seed that satisfies state of hs. + // state of hs must be satisfiable before optimization is called. // lbool next_seed() { scoped_stopwatch _sw(m_stats.m_aux_sat_time); @@ -914,67 +899,28 @@ namespace opt { // min c_i*(not x_i) for x_i are soft clauses. // max c_i*x_i for x_i are soft clauses - lbool is_sat = l_true; m_at_lower_bound = false; - expr_ref fml(m); - if (m_lower.is_pos()) { - solver::scoped_push _scope(maxs->s()); - fml = pb.mk_le(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_lower); - maxs->add_hard(fml); - is_sat = maxs->s().check_sat(0,0); - if (is_sat == l_true) { - maxs->set_model(); - extract_seed(); - m_at_lower_bound = true; - return l_true; - } - } - is_sat = maxs->s().check_sat(0,0); - if (is_sat == l_true) { - maxs->set_model(); - } - else { - m_at_lower_bound = true; - return is_sat; - } - is_sat = (*maxs)(); + + lbool is_sat = m_hs.compute_upper(); if (is_sat == l_true) { - extract_seed(); + is_sat = m_hs.compute_lower(); + } + if (is_sat == l_true) { + m_at_lower_bound = m_hs.get_upper() == m_hs.get_lower(); + if (m_hs.get_lower() > m_lower) { + m_lower = m_hs.get_lower(); + } + for (unsigned i = 0; i < num_soft(); ++i) { + m_seed[i] = is_active(i) && !m_hs.get_value(i); + } + TRACE("opt", print_seed(tout);); } return is_sat; } -#if 0 - if (!m_hs.compute_upper()) { - return l_undef; - } - solver::scoped_push _scope(maxs->s()); - fml = pb.mk_le(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_hs.get_upper()); - IF_VERBOSE(0, verbose_stream() << "upper: " << m_hs.get_upper() << " " << m_upper << "\n";); - maxs->add_hard(fml); - TRACE("opt", tout << "checking with upper bound: " << m_hs.get_upper() << "\n";); - is_sat = maxs->s().check_sat(0,0); - std::cout << is_sat << "\n"; - - // TBD: uper bound estimate does not include the negative constraints. -#endif - - void extract_seed() { - model_ref mdl; - maxs->get_model(mdl); - m_lower.reset(); - for (unsigned i = 0; i < num_soft(); ++i) { - m_seed[i] = is_active(i) && is_true(mdl, m_aux[i].get()); - if (!m_seed[i]) { - m_lower += m_weights[i]; - } - } - TRACE("opt", print_seed(tout);); - } - // - // check assignment returned by maxs with the original + // check assignment returned by HS with the original // hard constraints. // If the assignment is consistent with the hard constraints // update the current model, otherwise, update the current lower @@ -1008,9 +954,7 @@ namespace opt { // extend the current assignment to one that // satisfies as many soft constraints as possible. // update the upper bound based on this assignment - // (because maxs has the constraint that the new - // assignment improves the previous m_upper). - // + // bool grow() { scoped_stopwatch _sw(m_stats.m_model_expansion_time); for (unsigned i = 0; i < num_soft(); ++i) { @@ -1022,7 +966,7 @@ namespace opt { ensure_active(i); m_asms.push_back(m_aux[i].get()); lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - IF_VERBOSE(1, verbose_stream() + IF_VERBOSE(3, verbose_stream() << "check: " << mk_pp(m_asms.back(), m) << ":" << is_sat << "\n";); TRACE("opt", tout @@ -1054,6 +998,7 @@ namespace opt { } if (upper < m_upper) { m_upper = upper; + m_hs.set_upper(upper); TRACE("opt", tout << "new upper: " << m_upper << "\n";); } return true; @@ -1128,50 +1073,32 @@ namespace opt { // // must include some literal not from asms. - // furthermore, update upper bound constraint in maxs + // (furthermore, update upper bound constraint in HS) // void block_down() { uint_set indices; + unsigned_vector c_indices; for (unsigned i = 0; i < m_asms.size(); ++i) { unsigned index = m_aux2index.find(m_asms[i]); indices.insert(index); } - expr_ref_vector fmls(m); - expr_ref fml(m); for (unsigned i = 0; i < num_soft(); ++i) { if (!indices.contains(i)) { - fmls.push_back(m_aux[i].get()); + c_indices.push_back(i); } } - fml = m.mk_or(fmls.size(), fmls.c_ptr()); - maxs->add_hard(fml); - set_upper(); - TRACE("opt", tout << fml << "\n";); - } - - // constrain the upper bound. - // w1*(not r1) + w2*(not r2) + ... + w_n*(not r_n) < m_upper - void set_upper() { - expr_ref fml(m); - fml = pb.mk_lt(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_upper); - maxs->add_hard(fml); + m_hs.add_exists_false(c_indices.size(), c_indices.c_ptr()); } // should exclude some literal from core. void block_up() { - expr_ref_vector fmls(m); - expr_ref fml(m); unsigned_vector indices; for (unsigned i = 0; i < m_asms.size(); ++i) { unsigned index = m_aux2index.find(m_asms[i]); - fmls.push_back(m.mk_not(m_asms[i])); m_core_activity[index]++; indices.push_back(index); } - fml = m.mk_or(fmls.size(), fmls.c_ptr()); - TRACE("opt", tout << fml << "\n";); - m_hs.add_set(indices.size(), indices.c_ptr()); - maxs->add_hard(fml); + m_hs.add_exists_true(indices.size(), indices.c_ptr()); } @@ -1661,14 +1588,8 @@ namespace opt { else if (m_engine == symbol("bcd2")) { m_maxsmt = alloc(bcd2, s.get(), m); } - else if (m_engine == symbol("hsmax")) { - //m_params.set_bool("pb.enable_simplex", true); - ref s0 = alloc(opt_solver, m, m_params, symbol()); - s0->check_sat(0,0); - maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m); // , s0->get_context()); - s2->set_converter(s0->mc_ref().get()); - - m_maxsmt = alloc(hsmax, s.get(), m, s2); + else if (m_engine == symbol("hsmax")) { + m_maxsmt = alloc(hsmax, s.get(), m); } // NB: this is experimental one-round version of SLS else if (m_engine == symbol("sls")) { diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index b8ac520b2..193bf59f2 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -215,7 +215,7 @@ namespace sat { sat_asymm_branch_params::collect_param_descrs(d); } - void asymm_branch::collect_statistics(statistics & st) { + void asymm_branch::collect_statistics(statistics & st) const { st.update("elim literals", m_elim_literals); } diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 6ffd239eb..f10522fab 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -49,7 +49,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); void dec(unsigned c) { m_counter -= c; } diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 4b1ac2c92..959f5e94f 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -206,7 +206,7 @@ namespace sat { m_elim_literals = 0; } - void cleaner::collect_statistics(statistics & st) { + void cleaner::collect_statistics(statistics & st) const { st.update("elim clauses", m_elim_clauses); st.update("elim literals", m_elim_literals); } diff --git a/src/sat/sat_cleaner.h b/src/sat/sat_cleaner.h index d4306afcd..d22408926 100644 --- a/src/sat/sat_cleaner.h +++ b/src/sat/sat_cleaner.h @@ -42,7 +42,7 @@ namespace sat { bool operator()(bool force = false); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); void dec() { m_cleanup_counter--; } diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index f9741cd7b..e9710c2d4 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -259,7 +259,7 @@ namespace sat { m_to_assert.finalize(); } - void probing::collect_statistics(statistics & st) { + void probing::collect_statistics(statistics & st) const { st.update("probing assigned", m_num_assigned); } diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h index 9f3c1ae87..2061b74bd 100644 --- a/src/sat/sat_probing.h +++ b/src/sat/sat_probing.h @@ -71,7 +71,7 @@ namespace sat { void free_memory(); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); // return the literals implied by l. diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 29f3f006f..ffbdb31c6 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -223,7 +223,7 @@ namespace sat { return to_elim.size(); } - void scc::collect_statistics(statistics & st) { + void scc::collect_statistics(statistics & st) const { st.update("elim bool vars", m_num_elim); } diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index c85cc7d42..5f69e11c6 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -40,7 +40,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); }; }; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 3553a9031..969a6c37a 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1469,7 +1469,7 @@ namespace sat { sat_simplifier_params::collect_param_descrs(r); } - void simplifier::collect_statistics(statistics & st) { + void simplifier::collect_statistics(statistics & st) const { st.update("subsumed", m_num_subsumed); st.update("subsumption resolution", m_num_sub_res); st.update("elim literals", m_num_elim_lits); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 263354a4a..521990ea0 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -181,7 +181,7 @@ namespace sat { void free_memory(); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e807915c4..0e9f50828 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1988,7 +1988,7 @@ namespace sat { m_cancel = f; } - void solver::collect_statistics(statistics & st) { + void solver::collect_statistics(statistics & st) const { m_stats.collect_statistics(st); m_cleaner.collect_statistics(st); m_simplifier.collect_statistics(st); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 2a64c9cd5..0738f0118 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -143,7 +143,7 @@ namespace sat { static void collect_param_descrs(param_descrs & d); void set_cancel(bool f); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); void display_status(std::ostream & out) const;