diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 022ea52f3..abd47f156 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -782,7 +782,7 @@ namespace smt { class compiler { context & m_context; - ast_manager & m_ast_manager; + ast_manager & m; code_tree_manager & m_ct_manager; label_hasher & m_lbl_hasher; bool m_use_filters; @@ -812,23 +812,22 @@ namespace smt { unsigned_vector m_to_reset; ptr_vector m_compatible; ptr_vector m_incompatible; - ptr_vector m_seq; void set_register(unsigned reg, expr * p) { - m_registers.setx(reg, p, 0); + m_registers.setx(reg, p, nullptr); } check_mark get_check_mark(unsigned reg) const { return m_mark.get(reg, NOT_CHECKED); } - void set_check_mark(unsigned reg, check_mark m) { - m_mark.setx(reg, m, NOT_CHECKED); + void set_check_mark(unsigned reg, check_mark cm) { + m_mark.setx(reg, cm, NOT_CHECKED); } void init(code_tree * t, quantifier * qa, app * mp, unsigned first_idx) { - SASSERT(m_ast_manager.is_pattern(mp)); + SASSERT(m.is_pattern(mp)); #ifdef Z3DEBUG for (auto cm : m_mark) { SASSERT(cm == NOT_CHECKED); @@ -924,6 +923,7 @@ namespace smt { for (unsigned reg : m_todo) { expr * p = m_registers[reg]; SASSERT(!is_quantifier(p)); + TRACE("mam", tout << "lin: " << reg << " " << get_check_mark(reg) << " " << is_var(p) << "\n";); if (is_var(p)) { unsigned var_id = to_var(p)->get_idx(); if (m_vars[var_id] != -1) @@ -933,6 +933,7 @@ namespace smt { continue; } + SASSERT(is_app(p)); if (to_app(p)->is_ground()) { @@ -1229,8 +1230,8 @@ namespace smt { #ifdef Z3DEBUG for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { - CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m_ast_manager) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; - tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m_ast_manager) << "\n"; + CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; + tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n"; tout << "tree:\n" << *m_tree << "\n"; ); SASSERT(m_vars[i] >= 0); @@ -1285,6 +1286,7 @@ namespace smt { return nullptr; // it is unlikely we will find a compatible node } if (curr_compatibility > max_compatibility) { + TRACE("mam", tout << "better child " << best_child << " -> " << curr_child << "\n";); best_child = curr_child; max_compatibility = curr_compatibility; } @@ -1406,7 +1408,7 @@ namespace smt { bool is_semi_compatible(filter * instr) const { unsigned reg = instr->m_reg; return - m_registers[reg] != 0 && + m_registers[reg] != nullptr && get_check_mark(reg) == NOT_CHECKED && is_app(m_registers[reg]) && !is_ground(m_registers[reg]); @@ -1497,17 +1499,18 @@ namespace smt { while (curr != nullptr && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) { TRACE("mam_compiler_detail", tout << "processing instr: " << *curr << "\n";); switch (curr->m_opcode) { - case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: - if (is_compatible(static_cast(curr))) { + case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: { + bind* bnd = static_cast(curr); + if (is_compatible(bnd)) { TRACE("mam_compiler_detail", tout << "compatible\n";); - unsigned ireg = static_cast(curr)->m_ireg; + unsigned ireg = bnd->m_ireg; SASSERT(m_todo.contains(ireg)); m_todo.erase(ireg); set_check_mark(ireg, NOT_CHECKED); m_compatible.push_back(curr); app * app = to_app(m_registers[ireg]); - unsigned oreg = static_cast(curr)->m_oreg; - unsigned num_args = static_cast(curr)->m_num_args; + unsigned oreg = bnd->m_oreg; + unsigned num_args = bnd->m_num_args; for (unsigned i = 0; i < num_args; i++) { set_register(oreg + i, app->get_arg(i)); m_todo.push_back(oreg + i); @@ -1518,19 +1521,21 @@ namespace smt { m_incompatible.push_back(curr); } break; - case CHECK: - if (is_compatible(static_cast(curr))) { + } + case CHECK: { + check* chk = static_cast(curr); + if (is_compatible(chk)) { TRACE("mam_compiler_detail", tout << "compatible\n";); - unsigned reg = static_cast(curr)->m_reg; + unsigned reg = chk->m_reg; SASSERT(m_todo.contains(reg)); m_todo.erase(reg); set_check_mark(reg, NOT_CHECKED); m_compatible.push_back(curr); } - else if (m_use_filters && is_semi_compatible(static_cast(curr))) { + else if (m_use_filters && is_semi_compatible(chk)) { TRACE("mam_compiler_detail", tout << "semi compatible\n";); - unsigned reg = static_cast(curr)->m_reg; - enode * n1 = static_cast(curr)->m_enode; + unsigned reg = chk->m_reg; + enode * n1 = chk->m_enode; // n1->has_lbl_hash may be false, even // when update_filters is invoked before // executing this method. @@ -1556,10 +1561,11 @@ namespace smt { m_incompatible.push_back(curr); } else { - TRACE("mam_compiler_detail", tout << "incompatible\n";); + TRACE("mam_compiler_detail", tout << "incompatible " << chk->m_reg << "\n";); m_incompatible.push_back(curr); } break; + } case COMPARE: if (is_compatible(static_cast(curr))) { TRACE("mam_compiler_detail", tout << "compatible\n";); @@ -1567,8 +1573,10 @@ namespace smt { unsigned reg2 = static_cast(curr)->m_reg2; SASSERT(m_todo.contains(reg2)); m_todo.erase(reg2); + set_check_mark(reg2, NOT_CHECKED); if (is_var(m_registers[reg1])) { m_todo.erase(reg1); + set_check_mark(reg1, NOT_CHECKED); unsigned var_id = to_var(m_registers[reg1])->get_idx(); if (m_vars[var_id] == -1) m_vars[var_id] = reg1; @@ -1592,44 +1600,47 @@ namespace smt { m_incompatible.push_back(curr); } break; - case FILTER: + case FILTER: { + filter *flt = static_cast(curr); SASSERT(m_use_filters); - if (is_compatible(static_cast(curr))) { - TRACE("mam_compiler_detail", tout << "compatible\n";); - unsigned reg = static_cast(curr)->m_reg; + if (is_compatible(flt)) { + unsigned reg = flt->m_reg; + TRACE("mam_compiler_detail", tout << "compatible " << reg << "\n";); CTRACE("mam_compiler_bug", !m_todo.contains(reg), { - for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; } - tout << "\nregisters:\n"; - for (unsigned i = 0; i < m_registers.size(); i++) { if (m_registers[i]) { tout << i << ":\n" << mk_pp(m_registers[i], m_ast_manager) << "\n"; } } - tout << "quantifier:\n" << mk_pp(m_qa, m_ast_manager) << "\n"; - tout << "pattern:\n" << mk_pp(m_mp, m_ast_manager) << "\n"; - }); + for (unsigned t : m_todo) { tout << t << " "; } + tout << "\nregisters:\n"; + unsigned i = 0; + for (expr* r : m_registers) { if (r) { tout << i++ << ":\n" << mk_pp(r, m) << "\n"; } } + tout << "quantifier:\n" << mk_pp(m_qa, m) << "\n"; + tout << "pattern:\n" << mk_pp(m_mp, m) << "\n"; + }); SASSERT(m_todo.contains(reg)); - if (static_cast(curr)->m_lbl_set.size() == 1) + if (flt->m_lbl_set.size() == 1) set_check_mark(reg, CHECK_SINGLETON); else set_check_mark(reg, CHECK_SET); m_compatible.push_back(curr); } - else if (is_semi_compatible(static_cast(curr))) { - TRACE("mam_compiler_detail", tout << "semi compatible\n";); - unsigned reg = static_cast(curr)->m_reg; + else if (is_semi_compatible(flt)) { + unsigned reg = flt->m_reg; + TRACE("mam_compiler_detail", tout << "semi compatible " << reg << "\n";); CTRACE("mam_compiler_bug", !m_todo.contains(reg), { - for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; } - tout << "\nregisters:\n"; - for (unsigned i = 0; i < m_registers.size(); i++) { if (m_registers[i]) { tout << i << ":\n" << mk_pp(m_registers[i], m_ast_manager) << "\n"; } } - tout << "quantifier:\n" << mk_pp(m_qa, m_ast_manager) << "\n"; - tout << "pattern:\n" << mk_pp(m_mp, m_ast_manager) << "\n"; - }); + for (unsigned t : m_todo) { tout << t << " "; } + tout << "\nregisters:\n"; + unsigned i = 0; + for (expr* r : m_registers) { if (r) { tout << i++ << ":\n" << mk_pp(r, m) << "\n"; } } + tout << "quantifier:\n" << mk_pp(m_qa, m) << "\n"; + tout << "pattern:\n" << mk_pp(m_mp, m) << "\n"; + }); SASSERT(m_todo.contains(reg)); unsigned h = get_pat_lbl_hash(reg); TRACE("mam_lbl_bug", - tout << "curr_set: " << static_cast(curr)->m_lbl_set << "\n"; + tout << "curr_set: " << flt->m_lbl_set << "\n"; tout << "new hash: " << h << "\n";); set_check_mark(reg, CHECK_SET); - approx_set const & s = static_cast(curr)->m_lbl_set; + approx_set const & s = flt->m_lbl_set; if (s.size() > 1) { - m_ct_manager.insert_new_lbl_hash(static_cast(curr), h); + m_ct_manager.insert_new_lbl_hash(flt, h); m_compatible.push_back(curr); } else { @@ -1646,6 +1657,7 @@ namespace smt { m_incompatible.push_back(curr); } break; + } default: TRACE("mam_compiler_detail", tout << "incompatible\n";); m_incompatible.push_back(curr); @@ -1665,6 +1677,7 @@ namespace smt { SASSERT(curr->m_opcode == CHOOSE); choose * first_child = static_cast(curr); choose * best_child = find_best_child(first_child); + TRACE("mam", tout << "best child " << best_child << "\n";); if (best_child == nullptr) { // There is no compatible child // Suppose the sequence is: @@ -1728,7 +1741,7 @@ namespace smt { public: compiler(context & ctx, code_tree_manager & ct_mg, label_hasher & h, bool use_filters = true): m_context(ctx), - m_ast_manager(ctx.get_manager()), + m(ctx.get_manager()), m_ct_manager(ct_mg), m_lbl_hasher(h), m_use_filters(use_filters) { @@ -1742,14 +1755,14 @@ namespace smt { - first_idx: index of mp that will be the "head" (first to be processed) of the multi-pattern. */ code_tree * mk_tree(quantifier * qa, app * mp, unsigned first_idx, bool filter_candidates) { - SASSERT(m_ast_manager.is_pattern(mp)); + SASSERT(m.is_pattern(mp)); app * p = to_app(mp->get_arg(first_idx)); unsigned num_args = p->get_num_args(); code_tree * r = m_ct_manager.mk_code_tree(p->get_decl(), num_args, filter_candidates); init(r, qa, mp, first_idx); linearise(r->m_root, first_idx); r->m_num_choices = m_num_choices; - TRACE("mam_compiler", tout << "new tree for:\n" << mk_pp(mp, m_ast_manager) << "\n" << *r;); + TRACE("mam_compiler", tout << "new tree for:\n" << mk_pp(mp, m) << "\n" << *r;); return r; } @@ -1767,7 +1780,7 @@ namespace smt { return; } m_is_tmp_tree = is_tmp_tree; - TRACE("mam_compiler", tout << "updating tree with:\n" << mk_pp(mp, m_ast_manager) << "\n";); + TRACE("mam_compiler", tout << "updating tree with:\n" << mk_pp(mp, m) << "\n";); TRACE("mam_bug", tout << "before insertion\n" << *tree << "\n";); if (!is_tmp_tree) m_ct_manager.save_num_regs(tree); @@ -1783,7 +1796,10 @@ namespace smt { } TRACE("mam_bug", tout << "m_num_choices: " << m_num_choices << "\n"; - tout << "new tree:\n" << *tree;); + tout << "new tree:\n" << *tree; + tout << "todo "; + for (auto t : m_todo) tout << t << " "; + tout << "\n";); } }; @@ -1828,7 +1844,7 @@ namespace smt { class interpreter { context & m_context; - ast_manager & m_ast_manager; + ast_manager & m; mam & m_mam; bool m_use_filters; enode_vector m_registers; @@ -1870,7 +1886,7 @@ namespace smt { void update_max_generation(enode * n, enode * prev) { m_max_generation = std::max(m_max_generation, n->get_generation()); - if (m_ast_manager.has_trace_stream()) + if (m.has_trace_stream()) m_used_enodes.push_back(std::make_tuple(prev, n)); } @@ -1980,7 +1996,7 @@ namespace smt { public: interpreter(context & ctx, mam & ma, bool use_filters): m_context(ctx), - m_ast_manager(ctx.get_manager()), + m(ctx.get_manager()), m_mam(ma), m_use_filters(use_filters) { m_args.resize(INIT_ARGS_SIZE); @@ -1991,8 +2007,8 @@ namespace smt { void init(code_tree * t) { TRACE("mam_bug", tout << "preparing to match tree:\n" << *t << "\n";); - m_registers.reserve(t->get_num_regs(), 0); - m_bindings.reserve(t->get_num_regs(), 0); + m_registers.reserve(t->get_num_regs(), nullptr); + m_bindings.reserve(t->get_num_regs(), nullptr); if (m_backtrack_stack.size() < t->get_num_choices()) m_backtrack_stack.resize(t->get_num_choices()); } @@ -2002,7 +2018,7 @@ namespace smt { init(t); if (t->filter_candidates()) { for (enode* app : t->get_candidates()) { - TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); + TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m) << "\n";); if (!app->is_marked() && app->is_cgr()) { if (m_context.resource_limits_exceeded() || !execute_core(t, app)) return; @@ -2016,7 +2032,7 @@ namespace smt { } else { for (enode* app : t->get_candidates()) { - TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); + TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m) << "\n";); if (app->is_cgr()) { TRACE("trigger_bug", tout << "is_cgr\n";); if (m_context.resource_limits_exceeded() || !execute_core(t, app)) @@ -2215,7 +2231,7 @@ namespace smt { if (m_use_filters) out << ", lbls: " << n->get_root()->get_lbls() << " "; out << "\n"; - out << mk_pp(n->get_owner(), m_ast_manager) << "\n"; + out << mk_pp(n->get_owner(), m) << "\n"; } } @@ -2257,7 +2273,7 @@ namespace smt { } bool interpreter::execute_core(code_tree * t, enode * n) { - TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n";); + TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m) << "\n";); unsigned since_last_check = 0; #ifdef _PROFILE_MAM @@ -2279,7 +2295,7 @@ namespace smt { m_pattern_instances.push_back(n); m_max_generation = n->get_generation(); - if (m_ast_manager.has_trace_stream()) { + if (m.has_trace_stream()) { m_used_enodes.reset(); m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level } @@ -2378,7 +2394,7 @@ namespace smt { goto backtrack; // We will use the common root when instantiating the quantifier => log the necessary equalities - if (m_ast_manager.has_trace_stream()) { + if (m.has_trace_stream()) { m_used_enodes.push_back(std::make_tuple(m_n1, m_n1->get_root())); m_used_enodes.push_back(std::make_tuple(m_n2, m_n2->get_root())); } @@ -2395,7 +2411,7 @@ namespace smt { goto backtrack; // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log - if (m_ast_manager.has_trace_stream()) { + if (m.has_trace_stream()) { m_used_enodes.push_back(std::make_tuple(m_n1, m_n2)); } @@ -2443,7 +2459,7 @@ namespace smt { m_app = get_first_f_app(static_cast(m_pc)->m_label, static_cast(m_pc)->m_num_args, m_n1); \ if (!m_app) \ goto backtrack; \ - TRACE("mam_int", tout << "bind candidate: " << mk_pp(m_app->get_owner(), m_ast_manager) << "\n";); \ + TRACE("mam_int", tout << "bind candidate: " << mk_pp(m_app->get_owner(), m) << "\n";); \ m_backtrack_stack[m_top].m_instr = m_pc; \ m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation; \ m_backtrack_stack[m_top].m_old_used_enodes_size = m_curr_used_enodes_size; \ @@ -2581,7 +2597,7 @@ namespace smt { if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \ goto backtrack; \ update_max_generation(m_n1, nullptr); \ - if (m_ast_manager.has_trace_stream()) { \ + if (m.has_trace_stream()) { \ for (unsigned i = 0; i < static_cast(m_pc)->m_num_args; ++i) { \ m_used_enodes.push_back(std::make_tuple(m_n1->get_arg(i), m_n1->get_arg(i)->get_root())); \ } \ @@ -2593,7 +2609,7 @@ namespace smt { #define SET_VAR(IDX) \ m_args[IDX] = m_registers[static_cast(m_pc)->m_iregs[IDX]]; \ if (m_use_filters && static_cast(m_pc)->m_lbl_set.empty_intersection(m_args[IDX]->get_root()->get_plbls())) { \ - TRACE("trigger_bug", tout << "m_args[IDX]->get_root():\n" << mk_ismt2_pp(m_args[IDX]->get_root()->get_owner(), m_ast_manager) << "\n"; \ + TRACE("trigger_bug", tout << "m_args[IDX]->get_root():\n" << mk_ismt2_pp(m_args[IDX]->get_root()->get_owner(), m) << "\n"; \ tout << "cgr set: "; static_cast(m_pc)->m_lbl_set.display(tout); tout << "\n"; \ tout << "node set: "; m_args[IDX]->get_root()->get_plbls().display(tout); tout << "\n";); \ goto backtrack; \ @@ -2657,7 +2673,7 @@ namespace smt { if (m_app == nullptr) goto backtrack; m_pattern_instances.push_back(m_app); - TRACE("mam_int", tout << "continue candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); + TRACE("mam_int", tout << "continue candidate:\n" << mk_ll_pp(m_app->get_owner(), m);); for (unsigned i = 0; i < m_num_args; i++) m_registers[m_oreg+i] = m_app->get_arg(i); m_pc = m_pc->m_next; @@ -2677,7 +2693,7 @@ namespace smt { backtrack_point & bp = m_backtrack_stack[m_top - 1]; m_max_generation = bp.m_old_max_generation; - if (m_ast_manager.has_trace_stream()) + if (m.has_trace_stream()) m_used_enodes.shrink(bp.m_old_used_enodes_size); TRACE("mam_int", tout << "backtrack top: " << bp.m_instr << " " << *(bp.m_instr) << "\n";); @@ -2720,7 +2736,7 @@ namespace smt { goto backtrack; \ } \ bp.m_curr = m_app; \ - TRACE("mam_int", tout << "bind next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); \ + TRACE("mam_int", tout << "bind next candidate:\n" << mk_ll_pp(m_app->get_owner(), m);); \ m_oreg = m_b->m_oreg BBIND_COMMON(); @@ -2800,7 +2816,7 @@ namespace smt { m_pattern_instances.push_back(m_app); // continue succeeded update_max_generation(m_app, nullptr); // null indicates a top-level match - TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); + TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m);); m_num_args = c->m_num_args; m_oreg = c->m_oreg; for (unsigned i = 0; i < m_num_args; i++) @@ -2838,7 +2854,7 @@ namespace smt { // // ------------------------------------ class code_tree_map { - ast_manager & m_ast_manager; + ast_manager & m; compiler & m_compiler; ptr_vector m_trees; // mapping: func_label -> tree mam_trail_stack & m_trail_stack; @@ -2859,7 +2875,7 @@ namespace smt { public: code_tree_map(ast_manager & m, compiler & c, mam_trail_stack & s): - m_ast_manager(m), + m(m), m_compiler(c), m_trail_stack(s) { } @@ -2880,8 +2896,8 @@ namespace smt { - first_idx: index to be used as head of the multi-pattern mp */ void add_pattern(quantifier * qa, app * mp, unsigned first_idx) { - (void)m_ast_manager; - SASSERT(m_ast_manager.is_pattern(mp)); + (void)m; + SASSERT(m.is_pattern(mp)); SASSERT(first_idx < mp->get_num_args()); app * p = to_app(mp->get_arg(first_idx)); func_decl * lbl = p->get_decl(); @@ -3062,7 +3078,7 @@ namespace smt { // ------------------------------------ class mam_impl : public mam { protected: - ast_manager & m_ast_manager; + ast_manager & m; bool m_use_filters; mam_trail_stack m_trail_stack; label_hasher m_lbl_hasher; @@ -3130,7 +3146,7 @@ namespace smt { void add_candidate(code_tree * t, enode * app) { if (t != nullptr) { - TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_owner(), m_ast_manager);); + TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_owner(), m);); if (!t->has_candidates()) m_to_match.push_back(t); t->add_candidate(app); @@ -3188,7 +3204,7 @@ namespace smt { if (!r_plbls.may_contain(elem)) { m_trail_stack.push(mam_value_trail(r_plbls)); r_plbls.insert(elem); - TRACE("trigger_bug", tout << "updating plabels of:\n" << mk_ismt2_pp(c->get_root()->get_owner(), m_ast_manager) << "\n"; + TRACE("trigger_bug", tout << "updating plabels of:\n" << mk_ismt2_pp(c->get_root()->get_owner(), m) << "\n"; tout << "new_elem: " << static_cast(elem) << "\n"; tout << "plbls: " << c->get_root()->get_plbls() << "\n";); TRACE("mam_bug", tout << "updating plabels of: #" << c->get_root()->get_owner_id() << "\n"; @@ -3228,17 +3244,17 @@ namespace smt { } code_tree * mk_code(quantifier * qa, app * mp, unsigned pat_idx) { - SASSERT(m_ast_manager.is_pattern(mp)); + SASSERT(m.is_pattern(mp)); return m_compiler.mk_tree(qa, mp, pat_idx, true); } void insert_code(path_tree * t, quantifier * qa, app * mp, unsigned pat_idx) { - SASSERT(m_ast_manager.is_pattern(mp)); + SASSERT(m.is_pattern(mp)); m_compiler.insert(t->m_code, qa, mp, pat_idx, false); } path_tree * mk_path_tree(path * p, quantifier * qa, app * mp) { - SASSERT(m_ast_manager.is_pattern(mp)); + SASSERT(m.is_pattern(mp)); SASSERT(p != nullptr); unsigned pat_idx = p->m_pattern_idx; path_tree * head = nullptr; @@ -3259,7 +3275,7 @@ namespace smt { } void insert(path_tree * t, path * p, quantifier * qa, app * mp) { - SASSERT(m_ast_manager.is_pattern(mp)); + SASSERT(m.is_pattern(mp)); path_tree * head = t; path_tree * prev_sibling = nullptr; bool found_label = false; @@ -3442,7 +3458,7 @@ namespace smt { \brief Update inverted path index. */ void update_filters(quantifier * qa, app * mp) { - TRACE("mam_bug", tout << "updating filters using:\n" << mk_pp(mp, m_ast_manager) << "\n";); + TRACE("mam_bug", tout << "updating filters using:\n" << mk_pp(mp, m) << "\n";); unsigned num_vars = qa->get_num_decls(); if (num_vars >= m_var_paths.size()) m_var_paths.resize(num_vars+1); @@ -3499,6 +3515,7 @@ namespace smt { #ifdef _PROFILE_PATH_TREE t->m_watch.start(); #endif + m_todo.reset(); enode_vector * to_unmark = mk_tmp_vector(); enode_vector * to_unmark2 = mk_tmp_vector(); @@ -3576,7 +3593,7 @@ namespace smt { bool is_flat_assoc = lbl->is_flat_associative(); enode * curr_parent_root = curr_parent->get_root(); enode * curr_parent_cg = curr_parent->get_cg(); - TRACE("mam_path_tree", tout << "processing parent:\n" << mk_pp(curr_parent->get_owner(), m_ast_manager) << "\n";); + TRACE("mam_path_tree", tout << "processing parent:\n" << mk_pp(curr_parent->get_owner(), m) << "\n";); TRACE("mam_path_tree", tout << "parent is marked: " << curr_parent->is_marked() << "\n";); if (filter.may_contain(m_lbl_hasher(lbl)) && !curr_parent->is_marked() && @@ -3605,7 +3622,7 @@ namespace smt { is_eq(curr_tree->m_ground_arg, curr_parent->get_arg(curr_tree->m_ground_arg_idx)) )) { if (curr_tree->m_code) { - TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m_ast_manager) << "\n";); + TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m) << "\n";); add_candidate(curr_tree->m_code, curr_parent); } if (curr_tree->m_first_child) { @@ -3717,7 +3734,7 @@ namespace smt { } quantifier * qa = kv.first; app * mp = kv.second; - SASSERT(m_ast_manager.is_pattern(mp)); + SASSERT(m.is_pattern(mp)); app * p = to_app(mp->get_arg(0)); func_decl * lbl = p->get_decl(); if (m_context.get_num_enodes_of(lbl) > 0) { @@ -3754,7 +3771,7 @@ namespace smt { unsigned num_patterns = mp->get_num_args(); for (unsigned i = 0; i < num_patterns; i++) { app * pat = to_app(mp->get_arg(i)); - TRACE("mam_pat", tout << mk_ismt2_pp(qa, m_ast_manager) << "\npat:\n" << mk_ismt2_pp(pat, m_ast_manager) << "\n";); + TRACE("mam_pat", tout << mk_ismt2_pp(qa, m) << "\npat:\n" << mk_ismt2_pp(pat, m) << "\n";); SASSERT(!pat->is_ground()); todo.push_back(pat); } @@ -3780,13 +3797,13 @@ namespace smt { public: mam_impl(context & ctx, bool use_filters): mam(ctx), - m_ast_manager(ctx.get_manager()), + m(ctx.get_manager()), m_use_filters(use_filters), m_trail_stack(*this), m_ct_manager(m_lbl_hasher, m_trail_stack), m_compiler(ctx, m_ct_manager, m_lbl_hasher, use_filters), m_interpreter(ctx, *this, use_filters), - m_trees(m_ast_manager, m_compiler, m_trail_stack), + m_trees(m, m_compiler, m_trail_stack), m_region(m_trail_stack.get_region()), m_r1(nullptr), m_r2(nullptr) { @@ -3800,9 +3817,9 @@ namespace smt { } void add_pattern(quantifier * qa, app * mp) override { - SASSERT(m_ast_manager.is_pattern(mp)); - TRACE("trigger_bug", tout << "adding pattern\n" << mk_ismt2_pp(qa, m_ast_manager) << "\n" << mk_ismt2_pp(mp, m_ast_manager) << "\n";); - TRACE("mam_bug", tout << "adding pattern\n" << mk_pp(qa, m_ast_manager) << "\n" << mk_pp(mp, m_ast_manager) << "\n";); + SASSERT(m.is_pattern(mp)); + TRACE("trigger_bug", tout << "adding pattern\n" << mk_ismt2_pp(qa, m) << "\n" << mk_ismt2_pp(mp, m) << "\n";); + TRACE("mam_bug", tout << "adding pattern\n" << mk_pp(qa, m) << "\n" << mk_pp(mp, m) << "\n";); // Z3 checks if a pattern is ground or not before solving. // Ground patterns are discarded. // However, the simplifier may turn a non-ground pattern into a ground one. @@ -3900,14 +3917,14 @@ namespace smt { #endif void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector> & used_enodes) override { - TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";); + TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m) << "\n";); #ifdef Z3DEBUG if (m_check_missing_instances) { if (!m_context.slow_contains_instance(qa, num_bindings, bindings)) { TRACE("missing_instance", - tout << "qa:\n" << mk_ll_pp(qa, m_ast_manager) << "\npat:\n" << mk_ll_pp(pat, m_ast_manager); + tout << "qa:\n" << mk_ll_pp(qa, m) << "\npat:\n" << mk_ll_pp(pat, m); for (unsigned i = 0; i < num_bindings; i++) - tout << "#" << bindings[i]->get_owner_id() << "\n" << mk_ll_pp(bindings[i]->get_owner(), m_ast_manager) << "\n"; + tout << "#" << bindings[i]->get_owner_id() << "\n" << mk_ll_pp(bindings[i]->get_owner(), m) << "\n"; ); UNREACHABLE(); } @@ -3929,7 +3946,7 @@ namespace smt { // This method is invoked when n becomes relevant. // If lazy == true, then n is not added to the list of candidate enodes for matching. That is, the method just updates the lbls. void relevant_eh(enode * n, bool lazy) override { - TRACE("trigger_bug", tout << "relevant_eh:\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n"; + TRACE("trigger_bug", tout << "relevant_eh:\n" << mk_ismt2_pp(n->get_owner(), m) << "\n"; tout << "mam: " << this << "\n";); TRACE("mam", tout << "relevant_eh: #" << n->get_owner_id() << "\n";); if (n->has_lbl_hash()) @@ -3945,7 +3962,7 @@ namespace smt { update_lbls(n, h); if (is_plbl(lbl)) update_children_plbls(n, h); - TRACE("mam_bug", tout << "adding relevant candidate:\n" << mk_ll_pp(n->get_owner(), m_ast_manager) << "\n";); + TRACE("mam_bug", tout << "adding relevant candidate:\n" << mk_ll_pp(n->get_owner(), m) << "\n";); if (!lazy) add_candidate(n); }