From bed2097fc420f7596963e8e42defd3905b1a64c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Mar 2020 10:35:53 -0700 Subject: [PATCH] fix #3076 - need to apply relevancy propagation in mk_bits. Assume bv v is already relevant but did not have bits associated with it, the bits need to then be marked as relevant Signed-off-by: Nikolaj Bjorner --- src/qe/qsat.cpp | 5 ++--- src/smt/smt_context.cpp | 5 ++++- src/smt/smt_setup.cpp | 3 ++- src/smt/theory_bv.cpp | 33 ++++++++++++++++++++++----------- src/smt/theory_bv.h | 1 + 5 files changed, 31 insertions(+), 16 deletions(-) diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 73ed9ff52..c22142b8c 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -548,11 +548,10 @@ namespace qe { m_solver(mk_smt_solver(m, m_params, symbol::null)) { m_params.set_bool("model", true); - m_params.set_uint("relevancy_lvl", 0); + m_params.set_uint("relevancy", 0); m_params.set_uint("case_split_strategy", CS_ACTIVITY_WITH_CACHE); m_solver->updt_params(m_params); - } - + } solver& s() { return *m_solver; } solver const& s() const { return *m_solver; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 789fa1c2e..eceeb2fbc 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -149,6 +149,9 @@ namespace smt { void context::updt_params(params_ref const& p) { m_params.append(p); m_asserted_formulas.updt_params(p); + if (!m_setup.already_configured()) { + m_fparams.updt_params(p); + } } unsigned context::relevancy_lvl() const { @@ -308,7 +311,7 @@ namespace smt { } void context::assign_core(literal l, b_justification j, bool decision) { - CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << (decision?"decision: ":"propagating: ") << l << " "; + CTRACE("assign_core", l.var() == 2816, tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_smt2(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); m_assigned_literals.push_back(l); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index cc4dff65e..80d07cc56 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -152,6 +152,7 @@ namespace smt { ptr_vector fmls; m_context.get_asserted_formulas(fmls); st.collect(fmls.size(), fmls.c_ptr()); + TRACE("setup", st.display_primitive(tout);); IF_VERBOSE(1000, st.display_primitive(verbose_stream());); if (m_logic == "QF_UF") setup_QF_UF(st); @@ -947,7 +948,7 @@ namespace smt { ptr_vector fmls; m_context.get_asserted_formulas(fmls); st.collect(fmls.size(), fmls.c_ptr()); - TRACE("setup", tout << "setup_unknown\n";); + TRACE("setup", tout << "setup_unknown\n";); setup_arith(); setup_arrays(); setup_bv(); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index e2b751f8e..c59fecdc3 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -53,6 +53,7 @@ namespace smt { app * owner = n->get_owner(); unsigned bv_size = get_bv_size(n); context & ctx = get_context(); + bool is_relevant = ctx.is_relevant(n); literal_vector & bits = m_bits[v]; TRACE("bv", tout << "v" << v << "\n";); bits.reset(); @@ -61,6 +62,9 @@ namespace smt { ctx.internalize(bit, true); bool_var b = ctx.get_bool_var(bit); bits.push_back(literal(b)); + if (is_relevant && !ctx.is_relevant(b)) { + ctx.mark_as_relevant(b); + } } } @@ -885,9 +889,7 @@ namespace smt { find_wpos(v); } - bool theory_bv::internalize_term(app * term) { - scoped_suspend_rlimit _suspend_cancel(get_manager().limit()); - try { + bool theory_bv::internalize_term_core(app * term) { SASSERT(term->get_family_id() == get_family_id()); TRACE("bv", tout << "internalizing term: " << mk_bounded_pp(term, get_manager()) << "\n";); if (approximate_term(term)) { @@ -945,6 +947,12 @@ namespace smt { UNREACHABLE(); return false; } + } + + bool theory_bv::internalize_term(app * term) { + scoped_suspend_rlimit _suspend_cancel(get_manager().limit()); + try { + return internalize_term_core(term); } catch (z3_exception& ex) { IF_VERBOSE(1, verbose_stream() << "internalize_term: " << ex.msg() << "\n";); @@ -1129,7 +1137,6 @@ namespace smt { } } return false; - } void theory_bv::apply_sort_cnstr(enode * n, sort * s) { @@ -1236,7 +1243,7 @@ namespace smt { void theory_bv::assign_eh(bool_var v, bool is_true) { atom * a = get_bv2a(v); - TRACE("bv", tout << "assert: b" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";); + TRACE("bv", tout << "assert: p" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";); if (a->is_bit()) { // The following optimization is not correct. // Boolean variables created for performing bit-blasting are reused. @@ -1246,6 +1253,9 @@ namespace smt { // TRACE("bv", tout << "has th_justification\n";); // return; // } + //for (auto kv : m_prop_queue) { + // std::cout << "v" << kv.first << "[" << kv.second << "]\n"; + //} m_prop_queue.reset(); bit_atom * b = static_cast(a); var_pos_occ * curr = b->m_occs; @@ -1253,7 +1263,6 @@ namespace smt { m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx)); curr = curr->m_next; } - TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";); propagate_bits(); #if WATCH_DISEQ @@ -1286,7 +1295,7 @@ namespace smt { continue; } theory_var v2 = next(v); - TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << " " << ctx.get_scope_level() << "\n";); + TRACE("bv", tout << "propagating v" << v << " #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << " " << ctx.get_scope_level() << "\n";); literal antecedent = bit; if (val == l_false) { @@ -1307,7 +1316,7 @@ namespace smt { } assign_bit(consequent, v, v2, idx, antecedent, false); if (ctx.inconsistent()) { - TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";); + TRACE("bv", tout << "inconsistent " << bit << " " << bit2 << "\n";); m_prop_queue.reset(); return; } @@ -1389,7 +1398,7 @@ namespace smt { void theory_bv::relevant_eh(app * n) { ast_manager & m = get_manager(); context & ctx = get_context(); - TRACE("bv", tout << "relevant: " << mk_pp(n, m) << "\n";); + TRACE("bv", tout << "relevant: " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";); if (m.is_bool(n)) { bool_var v = ctx.get_bool_var(n); atom * a = get_bv2a(v); @@ -1425,6 +1434,7 @@ namespace smt { void theory_bv::push_scope_eh() { theory::push_scope_eh(); m_trail_stack.push_scope(); + // check_invariant(); #if WATCH_DISEQ m_diseq_watch_lim.push_back(m_diseq_watch_trail.size()); #endif @@ -1504,7 +1514,7 @@ namespace smt { void theory_bv::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { - TRACE("bv", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";); + TRACE("bv", tout << "merging: v" << v1 << " #" << get_enode(v1)->get_owner_id() << " v" << v2 << " #" << get_enode(v2)->get_owner_id() << "\n";); TRACE("bv_bit_prop", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";); if (!merge_zero_one_bits(r1, r2)) { TRACE("bv", tout << "conflict detected\n";); @@ -1540,6 +1550,7 @@ namespace smt { SASSERT(bit1 != ~bit2); lbool val1 = ctx.get_assignment(bit1); lbool val2 = ctx.get_assignment(bit2); + TRACE("bv", tout << "merge v" << v1 << " " << bit1 << ":= " << val1 << " " << bit2 << ":= " << val2 << "\n";); if (val1 == val2) continue; changed = true; @@ -1741,7 +1752,7 @@ namespace smt { context & ctx = get_context(); literal_vector const & bits = m_bits[v]; for (literal lit : bits) { - out << " "; + out << " " << lit << ":"; ctx.display_literal(out, lit); } numeral val; diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 6433c918d..fc6cdac30 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -173,6 +173,7 @@ namespace smt { void fixed_var_eh(theory_var v); void add_fixed_eq(theory_var v1, theory_var v2); bool get_fixed_value(theory_var v, numeral & result) const; + bool internalize_term_core(app * term); void internalize_num(app * n); void internalize_add(app * n); void internalize_sub(app * n);