From 0dd0fd26d49740bba504e7580d68006158369107 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Apr 2022 10:44:49 +0100 Subject: [PATCH] remove buggy prototype Signed-off-by: Nikolaj Bjorner --- src/opt/maxcore.cpp | 84 +----------------------------------------- src/opt/maxcore.h | 2 - src/opt/maxsmt.cpp | 3 -- src/opt/opt_params.pyg | 2 +- 4 files changed, 2 insertions(+), 89 deletions(-) diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp index 2c4c87306..792e5e17a 100644 --- a/src/opt/maxcore.cpp +++ b/src/opt/maxcore.cpp @@ -558,9 +558,6 @@ public: case strategy_t::s_primal_binary: bin_max_resolve(core, w); break; - case strategy_t::s_primal_binary_delay: - bin_delay_max_resolve(core, w); - break; case strategy_t::s_rc2: max_resolve_rc2(core, w); break; @@ -761,82 +758,7 @@ public: } - // binary - with delayed unfolding of new soft clauses. - struct unfold_record { - ptr_vector ws; - rational weight; - }; - obj_map m_unfold; - rational m_unfold_upper; - - void bin_delay_max_resolve(exprs const& _core, rational weight) { - expr_ref_vector core(m, _core.size(), _core.data()), partial(m); - expr_ref fml(m), cls(m); - for (expr* c : core) { - unfold_record r; - if (!m_unfold.find(c, r)) - continue; - IF_VERBOSE(1, verbose_stream() << "to unfold " << mk_pp(c, m) << " unfold size " << m_unfold.size() << " core " << core.size() << "\n"); - for (expr* f : r.ws) { - IF_VERBOSE(1, verbose_stream() << "unfold " << mk_pp(f, m) << "\n"); - new_assumption(f, r.weight); - } - m_unfold_upper -= r.weight * rational(r.ws.size() - 1); - m_unfold.remove(c); - } - - partial.resize(core.size(), nullptr); - - if (core.size() > 2) - m_unfold_upper += rational(core.size()-2)*weight; - - expr* w = nullptr; - for (unsigned i = 0; i + 1 < core.size(); i += 2) { - expr* a = core.get(i); - expr* b = core.get(i + 1); - expr* u = mk_fresh_bool("u"); - expr* v = mk_fresh_bool("v"); - // u = a or b - // v = a and b - cls = m.mk_or(a, b); - fml = m.mk_implies(u, cls); - add(fml); - update_model(u, cls); - m_defs.push_back(fml); - cls = m.mk_and(a, b); - fml = m.mk_implies(v, cls); - add(fml); - update_model(v, cls); - m_defs.push_back(fml); - core.push_back(v); - - // w = u and w1 and w2 - unfold_record r; - r.ws.push_back(u); - if (partial.get(i)) - r.ws.push_back(partial.get(i)); - if (partial.get(i + 1)) - r.ws.push_back(partial.get(i + 1)); - m_trail.append(r.ws.size(), r.ws.data()); - r.weight = weight; - if (r.ws.size() == 1) - w = u; - else { - w = mk_fresh_bool("w"); - cls = m.mk_and(r.ws); - fml = m.mk_implies(w, cls); - add(fml); - update_model(w, cls); - m_defs.push_back(fml); - m_unfold.insert(w, r); - } - partial.push_back(w); - } - if (w) - new_assumption(w, weight); - s().assert_expr(m.mk_not(core.back())); - } // rc2, using cardinality constraints @@ -854,6 +776,7 @@ public: obj_map m_at_mostk; obj_map m_bounds; + rational m_unfold_upper; expr* mk_atmost(expr_ref_vector const& es, unsigned bound, rational const& weight) { pb_util pb(m); @@ -1081,7 +1004,6 @@ public: add_upper_bound_block(); m_csmodel = nullptr; m_correction_set_size = 0; - m_unfold.reset(); m_unfold_upper = 0; m_at_mostk.reset(); m_bounds.reset(); @@ -1159,10 +1081,6 @@ opt::maxsmt_solver_base* opt::mk_maxres_binary( return alloc(maxcore, c, id, soft, maxcore::s_primal_binary); } -opt::maxsmt_solver_base* opt::mk_maxres_binary_delay( - maxsat_context& c, unsigned id, vector& soft) { - return alloc(maxcore, c, id, soft, maxcore::s_primal_binary_delay); -} opt::maxsmt_solver_base* opt::mk_primal_dual_maxres( maxsat_context& c, unsigned id, vector& soft) { diff --git a/src/opt/maxcore.h b/src/opt/maxcore.h index 42efeb0bf..2dba613a7 100644 --- a/src/opt/maxcore.h +++ b/src/opt/maxcore.h @@ -27,8 +27,6 @@ namespace opt { maxsmt_solver_base* mk_maxres_binary(maxsat_context& c, unsigned id, vector& soft); - maxsmt_solver_base* mk_maxres_binary_delay(maxsat_context& c, unsigned id, vector& soft); - maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector& soft); }; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index b2cdedf64..02de67bb5 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -197,9 +197,6 @@ namespace opt { else if (maxsat_engine == symbol("rc2")) { m_msolver = mk_rc2(m_c, m_index, m_soft); } - else if (maxsat_engine == symbol("maxres-bin-delay")) { - m_msolver = mk_maxres_binary_delay(m_c, m_index, m_soft); - } else if (maxsat_engine == symbol("pd-maxres")) { m_msolver = mk_primal_dual_maxres(m_c, m_index, m_soft); } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 914b3a72b..9c00020d5 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -2,7 +2,7 @@ def_module_params('opt', description='optimization parameters', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'symba'"), - ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'maxres-bin-delay', 'rc2'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('dump_models', BOOL, False, 'display intermediary models to stdout'),