From 1b9529e1e1520b31c71d5f652ffdda621bf109e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Aug 2014 01:55:32 -0700 Subject: [PATCH] fix scope bugs per Klaus Becker's examples Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 90 +++++++++++++++++++++++++++++------------ src/opt/maxsmt.cpp | 2 +- src/opt/opt_context.cpp | 35 ++++++++-------- src/opt/opt_context.h | 7 ++-- 4 files changed, 88 insertions(+), 46 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 955531c16..c0bb1cd8f 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -84,6 +84,7 @@ private: strategy_t m_st; rational m_max_upper; bool m_hill_climb; + bool m_all_cores; public: maxres(context& c, @@ -95,7 +96,8 @@ public: m_mss(m_s, m), m_trail(m), m_st(st), - m_hill_climb(true) + m_hill_climb(true), + m_all_cores(false) { } @@ -151,21 +153,9 @@ public: return l_undef; } switch (is_sat) { - case l_true: { - s().get_model(m_model); - expr_ref tmp(m); - DEBUG_CODE( - for (unsigned i = 0; i < m_asms.size(); ++i) { - VERIFY(m_model->eval(m_asms[i].get(), tmp)); - SASSERT(m.is_true(tmp)); - }); - for (unsigned i = 0; i < m_soft.size(); ++i) { - VERIFY(m_model->eval(m_soft[i].get(), tmp)); - m_assignment[i] = m.is_true(tmp); - } - m_upper = m_lower; + case l_true: + found_optimum(); return l_true; - } case l_false: is_sat = process_unsat(); if (is_sat != l_true) return is_sat; @@ -294,22 +284,67 @@ public: init(); init_local(); sls(); + m_all_cores = true; NOT_IMPLEMENTED_YET(); - ptr_vector mcs; vector > cores; return l_undef; -#if 0 - while (m_lower < m_upper) { + lbool is_sat = l_true; + while (m_lower < m_upper && is_sat == l_true) { TRACE("opt", display_vec(tout, m_asms.size(), m_asms.c_ptr()); s().display(tout); tout << "\n"; display(tout); ); + lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); + if (m_cancel) { + return l_undef; + } + switch (is_sat) { + case l_true: + found_optimum(); + return l_true; + case l_false: + is_sat = process_unsat(cores); + break; + default: + break; + } + if (is_sat == l_undef) { + return l_undef; + } + if (cores.empty()) { + SASSERT(is_sat == l_false); + break; + } + SASSERT(is_sat == l_true); + // there is some best model, + // extend it to a maximal assignment + // extracting the mss and mcs. + set_mus(false); + ptr_vector mss, mcs; + is_sat = m_mss(cores, mss, mcs); + set_mus(true); + if (is_sat != l_true) return is_sat; + // } m_lower = m_upper; return l_true; -#endif + } + + void found_optimum() { + s().get_model(m_model); + expr_ref tmp(m); + DEBUG_CODE( + for (unsigned i = 0; i < m_asms.size(); ++i) { + VERIFY(m_model->eval(m_asms[i].get(), tmp)); + SASSERT(m.is_true(tmp)); + }); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(m_soft[i].get(), tmp)); + m_assignment[i] = m.is_true(tmp); + } + m_upper = m_lower; } @@ -341,8 +376,7 @@ public: break; } cores.push_back(core); - // TBD: ad hoc to avoid searching for large cores.. - if (core.size() >= 3) { + if (!m_all_cores && core.size() >= 3) { break; } remove_soft(core, asms); @@ -409,7 +443,7 @@ public: return index; } - lbool process_sat(ptr_vector& corr_set) { + lbool process_sat(ptr_vector const& corr_set) { expr_ref fml(m), tmp(m); TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr());); if (corr_set.empty()) { @@ -425,6 +459,10 @@ public: lbool process_unsat() { vector > cores; + return process_unsat(cores); + } + + lbool process_unsat(vector >& cores) { lbool is_sat = get_cores(cores); if (is_sat != l_true) { return is_sat; @@ -438,7 +476,7 @@ public: return is_sat; } - lbool process_unsat(ptr_vector& core) { + lbool process_unsat(ptr_vector const& core) { expr_ref fml(m); remove_core(core); rational w = split_core(core); @@ -452,7 +490,7 @@ public: } lbool minimize_core(ptr_vector& core) { - if (m_c.sat_enabled()) { + if (m_c.sat_enabled() || core.empty()) { return l_true; } m_mus.reset(); @@ -521,7 +559,7 @@ public: } } - void max_resolve(ptr_vector& core, rational const& w) { + void max_resolve(ptr_vector const& core, rational const& w) { SASSERT(!core.empty()); expr_ref fml(m), asum(m); app_ref cls(m), d(m), dd(m); @@ -563,7 +601,7 @@ public: } // cs is a correction set (a complement of a (maximal) satisfying assignment). - void cs_max_resolve(ptr_vector& cs, rational const& w) { + void cs_max_resolve(ptr_vector const& cs, rational const& w) { TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr());); SASSERT(!cs.empty()); expr_ref fml(m), asum(m); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 9fe704942..8c9148e17 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -41,7 +41,7 @@ namespace opt { m_c(c), m_cancel(false), m_soft(m), m_assertions(m) { - m_s.get_model(m_model); + c.get_base_model(m_model); SASSERT(m_model); updt_params(c.params()); init_soft(ws, soft); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 327a636f7..59b0ee566 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -215,7 +215,7 @@ namespace opt { case 0: return is_sat; case 1: - return execute(m_objectives[0], true); + return execute(m_objectives[0], true, false); default: { opt_params optp(m_params); symbol pri = optp.priority(); @@ -232,6 +232,10 @@ namespace opt { } } + void context::get_base_model(model_ref& mdl) { + mdl = m_model; + } + void context::get_model(model_ref& mdl) { mdl = m_model; if (mdl) { @@ -242,27 +246,31 @@ namespace opt { } } - lbool context::execute_min_max(unsigned index, bool committed) { + lbool context::execute_min_max(unsigned index, bool committed, bool scoped) { + if (scoped) get_solver().push(); lbool result = m_optsmt.lex(index); - if (result == l_true && committed) m_optsmt.commit_assignment(index); if (result == l_true) m_optsmt.get_model(m_model); + if (scoped) get_solver().pop(1); + if (result == l_true && committed) m_optsmt.commit_assignment(index); return result; } - lbool context::execute_maxsat(symbol const& id, bool committed) { + lbool context::execute_maxsat(symbol const& id, bool committed, bool scoped) { model_ref tmp; maxsmt& ms = *m_maxsmts.find(id); + if (scoped) get_solver().push(); lbool result = ms(m_solver.get()); - if (result == l_true && committed) ms.commit_assignment(); if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model); + if (scoped) get_solver().pop(1); + if (result == l_true && committed) ms.commit_assignment(); return result; } - lbool context::execute(objective const& obj, bool committed) { + lbool context::execute(objective const& obj, bool committed, bool scoped) { switch(obj.m_type) { - case O_MAXIMIZE: return execute_min_max(obj.m_index, committed); - case O_MINIMIZE: return execute_min_max(obj.m_index, committed); - case O_MAXSMT: return execute_maxsat(obj.m_id, committed); + case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, scoped); + case O_MINIMIZE: return execute_min_max(obj.m_index, committed, scoped); + case O_MAXSMT: return execute_maxsat(obj.m_id, committed, scoped); default: UNREACHABLE(); return l_undef; } } @@ -271,9 +279,7 @@ namespace opt { lbool r = l_true; for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { bool is_last = i + 1 == m_objectives.size(); - if (!is_last) get_solver().push(); - r = execute(m_objectives[i], i + 1 < m_objectives.size()); - if (!is_last) get_solver().pop(1); + r = execute(m_objectives[i], i + 1 < m_objectives.size(), !is_last); if (r == l_true && !get_lower_as_num(i).is_finite()) { return r; } @@ -291,7 +297,7 @@ namespace opt { objective const& obj = m_objectives[i]; if (obj.m_type == O_MAXSMT) { solver::scoped_push _sp(get_solver()); - r = execute(obj, false); + r = execute(obj, false, false); } } return r; @@ -399,9 +405,6 @@ namespace opt { if (is_sat == l_true) { yield(); } - else { - m_solver->pop(1); - } return is_sat; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 5f3bd88cb..c2c9f46d8 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -179,14 +179,15 @@ namespace opt { void enable_sls(expr_ref_vector const& soft, weights_t& weights); void set_enable_sls(bool f) { m_enable_sls = f; } symbol const& maxsat_engine() const { return m_maxsat_engine; } + void get_base_model(model_ref& m); private: void validate_feasibility(maxsmt& ms); - lbool execute(objective const& obj, bool committed); - lbool execute_min_max(unsigned index, bool committed); - lbool execute_maxsat(symbol const& s, bool committed); + lbool execute(objective const& obj, bool committed, bool scoped); + lbool execute_min_max(unsigned index, bool committed, bool scoped); + lbool execute_maxsat(symbol const& s, bool committed, bool scoped); lbool execute_lex(); lbool execute_box(); lbool execute_pareto();