From ed7db892f9835ffb405e877e2e8b6ca62098bde2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 4 Jun 2022 08:00:56 +0100 Subject: [PATCH] Fix a couple compiler warnings --- src/ast/ast_pp_util.h | 10 +-- src/opt/maxcore.cpp | 163 +++++++++++++++++++++--------------------- 2 files changed, 86 insertions(+), 87 deletions(-) diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h index 1a04f8af0..06ade7eed 100644 --- a/src/ast/ast_pp_util.h +++ b/src/ast/ast_pp_util.h @@ -30,15 +30,15 @@ class ast_pp_util { stacked_value m_rec_decls; stacked_value m_decls; stacked_value m_sorts; - - public: + + public: decl_collector coll; - ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m), m_rec_decls(0), m_decls(0), m_sorts(0) {} + ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m) {} void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); } - + void collect(expr* e); @@ -59,7 +59,7 @@ class ast_pp_util { std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true); void push(); - + void pop(unsigned n); smt2_pp_environment& env() { return m_env; } diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp index 1a89129c5..46e4c5a7d 100644 --- a/src/opt/maxcore.cpp +++ b/src/opt/maxcore.cpp @@ -6,7 +6,7 @@ Module Name: maxcore.cpp Abstract: - + Core based (weighted) max-sat algorithms: - mu: max-sat algorithm by Nina and Bacchus, AAAI 2014. @@ -26,20 +26,20 @@ Abstract: the approach updates the upper bound if the current assignment improves the current best assignmet. Furthermore, take the soft constraints that are complements - to the current satisfying subset. - E.g, if F are the hard constraints and - s1,...,sn, t1,..., tm are the soft clauses and - F & s1 & ... & sn is satisfiable, then the complement + to the current satisfying subset. + E.g, if F are the hard constraints and + s1,...,sn, t1,..., tm are the soft clauses and + F & s1 & ... & sn is satisfiable, then the complement of of the current satisfying subset is t1, .., tm. Update the hard constraint: F := F & (t1 or ... or tm) Replace t1, .., tm by m-1 new soft clauses: t1 & t2, t3 & (t1 or t2), t4 & (t1 or t2 or t3), ..., tn & (t1 or ... t_{n-1}) - Claim: - If k of these soft clauses are satisfied, then k+1 of + Claim: + If k of these soft clauses are satisfied, then k+1 of the previous soft clauses are satisfied. - If k of these soft clauses are false in the satisfying assignment - for the updated F, then k of the original soft clauses are also false + If k of these soft clauses are false in the satisfying assignment + for the updated F, then k of the original soft clauses are also false under the assignment. In summary: any assignment to the new clauses that satsfies F has the same cost. @@ -78,7 +78,7 @@ public: s_primal, s_primal_dual, s_primal_binary, - s_rc2 + s_rc2 }; private: struct stats { @@ -103,14 +103,14 @@ private: stats m_stats; expr_ref_vector m_B; - expr_ref_vector m_asms; + expr_ref_vector m_asms; expr_ref_vector m_defs; obj_map m_asm2weight; expr_ref_vector m_new_core; mus m_mus; expr_ref_vector m_trail; strategy_t m_st; - rational m_max_upper; + rational m_max_upper; model_ref m_csmodel; lns_maxcore m_lnsctx; lns m_lns; @@ -160,16 +160,16 @@ public: default: UNREACHABLE(); break; - } + } } ~maxcore() override {} bool is_literal(expr* l) { - return + return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); - } + } void add(expr_ref_vector const& es) { for (expr* e : es) add(e); @@ -205,7 +205,7 @@ public: IF_VERBOSE(13, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";); m_asm2weight.insert(e, w); m_asms.push_back(e); - m_trail.push_back(e); + m_trail.push_back(e); TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n"; tout << m_asms << " " << "\n"; ); } @@ -222,7 +222,7 @@ public: improve_model(); if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { - TRACE("opt_verbose", + TRACE("opt_verbose", s().display(tout << m_asms << "\n") << "\n"; display(tout);); is_sat = check_sat_hill_climb(m_asms); @@ -230,8 +230,8 @@ public: return l_undef; } switch (is_sat) { - case l_true: - CTRACE("opt", m_model->is_false(m_asms), + case l_true: + CTRACE("opt", m_model->is_false(m_asms), tout << *m_model << "assumptions: "; for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " "; tout << "\n";); @@ -244,7 +244,7 @@ public: m_lower = m_upper; } if (is_sat == l_undef) { - return is_sat; + return is_sat; } break; case l_undef: @@ -270,7 +270,7 @@ public: return l_undef; } switch (is_sat) { - case l_true: + case l_true: get_current_correction_set(cs); if (cs.empty()) { m_found_feasible_optimum = m_model.get() != nullptr; @@ -286,7 +286,7 @@ public: m_lower = m_upper; } if (is_sat == l_undef) { - return is_sat; + return is_sat; } break; case l_undef: @@ -307,7 +307,7 @@ public: /** Give preference to cores that have large minimal values. */ - sort_assumptions(asms); + sort_assumptions(asms); unsigned last_index = 0; unsigned index = 0; SASSERT(index < asms.size() || asms.empty()); @@ -318,16 +318,16 @@ public: } last_index = index; is_sat = check_sat(index, asms.data()); - } + } } else { - is_sat = check_sat(asms.size(), asms.data()); - } + is_sat = check_sat(asms.size(), asms.data()); + } return is_sat; } lbool check_sat(unsigned sz, expr* const* asms) { - lbool r = s().check_sat(sz, asms); + lbool r = s().check_sat(sz, asms); if (r == l_true) { model_ref mdl; s().get_model(mdl); @@ -399,7 +399,7 @@ public: return l_true; } - + // 1. remove all core literals from m_asms // 2. re-add literals of higher weight than min-weight. // 3. 'core' stores the core literals that are @@ -407,19 +407,19 @@ public: cores.push_back(weighted_core(core, core_weight(core))); remove_soft(core, m_asms); - split_core(core); + split_core(core); if (core.size() >= m_max_core_size) break; - is_sat = check_sat_hill_climb(m_asms); + is_sat = check_sat_hill_climb(m_asms); } - TRACE("opt", + TRACE("opt", tout << "sat: " << is_sat << " num cores: " << cores.size() << "\n"; for (auto const& c : cores) display_vec(tout, c.m_core); tout << "num assumptions: " << m_asms.size() << "\n";); - + return is_sat; } @@ -479,14 +479,14 @@ public: TRACE("opt", display_vec(tout << "corr_set: ", corr_set);); remove_soft(corr_set, m_asms); rational w = split_core(corr_set); - cs_max_resolve(corr_set, w); + cs_max_resolve(corr_set, w); IF_VERBOSE(2, verbose_stream() << "(opt.maxres.correction-set " << corr_set.size() << ")\n";); m_csmodel = nullptr; m_correction_set_size = 0; } lbool process_unsat() { - if (m_enable_core_rotate) + if (m_enable_core_rotate) return core_rotate(); vector cores; @@ -518,28 +518,28 @@ public: return l_true; } - + unsigned max_core_size(vector const& cores) { unsigned result = 0; - for (auto const& c : cores) + for (auto const& c : cores) result = std::max(c.size(), result); return result; } void process_unsat(vector const& cores) { - for (auto const & c : cores) + for (auto const & c : cores) process_unsat(c.m_core, c.m_weight); improve_model(m_model); } void update_model(expr* def, expr* value) { - SASSERT(is_uninterp_const(def)); - if (m_csmodel) + SASSERT(is_uninterp_const(def)); + if (m_csmodel) m_csmodel->register_decl(to_app(def)->get_decl(), (*m_csmodel)(value)); if (m_model) m_model->register_decl(to_app(def)->get_decl(), (*m_model)(value)); } - + void process_unsat(exprs const& core, rational w) { IF_VERBOSE(3, verbose_stream() << "(maxres cs model valid: " << (m_csmodel.get() != nullptr) << " cs size:" << m_correction_set_size << " core: " << core.size() << ")\n";); expr_ref fml(m); @@ -568,7 +568,7 @@ public: m_lower = std::min(m_lower, m_upper); } if (m_csmodel.get() && m_correction_set_size > 0) { - // this estimate can overshoot for weighted soft constraints. + // this estimate can overshoot for weighted soft constraints. --m_correction_set_size; } trace(); @@ -578,7 +578,7 @@ public: get_current_correction_set(m_csmodel.get(), cs); m_correction_set_size = cs.size(); TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";); - if (m_correction_set_size >= core.size()) + if (m_correction_set_size >= core.size()) return; rational w(0); for (expr* a : m_asms) { @@ -593,7 +593,7 @@ public: bool get_mus_model(model_ref& mdl) { rational w(0); if (m_c.sat_enabled()) { - // SAT solver core extracts some model + // SAT solver core extracts some model // during unsat core computation. mdl = nullptr; s().get_model(mdl); @@ -601,20 +601,20 @@ public: else { w = m_mus.get_best_model(mdl); } - if (mdl.get() && w < m_upper) + if (mdl.get() && w < m_upper) update_assignment(mdl); return nullptr != mdl.get(); } lbool minimize_core(expr_ref_vector& core) { - if (core.empty()) + if (core.empty()) return l_true; - if (m_c.sat_enabled()) + if (m_c.sat_enabled()) return l_true; m_mus.reset(); m_mus.add_soft(core.size(), core.data()); lbool is_sat = m_mus.get_mus(m_new_core); - if (is_sat != l_true) + if (is_sat != l_true) return is_sat; core.reset(); core.append(m_new_core); @@ -629,7 +629,7 @@ public: if (core.empty()) return rational(0); // find the minimal weight: rational w = get_weight(core[0]); - for (unsigned i = 1; i < core.size(); ++i) + for (unsigned i = 1; i < core.size(); ++i) w = std::min(w, get_weight(core[i])); return w; } @@ -643,7 +643,7 @@ public: rational w3 = w2 - w; new_assumption(e, w3); } - } + } return w; } @@ -663,7 +663,7 @@ public: } void display(std::ostream& out) { - for (expr * a : m_asms) + for (expr * a : m_asms) out << mk_pp(a, m) << " : " << get_weight(a) << "\n"; } @@ -677,15 +677,15 @@ public: // // d_0 := true // d_i := b_{i-1} and d_{i-1} for i = 1...sz-1 - // soft (b_i or !d_i) + // soft (b_i or !d_i) // == (b_i or !(!b_{i-1} or d_{i-1})) // == (b_i or b_0 & b_1 & ... & b_{i-1}) - // + // // Soft constraint is satisfied if previous soft constraint // holds or if it is the first soft constraint to fail. - // + // // Soundness of this rule can be established using MaxRes - // + // for (unsigned i = 1; i < core.size(); ++i) { expr* b_i = core[i-1]; expr* b_i1 = core[i]; @@ -761,7 +761,7 @@ public: bound_info(expr_ref_vector const& es, unsigned k, rational const& weight): es(es.size(), es.data()), k(k), weight(weight) {} }; - + obj_map m_at_mostk; obj_map m_bounds; rational m_unfold_upper; @@ -770,7 +770,7 @@ public: pb_util pb(m); expr_ref am(pb.mk_at_most_k(es, bound), m); expr* r = nullptr; - if (m_at_mostk.find(am, r)) + if (m_at_mostk.find(am, r)) return r; r = mk_fresh_bool("r"); m_trail.push_back(am); @@ -806,7 +806,7 @@ public: new_assumption(am, weight); } } - + // cs is a correction set (a complement of a (maximal) satisfying assignment). void cs_max_resolve(exprs const& cs, rational const& w) { @@ -820,7 +820,7 @@ public: // // d_0 := false // d_i := b_{i-1} or d_{i-1} for i = 1...sz-1 - // soft (b_i and d_i) + // soft (b_i and d_i) // == (b_i and (b_0 or b_1 or ... or b_{i-1})) // // asm => b_i @@ -836,7 +836,7 @@ public: fml = m.mk_implies(d, cls); update_model(d, cls); add(fml); - m_defs.push_back(fml); + m_defs.push_back(fml); } else { d = cls; @@ -869,7 +869,7 @@ public: void improve_model(model_ref& mdl) { - if (!m_enable_lns) + if (!m_enable_lns) return; flet _disable_lns(m_enable_lns, false); m_lns.climb(mdl); @@ -881,16 +881,16 @@ public: exprs _core(core.size(), core.data()); wcores.push_back(weighted_core(_core, core_weight(_core))); remove_soft(_core, m_asms); - split_core(_core); + split_core(_core); } process_unsat(wcores); } rational cost(model& mdl) { rational upper = m_unfold_upper; - for (soft& s : m_soft) - if (!mdl.is_true(s.s)) - upper += s.weight; + for (soft& s : m_soft) + if (!mdl.is_true(s.s)) + upper += s.weight; return upper; } @@ -898,8 +898,8 @@ public: improve_model(mdl); mdl->set_model_completion(true); unsigned correction_set_size = 0; - for (expr* a : m_asms) - if (mdl->is_false(a)) + for (expr* a : m_asms) + if (mdl->is_false(a)) ++correction_set_size; if (!m_csmodel.get() || correction_set_size < m_correction_set_size) { @@ -916,7 +916,7 @@ public: return; } - if (!m_c.verify_model(m_index, mdl.get(), upper)) + if (!m_c.verify_model(m_index, mdl.get(), upper)) return; unsigned num_assertions = s().get_num_assertions(); @@ -925,14 +925,14 @@ public: TRACE("opt", tout << "updated upper: " << upper << "\n";); - for (soft& s : m_soft) + for (soft& s : m_soft) s.set_value(m_model->is_true(s.s)); - + verify_assignment(); if (num_assertions == s().get_num_assertions()) m_upper = upper; - + trace(); add_upper_bound_block(); @@ -947,17 +947,17 @@ public: for (soft& s : m_soft) { nsoft.push_back(mk_not(m, s.s)); weights.push_back(s.weight); - } + } fml = u.mk_lt(nsoft.size(), weights.data(), nsoft.data(), m_upper); TRACE("opt", tout << "block upper bound " << fml << "\n";);; - add(fml); + add(fml); } void remove_soft(exprs const& core, expr_ref_vector& asms) { TRACE("opt", tout << "before remove: " << asms << "\n";); unsigned j = 0; - for (expr* a : asms) - if (!core.contains(a)) + for (expr* a : asms) + if (!core.contains(a)) asms[j++] = a; asms.shrink(j); TRACE("opt", tout << "after remove: " << asms << "\n";); @@ -974,8 +974,8 @@ public: m_pivot_on_cs = p.maxres_pivot_on_correction_set(); m_wmax = p.maxres_wmax(); m_dump_benchmarks = p.dump_benchmarks(); - m_enable_lns = p.enable_lns(); - m_enable_core_rotate = p.enable_core_rotate(); + m_enable_lns = p.enable_lns(); + m_enable_core_rotate = p.enable_core_rotate(); m_lns_conflicts = p.lns_conflicts(); if (m_c.num_objectives() > 1) m_add_upper_bound_block = false; @@ -983,7 +983,6 @@ public: lbool init_local() { m_trail.reset(); - lbool is_sat = l_true; for (auto const& [e, w, t] : m_soft) add_soft(e, w); m_max_upper = m_upper; @@ -1008,13 +1007,13 @@ public: void verify_core(exprs const& core) { return; - IF_VERBOSE(1, verbose_stream() << "verify core " << s().check_sat(core.size(), core.data()) << "\n";); + IF_VERBOSE(1, verbose_stream() << "verify core " << s().check_sat(core.size(), core.data()) << "\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); _solver->assert_expr(core); lbool is_sat = _solver->check_sat(0, nullptr); IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << " core size " << core.size() << "\n"); - CTRACE("opt", is_sat != l_false, + CTRACE("opt", is_sat != l_false, for (expr* c : core) tout << "core: " << mk_pp(c, m) << "\n"; _solver->display(tout); tout << "other solver\n"; @@ -1025,18 +1024,18 @@ public: void verify_assumptions() { return; - IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";); + IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); _solver->assert_expr(m_asms); lbool is_sat = _solver->check_sat(0, nullptr); - IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n";); + IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n";); VERIFY(is_sat == l_true); } void verify_assignment() { return; - IF_VERBOSE(1, verbose_stream() << "verify assignment\n";); + IF_VERBOSE(1, verbose_stream() << "verify assignment\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); expr_ref n(m);