From 03572a61f82590de059f22baac124d5f57e0474b Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Tue, 30 Jun 2026 16:17:02 -0700 Subject: [PATCH] Improve generation accounting (#10008) Details in original PR: https://github.com/Z3Prover/z3/pull/10007 --------- Co-authored-by: Can Cebeci --- src/smt/mam.cpp | 48 ++++-------- src/smt/smt_case_split_queue.cpp | 7 +- src/smt/smt_cg_table.cpp | 63 ++++++++++++---- src/smt/smt_cg_table.h | 48 ++++++++---- src/smt/smt_context.cpp | 121 +++++++++++++++++++++++++++---- src/smt/smt_context.h | 41 ++++++++++- src/smt/smt_enode.cpp | 46 ++++-------- src/smt/smt_enode.h | 27 +++---- src/smt/smt_internalizer.cpp | 80 ++++++++++++++++++-- src/smt/smt_model_checker.cpp | 2 +- src/smt/smt_model_finder.cpp | 12 +-- src/smt/smt_quantifier.cpp | 11 +-- src/smt/smt_quick_checker.cpp | 4 +- src/util/chashtable.h | 2 +- 14 files changed, 365 insertions(+), 147 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 80918fcb45..f8ea774cbb 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -215,7 +215,6 @@ namespace { unsigned short m_num_args; unsigned m_ireg; unsigned m_oreg; - unsigned m_curr_max_generation = 0; }; struct get_cgr : public instruction { @@ -1881,47 +1880,33 @@ namespace { m_pool.recycle(v); } - void update_max_generation(enode * n, enode * prev, enode * min_gen_match=nullptr) { - unsigned new_gen = min_gen_match ? min_gen_match->get_generation() : n->get_generation(); - - m_max_generation = std::max(m_max_generation, new_gen); + void update_max_generation(enode * n, enode * prev) { + m_max_generation = std::max(m_max_generation, m_context.get_generation(n)); if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) m_used_enodes.push_back(std::make_tuple(prev, n)); } - void get_f_app(func_decl* lbl, unsigned num_expected_args, enode* curr, enode*& matching_cgr, enode*& min_gen_match) { - if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args) { - if (curr->is_cgr() && !matching_cgr) - matching_cgr = curr; - - if (!min_gen_match || min_gen_match->get_generation() > curr->get_generation()) { - min_gen_match = curr; - } - } - } - // We have to provide the number of expected arguments because we have flat-assoc applications such as +. // Flat-assoc applications may have arbitrary number of arguments. enode * get_first_f_app(func_decl * lbl, unsigned num_expected_args, enode * curr) { enode * first = curr; - enode *matching_cgr = nullptr, *min_gen_match = nullptr; do { - get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match); + if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) { + update_max_generation(curr, first); + return curr; + } curr = curr->get_next(); } while (curr != first); - if (matching_cgr) - update_max_generation(matching_cgr, first, min_gen_match); - return matching_cgr; + return nullptr; } enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) { curr = curr->get_next(); while (curr != first) { - if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr()) { - if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) - m_used_enodes.push_back(std::make_tuple(first, curr)); + if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) { + update_max_generation(curr, first); return curr; } curr = curr->get_next(); @@ -2065,7 +2050,7 @@ namespace { void get_min_max_top_generation(unsigned& min, unsigned& max) { SASSERT(!m_pattern_instances.empty()); if (m_min_top_generation.empty()) { - min = max = m_pattern_instances[0]->get_generation(); + min = max = m_context.get_generation(m_pattern_instances[0]); m_min_top_generation.push_back(min); m_max_top_generation.push_back(max); } @@ -2074,7 +2059,7 @@ namespace { max = m_max_top_generation.back(); } for (unsigned i = m_min_top_generation.size(); i < m_pattern_instances.size(); ++i) { - unsigned curr = m_pattern_instances[i]->get_generation(); + unsigned curr = m_context.get_generation(m_pattern_instances[i]); min = std::min(min, curr); m_min_top_generation.push_back(min); max = std::max(max, curr); @@ -2315,7 +2300,8 @@ namespace { m_min_top_generation.reset(); m_max_top_generation.reset(); m_pattern_instances.push_back(n); - m_max_generation = n->get_generation(); + + m_max_generation = m_context.get_generation(n); if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) { m_used_enodes.reset(); @@ -2492,7 +2478,6 @@ namespace { 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; \ m_backtrack_stack[m_top].m_curr = m_app; \ - const_cast(static_cast(m_pc))->m_curr_max_generation = m_max_generation; \ m_top++; BIND_COMMON(); @@ -2556,7 +2541,7 @@ namespace { case YIELD1: m_bindings[0] = m_registers[static_cast(m_pc)->m_bindings[0]]; #define ON_MATCH(NUM) \ - m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \ + m_max_generation = std::max(m_max_generation, get_max_generation(m_context, NUM, m_bindings.begin())); \ if (m_context.get_cancel_flag()) { \ return false; \ } \ @@ -2760,7 +2745,6 @@ namespace { #define BBIND_COMMON() m_b = static_cast(bp.m_instr); \ m_n1 = m_registers[m_b->m_ireg]; \ m_app = get_next_f_app(m_b->m_label, m_b->m_num_args, m_n1, bp.m_curr); \ - m_max_generation = m_b->m_curr_max_generation; \ if (!m_app) { \ m_top--; \ goto backtrack; \ @@ -3972,10 +3956,6 @@ namespace { } return; } - DEBUG_CODE( - for (unsigned i = 0; i < num_bindings; ++i) { - SASSERT(bindings[i]->get_generation() <= max_generation); - }); #endif unsigned min_gen = 0, max_gen = 0; diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 029758b85d..e0632b41a8 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -1012,7 +1012,7 @@ namespace { stack.pop_back(); if (m_context.e_internalized(curr)) { - gen = m_context.get_enode(curr)->get_generation(); + gen = m_context.get_generation(m_context.get_enode(curr)); if (gen > maxgen) maxgen = gen; if (gen < mingen) @@ -1046,7 +1046,7 @@ namespace { void operator()(expr * e) { if (m_context.e_internalized(e)) { enode * n = m_context.get_enode(e); - n->set_generation(&m_context, m_generation); + m_context.set_generation(n, m_generation); } } }; @@ -1069,7 +1069,8 @@ namespace { stack.pop_back(); if (m_context.e_internalized(curr)) { - unsigned curr_gen = m_context.get_enode(curr)->get_generation(); + enode * n = m_context.get_enode(curr); + unsigned curr_gen = m_context.get_generation(n); if (curr_gen > gen) { // Lower it. set_generation_rec(e, gen); diff --git a/src/smt/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp index 018a543c0b..d8f287462c 100644 --- a/src/smt/smt_cg_table.cpp +++ b/src/smt/smt_cg_table.cpp @@ -170,7 +170,7 @@ namespace smt { void cg_table::display_binary(std::ostream& out, void* t) const { binary_table* tb = UNTAG(binary_table*, t); out << "b "; - for (enode* n : *tb) { + for (auto const& [n, v] : *tb) { out << n->get_owner_id() << " " << cg_binary_hash()(n) << " "; } out << "\n"; @@ -179,7 +179,7 @@ namespace smt { void cg_table::display_binary_comm(std::ostream& out, void* t) const { comm_table* tb = UNTAG(comm_table*, t); out << "bc "; - for (enode* n : *tb) { + for (auto const& [n, v] : *tb) { out << n->get_owner_id() << " "; } out << "\n"; @@ -188,7 +188,7 @@ namespace smt { void cg_table::display_unary(std::ostream& out, void* t) const { unary_table* tb = UNTAG(unary_table*, t); out << "un "; - for (enode* n : *tb) { + for (auto const& [n, v] : *tb) { out << n->get_owner_id() << " "; } out << "\n"; @@ -197,36 +197,73 @@ namespace smt { void cg_table::display_nary(std::ostream& out, void* t) const { table* tb = UNTAG(table*, t); out << "nary "; - for (enode* n : *tb) { + for (auto const& [n, v] : *tb) { out << n->get_owner_id() << " "; } out << "\n"; } - enode_bool_pair cg_table::insert(enode * n) { + enode_bool_gen_ptr cg_table::insert(enode * n, unsigned generation) { // it doesn't make sense to insert a constant. SASSERT(n->get_num_args() > 0); SASSERT(!m_manager.is_and(n->get_expr())); SASSERT(!m_manager.is_or(n->get_expr())); enode * n_prime; + unsigned* payload = nullptr; void * t = get_table(n); switch (static_cast(GET_TAG(t))) { case UNARY: - n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); - return enode_bool_pair(n_prime, false); + if (auto* e = UNTAG(unary_table*, t)->find_core(n)) { + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + } + else { + e = UNTAG(unary_table*, t)->insert_if_not_there3(n, generation); + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + (*payload) = generation; + } + return enode_bool_gen_ptr(n_prime, false, payload); case BINARY: - n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); + if (auto* e = UNTAG(binary_table*, t)->find_core(n)) { + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + } + else { + e = UNTAG(binary_table*, t)->insert_if_not_there3(n, generation); + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + (*payload) = generation; + } TRACE(cg_table, tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n"; display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); - return enode_bool_pair(n_prime, false); + return enode_bool_gen_ptr(n_prime, false, payload); case BINARY_COMM: m_commutativity = false; - n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); - return enode_bool_pair(n_prime, m_commutativity); + if (auto* e = UNTAG(comm_table*, t)->find_core(n)) { + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + } + else { + e = UNTAG(comm_table*, t)->insert_if_not_there3(n, generation); + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + (*payload) = generation; + } + return enode_bool_gen_ptr(n_prime, m_commutativity, payload); default: - n_prime = UNTAG(table*, t)->insert_if_not_there(n); - return enode_bool_pair(n_prime, false); + if (auto* e = UNTAG(table*, t)->find_core(n)) { + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + } + else { + e = UNTAG(table*, t)->insert_if_not_there3(n, generation); + n_prime = e->get_data().m_key; + payload = &e->get_data().m_value; + (*payload) = generation; + } + return enode_bool_gen_ptr(n_prime, false, payload); } } diff --git a/src/smt/smt_cg_table.h b/src/smt/smt_cg_table.h index 9c2baed11e..78cd3a199b 100644 --- a/src/smt/smt_cg_table.h +++ b/src/smt/smt_cg_table.h @@ -21,10 +21,14 @@ Revision History: #include "smt/smt_enode.h" #include "util/hashtable.h" #include "util/chashtable.h" +#include "util/map.h" namespace smt { typedef std::pair enode_bool_pair; + typedef std::tuple enode_bool_gen_ptr; + typedef std::pair enode_gen_ptr; + typedef std::pair enode_pair; // one table per function symbol @@ -48,7 +52,7 @@ namespace smt { } }; - typedef chashtable unary_table; + typedef map unary_table; struct cg_binary_hash { unsigned operator()(enode * n) const { @@ -68,7 +72,7 @@ namespace smt { } }; - typedef chashtable binary_table; + typedef map binary_table; struct cg_comm_hash { unsigned operator()(enode * n) const { @@ -103,7 +107,7 @@ namespace smt { } }; - typedef chashtable comm_table; + typedef map comm_table; struct cg_hash { unsigned operator()(enode * n) const; @@ -113,7 +117,7 @@ namespace smt { bool operator()(enode * n1, enode * n2) const; }; - typedef chashtable table; + typedef map table; ast_manager & m_manager; bool m_commutativity; //!< true if the last found congruence used commutativity @@ -148,7 +152,7 @@ namespace smt { return n' and a boolean indicating whether n and n' are congruence modulo commutativity, otherwise insert n and return (n,false). */ - enode_bool_pair insert(enode * n); + enode_bool_gen_ptr insert(enode * n, unsigned generation); void erase(enode * n); @@ -167,35 +171,47 @@ namespace smt { } } - enode * find(enode * n) const { + enode_gen_ptr find_gen(enode * n) const { SASSERT(n->get_num_args() > 0); - enode * r = nullptr; void * t = const_cast(this)->get_table(n); + unary_table::entry* e = nullptr; switch (static_cast(GET_TAG(t))) { case UNARY: - return UNTAG(unary_table*, t)->find(n, r) ? r : nullptr; + e = UNTAG(unary_table*, t)->find_core(n); + return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); case BINARY: - return UNTAG(binary_table*, t)->find(n, r) ? r : nullptr; + e = UNTAG(binary_table*, t)->find_core(n); + return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); case BINARY_COMM: - return UNTAG(comm_table*, t)->find(n, r) ? r : nullptr; + e = UNTAG(comm_table*, t)->find_core(n); + return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); default: - return UNTAG(table*, t)->find(n, r) ? r : nullptr; + e = UNTAG(table*, t)->find_core(n); + return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); } } + enode * find(enode * n) const { + return find_gen(n).first; + } + bool contains_ptr(enode * n) const { - enode * r; SASSERT(n->get_num_args() > 0); void * t = const_cast(this)->get_table(n); + unary_table::entry* e = nullptr; switch (static_cast(GET_TAG(t))) { case UNARY: - return UNTAG(unary_table*, t)->find(n, r) && n == r; + e = UNTAG(unary_table*, t)->find_core(n); + return e && n == e->get_data().m_key; case BINARY: - return UNTAG(binary_table*, t)->find(n, r) && n == r; + e = UNTAG(binary_table*, t)->find_core(n); + return e && n == e->get_data().m_key; case BINARY_COMM: - return UNTAG(comm_table*, t)->find(n, r) && n == r; + e = UNTAG(comm_table*, t)->find_core(n); + return e && n == e->get_data().m_key; default: - return UNTAG(table*, t)->find(n, r) && n == r; + e = UNTAG(table*, t)->find_core(n); + return e && n == e->get_data().m_key; } } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0e8062e880..66c03c7991 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -537,7 +537,8 @@ namespace smt { mark_as_relevant(r1); } - push_trail(add_eq_trail(*this, r1, n1, r2->get_num_parents())); + + unsigned r2_num_parents = r2->get_num_parents(); m_qmanager->add_eq_eh(r1, r2); @@ -568,6 +569,8 @@ namespace smt { SASSERT(r1->get_root() == r2); reinsert_parents_into_cg_table(r1, r2, n1, n2, js); + push_trail(add_eq_trail(*this, r1, n1, r2_num_parents)); + if (n2->is_bool()) propagate_bool_enode_assignment(r1, r2, n1, n2); @@ -594,6 +597,8 @@ namespace smt { must be removed from the congruence table since their hash code will change. */ void context::remove_parents_from_cg_table(enode * r1) { + SASSERT(m_r1_parent_generations.empty()); + // Remove parents from the congruence table for (enode * parent : enode::parents(r1)) { CTRACE(add_eq, !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";); @@ -603,7 +608,8 @@ namespace smt { tout << "\n"; tout << "contains: " << m_cg_table.contains(parent) << "\n"; if (m_cg_table.contains(parent)) { - tout << "owner: " << m_cg_table.find(parent)->get_owner_id() << "\n"; + enode* owner = m_cg_table.find(parent); + tout << "owner: " << owner->get_owner_id() << "\n"; } m_cg_table.display(tout); ); @@ -614,6 +620,7 @@ namespace smt { SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent)); parent->set_mark(); if (parent->is_cgc_enabled()) { + m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent))); m_cg_table.erase(parent); SASSERT(!m_cg_table.contains_ptr(parent)); } @@ -621,6 +628,21 @@ namespace smt { } } + // Sticky update to the generation number of the congruence class + // Goes out of scope when n is garbage collected. + void context::set_generation_sticky(enode * n, unsigned generation) { + SASSERT(n->uses_cg_table()); + auto [cgr, cgc_gen] = m_cg_table.find_gen(n); + SASSERT(cgr); + SASSERT(cgc_gen); + // Callers are responsible for this. Sticky updates are too expensive to accommodate no-ops. + SASSERT(generation < *cgc_gen); + + *cgc_gen = generation; + m_sticky_generation_updates.insert(n, generation); + } + + /** \brief Reinsert the parents of r1 that were removed from the cg_table at remove_parents_from_cg_table. Some of these parents will @@ -638,6 +660,7 @@ namespace smt { enode_vector & r2_parents = r2->m_parents; enode_vector & r1_parents = r1->m_parents; unsigned num_r1_parents = r1_parents.size(); + unsigned cgc_enabled_idx = 0; for (unsigned i = 0; i < num_r1_parents; ++i) { enode* parent = r1_parents[i]; if (!parent->is_marked()) @@ -658,26 +681,40 @@ namespace smt { m_dyn_ack_manager.cg_conflict_eh(n1->get_app(), n2->get_app()); assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs))); } + if (parent->is_cgc_enabled()) { + auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++]; + SASSERT(p == parent); + m_constant_generations.insert(parent, parent_generation); + } // It is not necessary to reinsert the equality to the congruence table + // (because the only congruence propagations that could lead to are already handled by the assign() here). + continue; } } if (parent->is_cgc_enabled()) { - auto [parent_prime, used_commutativity] = m_cg_table.insert(parent); + auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++]; + SASSERT(p == parent); + auto [parent_prime, used_commutativity, gen_ptr] = m_cg_table.insert(parent, parent_generation); if (parent_prime == parent) { SASSERT(parent); - SASSERT(parent->is_cgr()); + SASSERT(parent->is_cgr()); SASSERT(m_cg_table.contains_ptr(parent)); + SASSERT(*gen_ptr == parent_generation); + r2_parents.push_back(parent); continue; } + parent->m_cg = parent_prime; - SASSERT(!m_cg_table.contains_ptr(parent)); + merge_cgc_generations(parent, parent_generation, parent_prime, gen_ptr); + if (parent_prime->m_root != parent->m_root) { TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id() << " used_commutativity: " << used_commutativity << "\n";); push_new_congruence(parent, parent_prime, used_commutativity); } + } else { // If congruence closure is not enabled for parent, then I just copy it @@ -685,6 +722,7 @@ namespace smt { r2_parents.push_back(parent); } } + m_r1_parent_generations.reset(); } /** @@ -940,6 +978,8 @@ namespace smt { // unmerge "equivalence" classes std::swap(r1->m_next, r2->m_next); + SASSERT(m_r1_parent_generations.empty()); + // remove the parents of r1 that remained as congruence roots enode_vector::iterator it = r2->begin_parents(); enode_vector::iterator end = r2->end_parents(); @@ -956,6 +996,8 @@ namespace smt { display(tout << "\n");); SASSERT(parent->is_cgr()); SASSERT(m_cg_table.contains_ptr(parent)); + if (!parent->is_eq()) + m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent))); m_cg_table.erase(parent); } } @@ -970,22 +1012,50 @@ namespace smt { // restore parents of r2 r2->m_parents.shrink(r2_num_parents); + unsigned cgr_parent_idx = 0; + // try to reinsert parents of r1 that are not cgr for (enode * parent : enode::parents(r1)) { TRACE(add_eq_parents, tout << "visiting: #" << parent->get_owner_id() << "\n";); if (parent->is_cgc_enabled()) { - enode * cg = parent->m_cg; if (!parent->is_true_eq() && - (parent == cg || // parent was root of the congruence class before and after the merge - !congruent(parent, cg) // parent was root of the congruence class before but not after the merge - )) { - auto [parent_cg, used_commutativity] = m_cg_table.insert(parent); + (parent == cg || // parent was root of the congruence class before and after the merge + !congruent(parent, cg)) // parent was root of the congruence class before but not after the merge + ) { + + unsigned gen; + if (parent->is_eq()) { + gen = 0; + } else if (parent == cg) { + enode *p = nullptr; + unsigned parent_generation; + if (cgr_parent_idx < m_r1_parent_generations.size()) { + std::tie(p, parent_generation) = m_r1_parent_generations[cgr_parent_idx]; + } + if (p == parent) { + cgr_parent_idx++; + gen = parent_generation; + } else { + SASSERT(m_cg_table.contains_ptr(parent)); + continue; + } + } else { + // Insert at some dummy generation here. An undo_merge_cgr will immediately follow to set the generation. + unsigned dummy_generation = 100000; // NOT UINT_MAX. In case this goes badly overflows would be hell to debug. + gen = dummy_generation; + } + + auto [parent_cg, used_commutativity, gen_ptr] = m_cg_table.insert(parent, gen); + (void)used_commutativity; + (void)gen_ptr; parent->m_cg = parent_cg; } } } + m_r1_parent_generations.reset(); + // restore theory vars if (r2->m_th_var_list.get_next() == nullptr) { // common case: r2 has at most one variable @@ -1020,6 +1090,30 @@ namespace smt { CASSERT("add_eq", check_invariant()); } + void context::undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) { + // TODO: optimization: don't bother unrolling e1 if e1 is an enode about to be garbage collected. + set_generation(e1, e1_generation); + set_generation(e2, e2_generation); + + apply_sticky_updates(e1, e1_generation, e2, e2_generation); + } + + void context::apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) { + SASSERT(e1->uses_cg_table()); + SASSERT(e2->uses_cg_table()); + // optimization opportunity: we actually just need to look at updates above the current decision level. + // Then we wouldn't have to check for minimum either. + for (auto const& [t, generation] : m_sticky_generation_updates) { + // SASSERT(t->uses_cg_table()); // may not hold if t is an equality that became true at some point after the generation update. + + if (generation < e1_generation && congruent(t, e1)) { + set_generation(e1, generation); + } else if (generation < e2_generation && congruent(t, e2)) { + set_generation(e2, generation); + } + } + } + /** \brief Auxiliary method for undo_add_eq. It restores the theory variables of a given root enode. @@ -1283,7 +1377,7 @@ namespace smt { */ enode * context::get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) { enode * tmp = m_tmp_enode.set(f, num_args, args); - enode * r = m_cg_table.find(tmp); + enode * r = m_cg_table.find(tmp); #ifdef Z3DEBUG if (r != nullptr) { SASSERT(r->get_decl() == f); @@ -2246,8 +2340,9 @@ namespace smt { unsigned ilvl = e->get_iscope_lvl(); if (ilvl <= new_scope_lvl) continue; // node and its children will not be recreated during backtracking - TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";); - m_cached_generation.insert(n, e->get_generation()); + unsigned generation = get_generation(e); + TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << generation << "\n";); + m_cached_generation.insert(n, generation); } for (expr * arg : *to_app(n)) { if (is_app(arg) || is_quantifier(arg)) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index f11b54aeb1..31e7722102 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -46,6 +46,7 @@ Revision History: #include "util/ref.h" #include "util/timer.h" #include "util/statistics.h" +#include "util/map.h" #include "smt/fingerprints.h" #include "smt/proto_model/proto_model.h" #include "smt/theory_user_propagator.h" @@ -66,6 +67,9 @@ namespace smt { class context; class kernel; + // Hash table for storing enode -> generation mappings + typedef ptr_addr_map enode_generation_table; + struct oom_exception : public z3_error { oom_exception() : z3_error(ERR_MEMOUT) {} }; @@ -156,6 +160,9 @@ namespace smt { vector m_decl2enodes; // decl -> enode (for decls with arity > 0) enode_vector m_empty_vector; cg_table m_cg_table; + enode_generation_table m_sticky_generation_updates; + enode_generation_table m_constant_generations; // generations for enodes with !e->uses_cg_table() + vector> m_r1_parent_generations; // generations of parents removed from m_cg_table while merging r1 struct new_eq { enode * m_lhs; @@ -615,6 +622,21 @@ namespace smt { return m_qmanager->get_generation(q); } + unsigned get_generation(enode * e) const { + // We don't support patterns with equality so there is no need to track generations for them. + if (e->is_eq()) + return 0; + + if (!e->uses_cg_table()) + return m_constant_generations.find(e); + + auto [cgr, generation] = m_cg_table.find_gen(e); + SASSERT(cgr); + return *generation; + } + + void set_generation(enode * e, unsigned generation); + /** \brief Return true if the logical context internalized universal quantifiers. */ @@ -1131,12 +1153,16 @@ namespace smt { void push_new_th_diseq(theory_id th, theory_var lhs, theory_var rhs); friend class add_eq_trail; - + friend class merge_cgc_generations_trail; void remove_parents_from_cg_table(enode * r1); void reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js); + void merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned *e2_generation_ptr); + + void set_generation_sticky(enode * e, unsigned generation); + void invert_trans(enode * n); theory_var get_closest_var(enode * n, theory_id th_id); @@ -1147,6 +1173,10 @@ namespace smt { void propagate_bool_enode_assignment_core(enode * source, enode * target); + void undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation); + + void apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation); + void undo_add_eq(enode * r1, enode * n1, unsigned r2_num_parents); void restore_theory_vars(enode * r2, enode * r1); @@ -1193,6 +1223,15 @@ namespace smt { static bool is_eq(enode const * n1, enode const * n2) { return n1->get_root() == n2->get_root(); } + enode * get_cg_root(enode * n) const { + SASSERT(n->get_num_args() > 0); + if (!n->uses_cg_table()) + return n->get_cg(); + auto r = m_cg_table.find(n); + SASSERT(r != nullptr); + return r; + } + bool is_diseq(enode * n1, enode * n2) const; bool is_diseq_slow(enode * n1, enode * n2) const; diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 05b174e5e0..e5dd01d24e 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -21,12 +21,12 @@ Revision History: #include "smt/smt_enode.h" namespace smt { - + /** \brief Initialize an enode in the given memory position. */ - enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, - unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, + enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, + bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); enode * n = new (mem) enode(); @@ -35,7 +35,6 @@ namespace smt { n->m_next = n; n->m_cg = nullptr; n->m_class_size = 1; - n->m_generation = generation; n->m_func_decl_id = UINT_MAX; n->m_mark = false; n->m_mark2 = false; @@ -64,19 +63,19 @@ namespace smt { return n; } - enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, - unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, + enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, + bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); unsigned sz = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args()); void * mem = r.allocate(sz); - return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent); + return init(m, mem, app2enode, owner, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent); } enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) { unsigned sz = get_enode_size(owner->get_num_args()); void * mem = alloc_svect(char, sz); - return init(m, mem, app2enode, owner, 0, false, false, 0, true, false); + return init(m, mem, app2enode, owner, false, false, 0, true, false); } void enode::del_eh(ast_manager & m, bool update_children_parent) { @@ -131,20 +130,6 @@ namespace smt { m_th_var_list.del_var(id); } - - /** - \brief Push old value of generation on the context trail stack - and update the generation. - */ - void enode::set_generation(context * ctx, unsigned generation) { - if (m_generation == generation) - return; - if (ctx) - ctx->push_trail(value_trail(m_generation)); - m_generation = generation; - } - - void enode::set_lbl_hash(context & ctx) { SASSERT(m_lbl_hash == -1); // m_lbl_hash should be different from -1, if and only if, @@ -161,16 +146,17 @@ namespace smt { } } - enode * enode::get_eq_enode_with_min_gen() { - if (m_generation == 0) - return this; + enode * enode::get_eq_enode_with_min_gen(context * ctx) { enode * r = this; enode * curr = this; + unsigned r_gen = ctx->get_generation(r); do { - if (curr->m_generation < r->m_generation) { + unsigned curr_gen = ctx->get_generation(curr); + if (curr_gen == 0) + return curr; + if (curr_gen < r_gen) { r = curr; - if (r->m_generation == 0) - return r; + r_gen = curr_gen; } curr = curr->m_next; } @@ -307,10 +293,10 @@ namespace smt { } } - unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) { + unsigned get_max_generation(context & ctx, unsigned num_enodes, enode * const * enodes) { unsigned max = 0; for (unsigned i = 0; i < num_enodes; ++i) { - unsigned curr = enodes[i]->get_generation(); + unsigned curr = ctx.get_generation(enodes[i]); if (curr > max) max = curr; } diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index e9dc4c4e13..84da1756ad 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -64,7 +64,6 @@ namespace smt { enode * m_next; //!< Next element in the equivalence class. enode * m_cg; unsigned m_class_size; //!< Size of the equivalence class if the enode is the root. - unsigned m_generation; //!< Tracks how many quantifier instantiation rounds were needed to generate this enode. unsigned m_func_decl_id; //!< Id generated by the congruence table for fast indexing. @@ -102,7 +101,7 @@ namespace smt { approx_set m_lbls; approx_set m_plbls; enode * m_args[0]; //!< Cached args - + friend class context; friend class conflict_resolution; friend class quantifier_manager; @@ -132,8 +131,8 @@ namespace smt { friend class tmp_enode; - static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, - unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, + static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, + bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); public: @@ -141,9 +140,9 @@ namespace smt { return sizeof(enode) + num_args * sizeof(enode*); } - static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, - unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, - bool cgc_enabled, bool update_children_parent); + static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, + bool suppress_args, bool merge_tf, unsigned iscope_lvl, + bool cgc_enabled, bool update_children_parent); static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner); @@ -314,6 +313,10 @@ namespace smt { return m_cg; } + bool uses_cg_table() const { + return get_num_args() > 0 && is_cgc_enabled() && !is_true_eq(); + } + bool is_cgc_enabled() const { return m_cgc_enabled; } @@ -393,18 +396,12 @@ namespace smt { trans_justification get_trans_justification() { return m_trans; } - - unsigned get_generation() const { - return m_generation; - } - - void set_generation(context * ctx, unsigned generation); /** \brief Return the enode n that is in the eqc of *this, and has the minimal generation. That is, there is no other enode with smaller generation. */ - enode * get_eq_enode_with_min_gen(); + enode * get_eq_enode_with_min_gen(context * ctx); unsigned get_iscope_lvl() const { return m_iscope_lvl; @@ -460,7 +457,7 @@ namespace smt { return congruent(n1, n2, aux); } - unsigned get_max_generation(unsigned num_enodes, enode * const * enodes); + unsigned get_max_generation(context & ctx, unsigned num_enodes, enode * const * enodes); void unmark_enodes(unsigned num_enodes, enode * const * enodes); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 3bb498882a..c4afaf43f5 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -102,8 +102,66 @@ namespace smt { } void context::update_generation(enode * e) { - if (0 < m_generation && m_generation < e->get_generation()) - e->set_generation(nullptr, m_generation); + // We don't support patterns with equality so there is no need to track generations for them. + if (e->is_eq()) + return; + + enode *cgr = e->get_num_args() == 0 ? e : get_cg_root(e); + if (0 < m_generation && m_generation < get_generation(cgr)) { + if (e->uses_cg_table()) + set_generation_sticky(e, m_generation); + else + m_constant_generations[e] = m_generation; // Sticky by default. Won't unmerge + } + } + + void context::set_generation(enode * e, unsigned generation) { + // We don't support patterns with equality so there is no need to track generations for them. + if (e->is_eq()) + return; + + if (e->uses_cg_table()) { + auto [cgr, cgc_gen] = m_cg_table.find_gen(e); + SASSERT(cgc_gen); + *cgc_gen = generation; + } else { + m_constant_generations[e] = generation; + } + } + + class merge_cgc_generations_trail : public trail { + context& ctx; + enode* m_e1; + unsigned m_e1_generation; + enode* m_e2; + unsigned m_e2_generation; + public: + merge_cgc_generations_trail(context& ctx, enode* e1, unsigned e1_generation, enode* e2, unsigned e2_generation): + ctx(ctx), + m_e1(e1), + m_e1_generation(e1_generation), + m_e2(e2), + m_e2_generation(e2_generation) { + } + + void undo() override { + ctx.undo_merge_cgc_generations(m_e1, m_e1_generation, m_e2, m_e2_generation); + } + }; + + void context::merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned *e2_generation_ptr) { + // We assume the congruence has already been updated. We might want to move that here, too. + SASSERT(e2->is_cgr()); + SASSERT(!m_cg_table.contains_ptr(e1)); + SASSERT(m_cg_table.contains_ptr(e2)); + + // Push trail even if we have a no-op. Otherwise we can't restore e1's generation after unmerging. + push_trail(merge_cgc_generations_trail(*this, e1, e1_generation, e2, *e2_generation_ptr)); + + if (e1_generation >= *e2_generation_ptr) + return; // no-op + + *e2_generation_ptr = e1_generation; } void context::ts_visit_child(expr * n, bool gate_ctx, svector & todo, bool & visited) { @@ -1002,7 +1060,7 @@ namespace smt { CTRACE(cached_generation, generation != m_generation, tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";); } - enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, + enode *e = enode::mk(m, get_region(), m_app2enode, to_app(n), suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true); TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";); if (m.is_unique_value(n)) @@ -1022,8 +1080,11 @@ namespace smt { } else { if (cgc_enabled) { - auto [e_prime, used_commutativity] = m_cg_table.insert(e); + auto [e_prime, used_commutativity, sibling_gen_ptr] = m_cg_table.insert(e, generation); if (e != e_prime) { + // We don't support patterns with equality so there is no need to track generations for them. + if (!e->is_eq()) + merge_cgc_generations(e, generation, e_prime, sibling_gen_ptr); e->m_cg = e_prime; push_new_congruence(e, e_prime, used_commutativity); } @@ -1032,6 +1093,8 @@ namespace smt { } } else { + SASSERT(!e->uses_cg_table()); + m_constant_generations.insert(e, generation); e->m_cg = e; } } @@ -1041,7 +1104,10 @@ namespace smt { m_decl2enodes.resize(decl_id+1); m_decl2enodes[decl_id].push_back(e); } + } else { + m_constant_generations.insert(e, generation); } + SASSERT(e_internalized(n)); m_stats.m_num_mk_enode++; TRACE(mk_enode, tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m) << "\n"; @@ -1066,10 +1132,11 @@ namespace smt { unsigned n_id = n->get_id(); enode * e = m_app2enode[n_id]; m_app2enode[n_id] = nullptr; - if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) { + if (e->is_cgr() && e->uses_cg_table()) { SASSERT(m_cg_table.contains_ptr(e)); m_cg_table.erase(e); } + SASSERT(!(e->get_num_args() > 0 && m_cg_table.contains_ptr(e))); if (e->get_num_args() > 0 && !e->is_eq()) { unsigned decl_id = e->get_decl_id(); SASSERT(decl_id < m_decl2enodes.size()); @@ -1080,6 +1147,9 @@ namespace smt { SASSERT(m_e_internalized_stack.size() == m_enodes.size()); m_enodes.pop_back(); m_e_internalized_stack.pop_back(); + m_sticky_generation_updates.erase(e); + if (!e->uses_cg_table()) + m_constant_generations.erase(e); } /** diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index c6c914fe03..feccd7149e 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -109,7 +109,7 @@ namespace smt { for (auto const& kv : *m_root2value) { enode * n = kv.m_key; expr * val = kv.m_value; - n = n->get_eq_enode_with_min_gen(); + n = n->get_eq_enode_with_min_gen(m_context); expr* e = n->get_expr(); if (!m.is_value(e)) m_value2expr.insert(val, e); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 4ba66a51be..4b461a59a1 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1235,7 +1235,7 @@ namespace smt { // a necessary instantiation. enode* e_arg = n->get_arg(m_arg_i); expr* arg = e_arg->get_expr(); - A_f_i->insert(arg, e_arg->get_generation()); + A_f_i->insert(arg, ctx->get_generation(e_arg)); } } } @@ -1253,7 +1253,7 @@ namespace smt { if (ctx->is_relevant(n)) { enode* e_arg = n->get_arg(m_arg_i); expr* arg = e_arg->get_expr(); - s->insert(arg, e_arg->get_generation()); + s->insert(arg, ctx->get_generation(e_arg)); } } } @@ -1309,7 +1309,7 @@ namespace smt { bv_rw.mk_sub(arg, m_offset, arg_minus_k); else arith_rw.mk_sub(arg, m_offset, arg_minus_k); - S_j->insert(arg_minus_k, e_arg->get_generation()); + S_j->insert(arg_minus_k, ctx->get_generation(e_arg)); } } } @@ -1421,7 +1421,7 @@ namespace smt { auto e = n->get_expr(); if (srt == n->get_sort()) { TRACE(model_finder, tout << "inserting " << mk_pp(e, m) << " into inst set\n"); - S->insert(e, n->get_generation()); + S->insert(e, ctx->get_generation(n)); } else if (is_app(e) && to_app(e)->get_decl()->is_skolem()) ; @@ -1557,7 +1557,7 @@ namespace smt { if (ctx->is_relevant(p) && p->get_decl() == m_select->get_decl()) { SASSERT(m_arg_i < p->get_num_args()); enode* e_arg = p->get_arg(m_arg_i); - A_f_i->insert(e_arg->get_expr(), e_arg->get_generation()); + A_f_i->insert(e_arg->get_expr(), ctx->get_generation(e_arg)); } } } @@ -1686,7 +1686,7 @@ namespace smt { node* S_q_i = slv.get_uvar(q, m_var_i); for (enode* n : ctx->enodes()) { if (ctx->is_relevant(n) && n->get_expr()->get_sort() == s) { - S_q_i->insert(n->get_expr(), n->get_generation()); + S_q_i->insert(n->get_expr(), ctx->get_generation(n)); } } } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 19953be75d..9bd21238de 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -250,15 +250,12 @@ namespace smt { trace_stream() << "\n"; } else { std::ostream & out = trace_stream(); - obj_hashtable already_visited; - // In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables // is used. We need to make sure that all of these equalities appear in the log. for (unsigned i = 0; i < num_bindings; ++i) { log_justification_to_root(out, bindings[i], already_visited, m_context, m()); } - for (auto n : used_enodes) { enode *orig = std::get<0>(n); enode *substituted = std::get<1>(n); @@ -267,7 +264,6 @@ namespace smt { log_justification_to_root(out, substituted, already_visited, m_context, m()); } } - // At this point all relevant equalities for the match are logged. out << "[new-match] " << f->get_data_hash() << " #" << q->get_id() << " #" << pat->get_id(); for (unsigned i = 0; i < num_bindings; ++i) { @@ -288,7 +284,7 @@ namespace smt { out << "\n"; } } - + bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, @@ -709,8 +705,9 @@ namespace smt { } enode* n = m_context->get_enode(e); new_bindings.push_back(n); - if (n->get_generation() > max_gen) - max_gen = n->get_generation(); + unsigned gen = m_context->get_generation(n); + if (gen > max_gen) + max_gen = gen; } TRACE(ho_matching, diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp index f267cb481a..d1fca891c6 100644 --- a/src/smt/smt_quick_checker.cpp +++ b/src/smt/smt_quick_checker.cpp @@ -235,8 +235,8 @@ namespace smt { TRACE(quick_checker, tout << "found new candidate\n";); TRACE(quick_checker_sizes, tout << "found new candidate\n"; for (unsigned i = 0; i < m_num_bindings; ++i) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";); - unsigned max_generation = get_max_generation(m_num_bindings, m_bindings.data()); - if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(), + unsigned max_generation = get_max_generation(m_context, m_num_bindings, m_bindings.data()); + if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(), max_generation, 0, // min_top_generation is only available for instances created by the MAM 0, // max_top_generation is only available for instances created by the MAM diff --git a/src/util/chashtable.h b/src/util/chashtable.h index 5d4e4caa66..56d509f320 100644 --- a/src/util/chashtable.h +++ b/src/util/chashtable.h @@ -484,7 +484,7 @@ public: unsigned idx = h & mask; cell * c = m_table + idx; if (c->is_free()) - return; + return; cell * prev = nullptr; do { if (equals(c->m_data, d)) {