From a9807878ea95ee149216ed511cc46d24260d0627 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Aug 2015 12:20:30 -0700 Subject: [PATCH] reworking pd-maxres Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 26 +++++++++++++++++++------- src/opt/maxsmt.cpp | 4 ---- src/opt/maxsmt.h | 1 - src/opt/opt_context.cpp | 4 ---- src/opt/opt_context.h | 2 -- src/sat/sat_solver.cpp | 3 +++ src/sat/sat_solver.h | 1 + 7 files changed, 23 insertions(+), 18 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index bf98e80ed..c697438c3 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -104,6 +104,7 @@ private: bool m_wmax; // Block upper bound using wmax // this option is disabled if SAT core is used. + std::string m_trace_id; typedef ptr_vector exprs; public: @@ -125,6 +126,14 @@ public: m_maximize_assignment(false), m_max_correction_set_size(3) { + switch(st) { + case s_primal: + m_trace_id = "maxres"; + break; + case s_primal_dual: + m_trace_id = "pd-maxres"; + break; + } } virtual ~maxres() {} @@ -168,10 +177,14 @@ public: m_trail.push_back(e); } + void trace() { + trace_bounds(m_trace_id.c_str()); + } + lbool mus_solver() { init(); init_local(); - trace_bounds("maxres"); + trace(); while (m_lower < m_upper) { TRACE("opt", display_vec(tout, m_asms); @@ -197,16 +210,15 @@ public: break; } } - trace_bounds("maxres"); + trace(); return l_true; } lbool primal_dual_solver() { init(); init_local(); - set_soft_assumptions(); lbool is_sat = l_true; - trace_bounds("maxres"); + trace(); exprs cs; while (m_lower < m_upper) { is_sat = check_sat_hill_climb(m_asms); @@ -235,7 +247,7 @@ public: break; } } - trace_bounds("maxres"); + trace(); return l_true; } @@ -456,7 +468,7 @@ public: fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr())); s().assert_expr(fml); m_lower += w; - trace_bounds("maxres"); + trace(); } bool get_mus_model(model_ref& mdl) { @@ -652,7 +664,7 @@ public: } m_upper = upper; DEBUG_CODE(verify_assignment();); - trace_bounds("maxres"); + trace(); add_upper_bound_block(); } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 0267b8bb7..0729d8396 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -101,10 +101,6 @@ namespace opt { m_c.enable_sls(force); } - void maxsmt_solver_base::set_soft_assumptions() { - m_c.set_soft_assumptions(); - } - app* maxsmt_solver_base::mk_fresh_bool(char const* name) { app* result = m.mk_fresh_const(name, m.mk_bool_sort()); m_c.fm().insert(result->get_decl()); diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index ef85b9de8..8d290a640 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -101,7 +101,6 @@ namespace opt { protected: void enable_sls(bool force); - void set_soft_assumptions(); void trace_bounds(char const* solver); }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 2936ee3c0..4ae4b0112 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -530,10 +530,6 @@ namespace opt { } } - void context::set_soft_assumptions() { - // TBD no-op - } - void context::enable_sls(bool force) { if ((force || m_enable_sls) && m_sat_solver.get()) { m_params.set_bool("optimize_model", true); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 194c08495..f872d70b5 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -51,7 +51,6 @@ namespace opt { virtual ast_manager& get_manager() = 0; virtual params_ref& params() = 0; virtual void enable_sls(bool force) = 0; // stochastic local search - virtual void set_soft_assumptions() = 0; // configure SAT solver to skip assumptions assigned by unit-propagation virtual symbol const& maxsat_engine() const = 0; // retrieve maxsat engine configuration parameter. virtual void get_base_model(model_ref& _m) = 0; // retrieve model from initial satisfiability call. virtual smt::context& smt_context() = 0; // access SMT context for SMT based MaxSMT solver (wmax requires SMT core) @@ -216,7 +215,6 @@ namespace opt { virtual ast_manager& get_manager() { return this->m; } virtual params_ref& params() { return m_params; } virtual void enable_sls(bool force); - virtual void set_soft_assumptions(); virtual symbol const& maxsat_engine() const { return m_maxsat_engine; } virtual void get_base_model(model_ref& _m); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index dc258817b..0200b70db 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -925,6 +925,7 @@ namespace sat { else { svector blocker; if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) { + ++m_stats.m_blocked_corr_sets; pop_to_base_level(); mk_clause(blocker.size(), blocker.c_ptr()); goto retry_init_assumptions; @@ -2811,6 +2812,7 @@ namespace sat { st.update("restarts", m_restart); st.update("minimized lits", m_minimized_lits); st.update("dyn subsumption resolution", m_dyn_sub_res); + st.update("blocked correction sets", m_blocked_corr_sets); } void stats::reset() { @@ -2829,6 +2831,7 @@ namespace sat { m_minimized_lits = 0; m_dyn_sub_res = 0; m_non_learned_generation = 0; + m_blocked_corr_sets = 0; } void mk_stat::display(std::ostream & out) const { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 76a42829d..49a8144f0 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -60,6 +60,7 @@ namespace sat { unsigned m_minimized_lits; unsigned m_dyn_sub_res; unsigned m_non_learned_generation; + unsigned m_blocked_corr_sets; stats() { reset(); } void reset(); void collect_statistics(statistics & st) const;