From 184ae7211e8f51f39f6bc9e540221684f7912cbd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Oct 2018 10:00:57 -0700 Subject: [PATCH] fix #1897 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 14 +++---- src/smt/smt_context.h | 16 ++++++++ src/smt/smt_context_pp.cpp | 12 ++++++ src/smt/theory_datatype.cpp | 77 +++++++++++++++++++------------------ src/smt/theory_lra.cpp | 16 ++++---- 5 files changed, 82 insertions(+), 53 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 17a7ce3a3..41f11dca2 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -494,7 +494,7 @@ namespace smt { try { TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); - TRACE("add_eq_detail", tout << "assigning\n" << mk_pp(n1->get_owner(), m_manager) << "\n" << mk_pp(n2->get_owner(), m_manager) << "\n"; + TRACE("add_eq_detail", tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n"; tout << "kind: " << js.get_kind() << "\n";); m_stats.m_num_add_eq++; @@ -1232,7 +1232,7 @@ namespace smt { if (depth == 0) return false; if (r1->get_num_parents() < SMALL_NUM_PARENTS) { - TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";); + TRACE("is_ext_diseq", tout << enode_pp(n1, *this) << " " << enode_pp(n2, *this) << " " << depth << "\n";); for (enode * p1 : enode::parents(r1)) { if (!is_relevant(p1)) continue; @@ -1241,7 +1241,7 @@ namespace smt { if (!p1->is_cgr()) continue; func_decl * f = p1->get_decl(); - TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";); + TRACE("is_ext_diseq", tout << "p1: " << enode_pp(p1, *this) << "\n";); unsigned num_args = p1->get_num_args(); for (enode * p2 : enode::parents(r2)) { if (!is_relevant(p2)) @@ -1250,7 +1250,7 @@ namespace smt { continue; if (!p2->is_cgr()) continue; - TRACE("is_ext_diseq", tout << "p2: " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";); + TRACE("is_ext_diseq", tout << "p2: " << enode_pp(p2, *this) << "\n";); if (p1->get_root() != p2->get_root() && p2->get_decl() == f && p2->get_num_args() == num_args) { unsigned j = 0; for (j = 0; j < num_args; j++) { @@ -1264,7 +1264,7 @@ namespace smt { break; } if (j == num_args) { - TRACE("is_ext_diseq", tout << "found parents: " << mk_bounded_pp(p1->get_owner(), m_manager) << " " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";); + TRACE("is_ext_diseq", tout << "found parents: " << enode_pp(p1, *this) << " " << enode_pp(p2, *this) << "\n";); if (is_ext_diseq(p1, p2, depth - 1)) return true; } @@ -1770,7 +1770,7 @@ namespace smt { void context::set_conflict(const b_justification & js, literal not_l) { if (!inconsistent()) { - TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); ); + TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout << " ", js); ); m_conflict = js; m_not_l = not_l; } @@ -4290,7 +4290,7 @@ namespace smt { for (enode * parent : enode::parents(n)) { family_id fid = parent->get_owner()->get_family_id(); if (fid != th_id && fid != m_manager.get_basic_family_id()) { - TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";); + TRACE("is_shared", tout << enode_pp(n, *this) << "\nis shared because of:\n" << enode_pp(parent, *this) << "\n";); return true; } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 5733829a3..d0c9cc776 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1609,6 +1609,22 @@ namespace smt { void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); } }; + struct enode_eq_pp { + context const& ctx; + enode_pair const& p; + enode_eq_pp(enode_pair const& p, context const& ctx): ctx(ctx), p(p) {} + }; + + std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p); + + struct enode_pp { + context const& ctx; + enode* n; + enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {} + }; + + std::ostream& operator<<(std::ostream& out, enode_pp const& p); + }; #endif /* SMT_CONTEXT_H_ */ diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index fb67d91d6..5dea80f5e 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -603,5 +603,17 @@ namespace smt { display(out, j); } + std::ostream& operator<<(std::ostream& out, enode_pp const& p) { + ast_manager& m = p.ctx.get_manager(); + enode* n = p.n; + return out << "[#" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m) << "]"; + } + + std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) { + return out << enode_pp(p.p.first, p.ctx) << " = " << enode_pp(p.p.second, p.ctx) << "\n"; + } + + + }; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 049555297..6aa49efae 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -365,7 +365,7 @@ namespace smt { if (!is_recognizer(n)) return; TRACE("datatype", tout << "assigning recognizer: #" << n->get_owner_id() << " is_true: " << is_true << "\n" - << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";); + << enode_pp(n, ctx) << "\n";); SASSERT(n->get_num_args() == 1); enode * arg = n->get_arg(0); theory_var tv = arg->get_th_var(get_id()); @@ -393,11 +393,10 @@ namespace smt { } void theory_datatype::relevant_eh(app * n) { - TRACE("datatype", tout << "relevant_eh: " << mk_bounded_pp(n, get_manager()) << "\n";); context & ctx = get_context(); + TRACE("datatype", tout << "relevant_eh: " << mk_pp(n, get_manager()) << "\n";); SASSERT(ctx.relevancy()); if (is_recognizer(n)) { - TRACE("datatype", tout << "relevant_eh: #" << n->get_id() << "\n" << mk_bounded_pp(n, get_manager()) << "\n";); SASSERT(ctx.e_internalized(n)); enode * e = ctx.get_enode(n); theory_var v = e->get_arg(0)->get_th_var(get_id()); @@ -483,31 +482,41 @@ namespace smt { SASSERT(app->get_root() == root->get_root()); if (app != root) m_used_eqs.push_back(enode_pair(app, root)); + + TRACE("datatype", + tout << "occurs_check\n"; + for (enode_pair const& p : m_used_eqs) { + tout << enode_eq_pp(p, get_context()); + }); } // start exploring subgraph below `app` bool theory_datatype::occurs_check_enter(enode * app) { - oc_mark_on_stack(app); - theory_var v = app->get_root()->get_th_var(get_id()); - if (v != null_theory_var) { - v = m_find.find(v); - var_data * d = m_var_data[v]; - if (d->m_constructor) { - for (enode * arg : enode::args(d->m_constructor)) { - if (oc_cycle_free(arg)) { - continue; - } - if (oc_on_stack(arg)) { - // arg was explored before app, and is still on the stack: cycle - occurs_check_explain(app, arg); - return true; - } - // explore `arg` (with parent `app`) - if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) { - m_parent.insert(arg->get_root(), app); - oc_push_stack(arg); - } - } + app = app->get_root(); + theory_var v = app->get_th_var(get_id()); + if (v == null_theory_var) { + return false; + } + v = m_find.find(v); + var_data * d = m_var_data[v]; + if (!d->m_constructor) { + return false; + } + enode * parent = d->m_constructor; + oc_mark_on_stack(parent); + for (enode * arg : enode::args(parent)) { + if (oc_cycle_free(arg)) { + continue; + } + if (oc_on_stack(arg)) { + // arg was explored before app, and is still on the stack: cycle + occurs_check_explain(parent, arg); + return true; + } + // explore `arg` (with paren) + if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) { + m_parent.insert(arg->get_root(), parent); + oc_push_stack(arg); } } return false; @@ -521,7 +530,7 @@ namespace smt { a3 = cons(v3, a1) */ bool theory_datatype::occurs_check(enode * n) { - TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";); + TRACE("datatype", tout << "occurs check: " << enode_pp(n, get_context()) << "\n";); m_stats.m_occurs_check++; bool res = false; @@ -535,7 +544,7 @@ namespace smt { if (oc_cycle_free(app)) continue; - TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";); + TRACE("datatype", tout << "occurs check loop: " << enode_pp(app, get_context()) << (op==ENTER?" enter":" exit")<< "\n";); switch (op) { case ENTER: @@ -553,12 +562,6 @@ namespace smt { context & ctx = get_context(); region & r = ctx.get_region(); ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr()))); - TRACE("datatype", - tout << "occurs_check: true\n"; - for (enode_pair const& p : m_used_eqs) { - tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n"; - tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n"; - }); } return res; } @@ -613,7 +616,7 @@ namespace smt { var_data * d = m_var_data[v]; out << "v" << v << " #" << get_enode(v)->get_owner_id() << " -> v" << m_find.find(v) << " "; if (d->m_constructor) - out << mk_bounded_pp(d->m_constructor->get_owner(), get_manager()); + out << enode_pp(d->m_constructor, get_context()); else out << "(null)"; out << "\n"; @@ -778,11 +781,11 @@ namespace smt { SASSERT(!lits.empty()); region & reg = ctx.get_region(); TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n"; - for (unsigned i = 0; i < lits.size(); i++) { - ctx.display_detailed_literal(tout, lits[i]); tout << "\n"; + for (literal l : lits) { + ctx.display_detailed_literal(tout, l); tout << "\n"; } - for (unsigned i = 0; i < eqs.size(); i++) { - tout << mk_ismt2_pp(eqs[i].first->get_owner(), get_manager()) << " = " << mk_ismt2_pp(eqs[i].second->get_owner(), get_manager()) << "\n"; + for (auto const& p : eqs) { + tout << enode_eq_pp(p, ctx); }); ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr()))); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4a04fdaaf..0b25aa626 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1361,8 +1361,7 @@ public: } enode* n2 = get_enode(other); if (n1->get_root() != n2->get_root()) { - TRACE("arith", tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n"; - tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n"; + TRACE("arith", tout << enode_eq_pp(enode_pair(n1, n2), ctx()); tout << "v" << v << " = " << "v" << other << "\n";); m_assume_eq_candidates.push_back(std::make_pair(v, other)); result = true; @@ -2800,15 +2799,15 @@ public: get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr)); TRACE("arith", - for (unsigned i = 0; i < m_core.size(); ++i) { - ctx().display_detailed_literal(tout, m_core[i]); + for (literal c : m_core) { + ctx().display_detailed_literal(tout, c); tout << "\n"; } - for (unsigned i = 0; i < m_eqs.size(); ++i) { - tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n"; + for (enode_pair const& p : m_eqs) { + tout << enode_eq_pp(p, ctx()); } tout << " ==> "; - tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n"; + tout << enode_pp(x, ctx()) << " = " << enode_pp(y, ctx()) << "\n"; ); // parameters are TBD. @@ -3371,8 +3370,7 @@ public: break; } case equality_source: - out << mk_pp(m_equalities[idx].first->get_owner(), m) << " = " - << mk_pp(m_equalities[idx].second->get_owner(), m) << "\n"; + out << enode_eq_pp(m_equalities[idx], ctx()); break; case definition_source: { theory_var v = m_definitions[idx];