From 73070585b83c77bee5ebe08664d350056d5463c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Sep 2014 13:06:01 -0700 Subject: [PATCH] fix bug in core generation in legacy core: it ignores complementary literals Signed-off-by: Nikolaj Bjorner --- src/opt/inc_sat_solver.cpp | 7 ++----- src/opt/maxres.cpp | 3 +++ src/opt/maxsmt.cpp | 4 ++-- src/opt/opt_context.cpp | 1 + src/sat/sat_solver.cpp | 3 +++ src/sat/sat_solver.h | 4 +++- src/smt/smt_context.cpp | 18 ++++++++---------- src/smt/smt_context.h | 6 +++--- 8 files changed, 25 insertions(+), 21 deletions(-) diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index 11aa24d71..41e4d12de 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -356,16 +356,13 @@ private: } } - // TBD: this is super-expensive because of the - // bit-blasting model converter. - void extract_model() { TRACE("sat", tout << "retrieve model\n";); - sat::model const & ll_m = m_solver.get_model(); - if (ll_m.empty()) { + if (!m_solver.model_is_current()) { m_model = 0; return; } + sat::model const & ll_m = m_solver.get_model(); model_ref md = alloc(model, m); atom2bool_var::iterator it = m_map.begin(); atom2bool_var::iterator end = m_map.end(); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 60cc11555..c2de70ad6 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -130,6 +130,7 @@ public: if (m_asm2weight.find(e, weight)) { weight += w; m_asm2weight.insert(e, weight); + m_upper += w; return; } if (is_literal(e)) { @@ -154,6 +155,7 @@ public: lbool mus_solver() { init(); init_local(); + trace_bounds("maxres"); while (m_lower < m_upper) { TRACE("opt", display_vec(tout, m_asms.size(), m_asms.c_ptr()); @@ -776,6 +778,7 @@ public: if (!m.is_true(tmp)) { upper += m_weights[i]; } + TRACE("opt", tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";); CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";); } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index e737f9efe..d12fabfa7 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -71,9 +71,9 @@ namespace opt { } TRACE("opt", - tout << m_upper << ": "; + tout << "upper: " << m_upper << " assignments: "; for (unsigned i = 0; i < m_weights.size(); ++i) { - tout << (m_assignment[i]?"1":"0"); + tout << (m_assignment[i]?"T":"F"); } tout << "\n";); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b71826e9b..9b48707bd 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -830,6 +830,7 @@ namespace opt { void context::update_bound(bool is_lower) { expr_ref val(m); + if (!m_model.get()) return; bool override = true; for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4b1bd32b1..082a4a4b4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -948,6 +948,7 @@ namespace sat { } void solver::init_search() { + m_model_is_current = false; m_phase_counter = 0; m_phase_cache_on = false; m_conflicts_since_restart = 0; @@ -1036,6 +1037,7 @@ namespace sat { void solver::mk_model() { m_model.reset(); + m_model_is_current = true; unsigned num = num_vars(); m_model.resize(num, l_undef); for (bool_var v = 0; v < num; v++) { @@ -1738,6 +1740,7 @@ namespace sat { m_mus(); // ignore return value on cancelation. m_model.reset(); m_model.append(m_mus.get_model()); + m_model_is_current = true; } } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e83da892b..f2602ff25 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -76,8 +76,9 @@ namespace sat { random_gen m_rand; clause_allocator m_cls_allocator; cleaner m_cleaner; - model m_model; + model m_model; model_converter m_mc; + bool m_model_is_current; simplifier m_simplifier; scc m_scc; asymm_branch m_asymm_branch; @@ -270,6 +271,7 @@ namespace sat { public: lbool check(unsigned num_lits = 0, literal const* lits = 0); model const & get_model() const { return m_model; } + bool model_is_current() const { return m_model_is_current; } literal_vector const& get_core() const { return m_core; } model_converter const & get_model_converter() const { return m_mc; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index bd518faff..d86b2da77 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2852,7 +2852,7 @@ namespace smt { void context::init_assumptions(unsigned num_assumptions, expr * const * assumptions) { reset_assumptions(); - m_bool_var2assumption.reset(); + m_literal2assumption.reset(); m_unsat_core.reset(); if (num_assumptions > 0) { // We must give a chance to the theories to propagate before we create a new scope... @@ -2868,7 +2868,7 @@ namespace smt { proof * pr = m_manager.mk_asserted(curr_assumption); internalize_assertion(curr_assumption, pr, 0); literal l = get_literal(curr_assumption); - m_bool_var2assumption.insert(l.var(), curr_assumption); + m_literal2assumption.insert(l.index(), curr_assumption); // mark_as_relevant(l); <<< not needed // internalize_assertion marked l as relevant. SASSERT(is_relevant(l)); @@ -2877,7 +2877,7 @@ namespace smt { assign(l, mk_justification(justification_proof_wrapper(*this, pr))); else assign(l, b_justification::mk_axiom()); - m_assumptions.push_back(l.var()); + m_assumptions.push_back(l); get_bdata(l.var()).m_assumption = true; } } @@ -2887,10 +2887,10 @@ namespace smt { } void context::reset_assumptions() { - bool_var_vector::iterator it = m_assumptions.begin(); - bool_var_vector::iterator end = m_assumptions.end(); + literal_vector::iterator it = m_assumptions.begin(); + literal_vector::iterator end = m_assumptions.end(); for (; it != end; ++it) - get_bdata(*it).m_assumption = false; + get_bdata(it->var()).m_assumption = false; m_assumptions.reset(); } @@ -2907,10 +2907,8 @@ namespace smt { literal l = *it; TRACE("unsat_core_bug", tout << "answer literal: " << l << "\n";); SASSERT(get_bdata(l.var()).m_assumption); - SASSERT(m_bool_var2assumption.contains(l.var())); - expr * a = 0; - m_bool_var2assumption.find(l.var(), a); - SASSERT(a); + SASSERT(m_literal2assumption.contains(l.index())); + expr * a = m_literal2assumption[l.index()]; if (!already_found_assumptions.contains(a)) { already_found_assumptions.insert(a); m_unsat_core.push_back(a); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 42af9738b..d3dc8a492 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -201,9 +201,9 @@ namespace smt { // Unsat core extraction // // ----------------------------------- - typedef u_map bool_var2assumption; - bool_var_vector m_assumptions; - bool_var2assumption m_bool_var2assumption; // maps an expression associated with a literal to the original assumption + typedef u_map literal2assumption; + literal_vector m_assumptions; + literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption expr_ref_vector m_unsat_core; // -----------------------------------