From e8056e066dd405416e3ffd87dee82e2ab937e4eb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Jul 2014 12:57:30 -0700 Subject: [PATCH] enable bvsat, multi disjoint cores for dual-maxres Signed-off-by: Nikolaj Bjorner --- src/opt/dual_maxres.cpp | 72 +++++++++++++++++++++++++++++++++-------- src/opt/maxres.cpp | 1 + src/opt/maxsmt.cpp | 14 ++++++-- 3 files changed, 71 insertions(+), 16 deletions(-) diff --git a/src/opt/dual_maxres.cpp b/src/opt/dual_maxres.cpp index 55d347e9e..95834ca1a 100644 --- a/src/opt/dual_maxres.cpp +++ b/src/opt/dual_maxres.cpp @@ -111,8 +111,11 @@ public: solver::scoped_push _sc(*m_s.get()); init(); init_local(); + enable_bvsat(); + enable_sls(); lbool was_sat = l_false; ptr_vector soft_compl; + vector > cores; while (m_lower < m_upper) { TRACE("opt", display_vec(tout, m_asms.size(), m_asms.c_ptr()); @@ -131,7 +134,10 @@ public: case l_undef: break; case l_false: - is_sat = process_unsat(soft_compl); + is_sat = get_cores(soft_compl, cores); + for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) { + is_sat = process_unsat(cores[i]); + } break; case l_true: is_sat = process_sat(soft_compl); @@ -166,18 +172,54 @@ public: return l_true; } + // + // Retrieve a set of disjoint cores over the current assumptions. + // TBD: when the remaining are satisfiable, then extend the + // satisfying model to improve upper bound. + // + lbool get_cores(ptr_vector& core, vector >& cores) { + // assume 'core' is minimal. + expr_ref_vector asms(m); + asms.append(m_asms.size(), m_asms.c_ptr()); + remove_soft(core, asms); + cores.reset(); + cores.push_back(core); + ptr_vector new_core; + while (true) { + lbool is_sat = m_s->check_sat(asms.size(), asms.c_ptr()); + switch (is_sat) { + case l_false: + new_core.reset(); + m_s->get_unsat_core(new_core); + switch (minimize_core(new_core)) { + case l_false: + return l_false; + case l_true: + cores.push_back(new_core); + remove_soft(new_core, asms); + break; + default: + return l_undef; + } + break; + case l_true: + TRACE("opt", + tout << "num cores: " << cores.size() << "\n"; + tout << "num satisfying: " << asms.size() << "\n";); + return l_true; + default: + return l_undef; + } + } + } + lbool process_unsat(ptr_vector& core) { expr_ref fml(m); TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());); SASSERT(!core.empty()); - lbool is_sat = minimize_core(core); - SASSERT(!core.empty()); if (core.empty()) { return l_false; } - if (is_sat != l_true) { - return is_sat; - } remove_soft(core); rational w = split_soft(core); TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); @@ -186,7 +228,7 @@ public: IF_VERBOSE(1, verbose_stream() << "(opt.dual_max_res [" << m_lower << ":" << m_upper << "])\n";); - return is_sat; + return l_true; } // @@ -221,7 +263,7 @@ public: if (num_true*2 < m_asms.size()) { soft_compl.reset(); m_s->get_unsat_core(soft_compl); - return l_false; + return minimize_core(soft_compl); } break; case l_true: @@ -394,16 +436,20 @@ public: m_s->assert_expr(fml); } - void remove_soft(ptr_vector const& soft) { - for (unsigned i = 0; i < m_asms.size(); ++i) { - if (soft.contains(m_asms[i].get())) { - m_asms[i] = m_asms.back(); - m_asms.pop_back(); + void remove_soft(ptr_vector const& soft, expr_ref_vector& asms) { + for (unsigned i = 0; i < asms.size(); ++i) { + if (soft.contains(asms[i].get())) { + asms[i] = asms.back(); + asms.pop_back(); --i; } } } + void remove_soft(ptr_vector const& soft) { + remove_soft(soft, m_asms); + } + virtual void set_cancel(bool f) { maxsmt_solver_base::set_cancel(f); m_mus.set_cancel(f); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index fa0210ee2..98abb7bfd 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -90,6 +90,7 @@ public: solver::scoped_push _sc(*m_s.get()); init(); init_local(); + enable_bvsat(); while (true) { TRACE("opt", display_vec(tout, m_asms.size(), m_asms.c_ptr()); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index df42ac11f..821113e28 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -130,7 +130,14 @@ namespace opt { } void maxsmt_solver_base::enable_inc_bvsat() { - + solver* sat_solver = mk_inc_sat_solver(m, m_params); + unsigned sz = s().get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + sat_solver->assert_expr(s().get_assertion(i)); + } + unsigned lvl = m_s->get_scope_level(); + while (lvl > 0) { sat_solver->push(); --lvl; } + m_s = sat_solver; } void maxsmt_solver_base::enable_noninc_bvsat() { @@ -145,13 +152,14 @@ namespace opt { unsigned lvl = m_s->get_scope_level(); while (lvl > 0) { sat_solver->push(); --lvl; } m_s = sat_solver; - m_sat_enabled = true; } void maxsmt_solver_base::enable_bvsat() { if (m_enable_sat && !m_sat_enabled && probe_bv()) { - enable_noninc_bvsat(); + enable_inc_bvsat(); + // enable_noninc_bvsat(); + m_sat_enabled = true; } }