From c5f231acdfab2a8032201fb213d169f818ac0cef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Nov 2017 08:16:41 -0800 Subject: [PATCH] debugging #1233 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_conflict_resolution.cpp | 38 +++++++++-------------------- src/smt/smt_context.cpp | 9 ++++++- src/smt/smt_context.h | 2 +- src/smt/theory_seq.cpp | 23 +++++++++++++++++ 4 files changed, 43 insertions(+), 29 deletions(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 6188c8b1a..02c38a2bd 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -313,8 +313,8 @@ namespace smt { SASSERT(var < static_cast(m_ctx.get_num_bool_vars())); TRACE("conflict", tout << "processing antecedent (level " << lvl << "):"; m_ctx.display_literal(tout, antecedent); - m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";); - + m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";); + if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) { m_ctx.set_mark(var); m_ctx.inc_bvar_activity(var); @@ -328,8 +328,7 @@ namespace smt { if (get_manager().has_trace_stream()) { get_manager().trace_stream() << "[resolve-lit] " << m_conflict_lvl - lvl << " "; - m_ctx.display_literal(get_manager().trace_stream(), ~antecedent); - get_manager().trace_stream() << "\n"; + m_ctx.display_literal(get_manager().trace_stream(), ~antecedent) << "\n"; } if (lvl == m_conflict_lvl) { @@ -391,7 +390,7 @@ namespace smt { << " search_lvl: " << m_ctx.get_search_level() << "\n"; tout << "js.kind: " << js.get_kind() << "\n"; tout << "consequent: " << consequent << ": "; - m_ctx.display_literal_verbose(tout, consequent); tout << "\n"; + m_ctx.display_literal_verbose(tout, consequent) << "\n"; m_ctx.display(tout, js); tout << "\n"; ); @@ -430,32 +429,16 @@ namespace smt { void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) { unmark_justifications(0); - TRACE("conflict", - tout << "before minimization:\n"; - m_ctx.display_literals(tout, m_lemma); - tout << "\n";); + TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n";); - TRACE("conflict_verbose", - tout << "before minimization:\n"; - m_ctx.display_literals_verbose(tout, m_lemma); - tout << "\n";); + TRACE("conflict_verbose",m_ctx.display_literals_verbose(tout << "before minimization:\n", m_lemma) << "\n";); if (m_params.m_minimize_lemmas) minimize_lemma(); - TRACE("conflict", - tout << "after minimization:\n"; - m_ctx.display_literals(tout, m_lemma); - tout << "\n";); - - TRACE("conflict_verbose", - tout << "after minimization:\n"; - m_ctx.display_literals_verbose(tout, m_lemma); - tout << "\n";); - - TRACE("conflict_bug", - m_ctx.display_literals_verbose(tout, m_lemma); - tout << "\n";); + TRACE("conflict", m_ctx.display_literals(tout << "after minimization:\n", m_lemma) << "\n";); + TRACE("conflict_verbose", m_ctx.display_literals_verbose(tout << "after minimization:\n", m_lemma) << "\n";); + TRACE("conflict_bug", m_ctx.display_literals_verbose(tout, m_lemma) << "\n";); literal_vector::iterator it = m_lemma.begin(); literal_vector::iterator end = m_lemma.end(); @@ -527,7 +510,8 @@ namespace smt { get_manager().trace_stream() << "\n"; } - TRACE("conflict", tout << "processing consequent: " << idx << " "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n"; + TRACE("conflict", tout << "processing consequent id: " << idx << " lit: " << consequent << " "; m_ctx.display_literal(tout, consequent); + m_ctx.display_literal_verbose(tout, consequent) << "\n"; tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n"; ); SASSERT(js != null_b_justification); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 30979fc4b..8819e37b6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -287,6 +287,13 @@ namespace smt { void context::assign_core(literal l, b_justification j, bool decision) { +#if 0 + // for debugging #1233 + if (l.var() == 11133 && l.sign()) { + std::cout << l << "\n"; + UNREACHABLE(); + } +#endif TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); @@ -902,7 +909,7 @@ namespace smt { } /** - \brief Propabate the boolean assignment when two equivalence classes are merged. + \brief Propagate the boolean assignment when two equivalence classes are merged. */ void context::propagate_bool_enode_assignment(enode * r1, enode * r2, enode * n1, enode * n2) { SASSERT(n1->is_bool()); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index d55e36f44..e50c03c8a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1237,7 +1237,7 @@ namespace smt { std::ostream& display_literal(std::ostream & out, literal l) const; - void display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m_manager, m_bool_var2expr.c_ptr()); } + std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m_manager, m_bool_var2expr.c_ptr()); return out; } void display_literal_info(std::ostream & out, literal l) const; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d55484384..caba4e92e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1298,6 +1298,21 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { display_deps(tout, dep); ); +#if 0 + //std::cout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n"; + //display_deps(std::cout, dep); + + for (literal lit : lits) { + SASSERT(ctx.get_assignment(lit) == l_true); + } + for (enode_pair p : eqs) { + if (p.first->get_root() != p.second->get_root()) { + std::cout << mk_pp(p.first->get_owner(), m) << " " << mk_pp(p.second->get_owner(), m) << "\n"; + } + SASSERT(p.first->get_root() == p.second->get_root()); + } +#endif + justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); @@ -3027,6 +3042,8 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { enode* n1 = ctx.get_enode(num); enode* n2 = ctx.get_enode(e1); res = m_util.str.mk_string(symbol(val.to_string().c_str())); +#if 1 + // TBD remove this: using roots is unsound for propagation. if (n1->get_root() == n2->get_root()) { result = res; deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2))); @@ -3037,6 +3054,12 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false)); result = e; } +#else + TRACE("seq", tout << "add axiom\n";); + add_axiom(~mk_eq(num, e1, false), mk_eq(e, res, false)); + add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false)); + result = e; +#endif } else { result = e;