diff --git a/src/sat/smt/q_clause.cpp b/src/sat/smt/q_clause.cpp index 097a61a14..d2b58bb2a 100644 --- a/src/sat/smt/q_clause.cpp +++ b/src/sat/smt/q_clause.cpp @@ -32,8 +32,8 @@ namespace q { << mk_bounded_pp(rhs, m, 2); } - std::ostream& binding::display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const { - for (unsigned i = 0; i < num_nodes; ++i) + std::ostream& binding::display(euf::solver& ctx, std::ostream& out) const { + for (unsigned i = 0; i < size(); ++i) out << ctx.bpp((*this)[i]) << " "; return out; } @@ -46,7 +46,7 @@ namespace q { if (!b) return out; do { - b->display(ctx, num_decls(), out) << "\n"; + b->display(ctx, out) << "\n"; b = b->next(); } while (b != m_bindings); diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 08a6f615a..0c89b2ade 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -79,7 +79,7 @@ namespace q { euf::enode* operator[](unsigned i) const { return m_nodes[i]; } - std::ostream& display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const; + std::ostream& display(euf::solver& ctx, std::ostream& out) const; unsigned size() const { return c->num_decls(); } diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 942c070fd..c0288e5cf 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -270,13 +270,14 @@ namespace q { } void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) { - TRACE("q", tout << "on-binding " << mk_pp(q, m) << "\n";); unsigned idx = m_q2clauses[q]; clause& c = *m_clauses[idx]; bool new_propagation = false; binding* b = alloc_binding(c, pat, _binding, max_generation, min_gen, max_gen); if (!b) return; + TRACE("q", b->display(ctx, tout << "on-binding " << mk_pp(q, m) << "\n") << "\n";); + if (false && propagate(false, _binding, max_generation, c, new_propagation)) return; @@ -558,7 +559,7 @@ namespace q { m_mam->propagate(); bool propagated = flush_prop_queue(); if (m_qhead >= m_clause_queue.size()) - return m_inst_queue.propagate(); + return m_inst_queue.propagate() || propagated; ctx.push(value_trail(m_qhead)); ptr_buffer to_remove; for (; m_qhead < m_clause_queue.size(); ++m_qhead) { @@ -613,8 +614,8 @@ namespace q { return true; for (unsigned i = 0; i < m_clauses.size(); ++i) if (m_clauses[i]->m_bindings) - std::cout << "missed propagation " << i << "\n"; - + IF_VERBOSE(0, verbose_stream() << "missed propagation " << i << "\n"); + TRACE("q", tout << "no more propagation\n";); return false; } diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 6581d271d..a968314c2 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -409,16 +409,17 @@ namespace q { unsigned m_num_args; //!< we need this information to avoid the nary *,+ crash bug bool m_filter_candidates; unsigned m_num_regs; - unsigned m_num_choices; - instruction * m_root; + unsigned m_num_choices = 0; + instruction * m_root = nullptr; enode_vector m_candidates; + unsigned m_qhead = 0; #ifdef Z3DEBUG - egraph * m_egraph; + egraph * m_egraph = nullptr; svector> m_patterns; #endif #ifdef _PROFILE_MAM stopwatch m_watch; - unsigned m_counter; + unsigned m_counter = 0; #endif friend class compiler; friend class code_tree_manager; @@ -492,13 +493,7 @@ namespace q { m_root_lbl(lbl), m_num_args(num_args), m_filter_candidates(filter_candidates), - m_num_regs(num_args + 1), - m_num_choices(0), - m_root(nullptr) { - DEBUG_CODE(m_egraph = nullptr;); -#ifdef _PROFILE_MAM - m_counter = 0; -#endif + m_num_regs(num_args + 1) { (void)m_lbl_hasher; } @@ -546,16 +541,40 @@ namespace q { return m_root; } - void add_candidate(enode * n) { + void add_candidate(euf::solver& ctx, enode * n) { m_candidates.push_back(n); + ctx.push(push_back_trail(m_candidates)); } + void unmark(unsigned head) { + for (unsigned i = m_candidates.size(); i-- > head; ) { + enode* app = m_candidates[i]; + if (app->is_marked1()) + app->unmark1(); + } + } + + struct scoped_unmark { + unsigned m_qhead; + code_tree* t; + scoped_unmark(code_tree* t) : m_qhead(t->m_qhead), t(t) {} + ~scoped_unmark() { t->unmark(m_qhead); } + }; + + bool has_candidates() const { - return !m_candidates.empty(); + return m_qhead < m_candidates.size(); } - void reset_candidates() { - m_candidates.reset(); + void save_qhead(euf::solver& ctx) { + ctx.push(value_trail(m_qhead)); + } + + enode* next_candidate() { + if (m_qhead < m_candidates.size()) + return m_candidates[m_qhead++]; + else + return nullptr; } enode_vector const & get_candidates() const { @@ -1987,24 +2006,18 @@ namespace q { m_backtrack_stack.resize(t->get_num_choices()); } - struct scoped_unmark { - code_tree* t; - scoped_unmark(code_tree* t) : t(t) {} - ~scoped_unmark() { - for (enode* app : t->get_candidates()) - if (app->is_marked1()) - app->unmark1(); - } - }; void execute(code_tree * t) { + if (!t->has_candidates()) + return; TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout);); init(t); + t->save_qhead(ctx); + enode* app; if (t->filter_candidates()) { - scoped_unmark _unmark(t); - for (unsigned i = 0; i < t->get_candidates().size() && !ctx.resource_limits_exceeded(); ++i) { - enode* app = t->get_candidates()[i]; - TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";); + code_tree::scoped_unmark _unmark(t); + while ((app = t->next_candidate()) && !ctx.resource_limits_exceeded()) { + TRACE("trigger_bug", tout << "candidate\n" << ctx.bpp(app) << "\n";); if (!app->is_marked1() && app->is_cgr()) { execute_core(t, app); app->mark1(); @@ -2012,9 +2025,8 @@ namespace q { } } else { - for (unsigned i = 0; i < t->get_candidates().size() && !ctx.resource_limits_exceeded(); ++i) { - enode* app = t->get_candidates()[i]; - TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";); + while ((app = t->next_candidate()) && !ctx.resource_limits_exceeded()) { + TRACE("trigger_bug", tout << "candidate\n" << ctx.bpp(app) << "\n";); if (app->is_cgr()) execute_core(t, app); } @@ -2477,17 +2489,18 @@ namespace q { case YIELD1: m_bindings[0] = m_registers[static_cast(m_pc)->m_bindings[0]]; -#define ON_MATCH(NUM) \ +#define ON_MATCH(NUM) \ m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \ - if (!m.inc()) { \ - return false; \ - } \ + if (!m.inc()) \ + return false; \ + \ m_mam.on_match(static_cast(m_pc)->m_qa, \ static_cast(m_pc)->m_pat, \ NUM, \ m_bindings.begin(), \ m_max_generation) + SASSERT(static_cast(m_pc)->m_qa->get_decl_sort(0) == m_bindings[0]->get_expr()->get_sort()); ON_MATCH(1); goto backtrack; @@ -3059,29 +3072,9 @@ namespace q { // temporary field used to collect candidates ptr_vector m_todo; - enode * m_root { nullptr }; // temp field - enode * m_other { nullptr }; // temp field - bool m_check_missing_instances { false }; - - class pop_to_match : public trail { - mam_impl& i; - public: - pop_to_match(mam_impl& i):i(i) {} - void undo() override { - code_tree* t = i.m_to_match.back(); - t->reset_candidates(); - i.m_to_match.pop_back(); - } - }; - - class reset_new_patterns : public trail { - mam_impl& i; - public: - reset_new_patterns(mam_impl& i):i(i) {} - void undo() override { - i.m_new_patterns.reset(); - } - }; + enode * m_root = nullptr; // temp field + enode * m_other = nullptr; // temp field + bool m_check_missing_instances = false; enode_vector * mk_tmp_vector() { enode_vector * r = m_pool.mk(); @@ -3094,14 +3087,14 @@ namespace q { } void add_candidate(code_tree * t, enode * app) { - if (t) { - TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_expr(), m);); - if (!t->has_candidates()) { - ctx.push(pop_to_match(*this)); - m_to_match.push_back(t); - } - t->add_candidate(app); + if (!t) + return; + TRACE("q", tout << "candidate " << t << " " << ctx.bpp(app) << "\n";); + if (!t->has_candidates()) { + ctx.push(push_back_trail(m_to_match)); + m_to_match.push_back(t); } + t->add_candidate(ctx, app); } void add_candidate(enode * app) { @@ -3678,14 +3671,20 @@ namespace q { } } - void match_new_patterns() { + unsigned m_new_patterns_qhead = 0; + + void propagate_new_patterns() { + if (m_new_patterns_qhead >= m_new_patterns.size()) + return; + ctx.push(value_trail(m_new_patterns_qhead)); + TRACE("mam_new_pat", tout << "matching new patterns:\n";); m_tmp_trees_to_delete.reset(); - for (auto const& kv : m_new_patterns) { + for (; m_new_patterns_qhead < m_new_patterns.size(); ++m_new_patterns_qhead) { if (!m.inc()) break; - quantifier * qa = kv.first; - app * mp = kv.second; + auto [qa, mp] = m_new_patterns[m_new_patterns_qhead]; + SASSERT(m.is_pattern(mp)); app * p = to_app(mp->get_arg(0)); func_decl * lbl = p->get_decl(); @@ -3717,7 +3716,6 @@ namespace q { m_tmp_trees[lbl_id] = nullptr; dealloc(tmp_tree); } - m_new_patterns.reset(); } public: @@ -3753,7 +3751,7 @@ namespace q { return; // ignore multi-pattern containing ground pattern. update_filters(qa, mp); m_new_patterns.push_back(qp_pair(qa, mp)); - ctx.push(reset_new_patterns(*this)); + ctx.push(push_back_trail(m_new_patterns)); // The matching abstract machine implements incremental // e-matching. So, for a multi-pattern [ p_1, ..., p_n ], // we have to make n insertions. In the i-th insertion, @@ -3764,7 +3762,6 @@ namespace q { void reset() override { m_trees.reset(); - m_new_patterns.reset(); m_is_plbl.reset(); m_is_clbl.reset(); reset_pp_pc(); @@ -3779,22 +3776,18 @@ namespace q { return out; } - void propagate() override { - TRACE("trigger_bug", tout << "match\n"; display(tout);); - if (m_to_match_head >= m_to_match.size()) + void propagate_to_match() { + if (m_to_match_head >= m_to_match.size()) return; ctx.push(value_trail(m_to_match_head)); - for (; m_to_match_head < m_to_match.size(); ++m_to_match_head) { - code_tree* t = m_to_match[m_to_match_head]; - if (t->has_candidates()) { - m_interpreter.execute(t); - t->reset_candidates(); - } - } - if (!m_new_patterns.empty()) { - match_new_patterns(); - m_new_patterns.reset(); - } + for (; m_to_match_head < m_to_match.size(); ++m_to_match_head) + m_interpreter.execute(m_to_match[m_to_match_head]); + } + + void propagate() override { + TRACE("trigger_bug", tout << "match\n"; display(tout);); + propagate_to_match(); + propagate_new_patterns(); } void rematch(bool use_irrelevant) override { diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp index c534c9f80..d74ee4e39 100644 --- a/src/sat/smt/q_queue.cpp +++ b/src/sat/smt/q_queue.cpp @@ -149,6 +149,12 @@ namespace q { if (false && em.propagate(true, f.nodes(), gen, *f.c, new_propagation)) return; +#if 0 + std::cout << mk_pp(q, m) << "\n"; + std::cout << num_bindings << "\n"; + for (unsigned i = 0; i < num_bindings; ++i) + std::cout << mk_pp(f[i]->get_expr(), m) << " " << mk_pp(f[i]->get_sort(), m) << "\n"; +#endif auto* ebindings = m_subst(q, num_bindings); for (unsigned i = 0; i < num_bindings; ++i) ebindings[i] = f[i]->get_expr(); @@ -161,6 +167,9 @@ namespace q { stat->inc_num_instances(); m_stats.m_num_instances++; + + // f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") << "\n"; + euf::solver::scoped_generation _sg(ctx, gen); sat::literal result_l = ctx.mk_literal(instance); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 69c773460..a5a42ee7a 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -676,7 +676,7 @@ namespace smt { 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_expr(), m) << "]"; + return out << n->get_owner_id() << ": " << mk_bounded_pp(n->get_expr(), m); } std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) {