From 3f6a57e8a8cf7b73a1b459b5cf65899d6a043a4e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Jul 2026 15:43:41 -0700 Subject: [PATCH] Improve generation accounting (#10008) (#10009) Details in original PR: https://github.com/Z3Prover/z3/pull/10007 --------- --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Can Cebeci Co-authored-by: Can Cebeci --- src/smt/mam.cpp | 48 ++++--------- src/smt/smt_case_split_queue.cpp | 7 +- src/smt/smt_context.cpp | 119 ++++++++++++++++++++++++++++--- src/smt/smt_context.h | 49 ++++++++++++- src/smt/smt_enode.cpp | 43 +++-------- src/smt/smt_enode.h | 22 +++--- src/smt/smt_internalizer.cpp | 64 ++++++++++++++++- src/smt/smt_model_checker.cpp | 2 +- src/smt/smt_model_finder.cpp | 12 ++-- src/smt/smt_quantifier.cpp | 10 ++- src/smt/smt_quick_checker.cpp | 4 +- src/util/chashtable.h | 2 +- 12 files changed, 267 insertions(+), 115 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 80918fcb45..485228f059 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, m_context.get_max_generation(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_context.cpp b/src/smt/smt_context.cpp index 4fafb42980..b8e572513a 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); @@ -567,6 +568,10 @@ namespace smt { SASSERT(r1->get_root() == r2); reinsert_parents_into_cg_table(r1, r2, n1, n2, js); + + // We push the add_eq_trail after reinsert_parents_into_cg_table because the latter may push merge_cgc_generations trails, + // and we want add_eq to be undone before merge_cgc_generations is undone. + 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 +599,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 +610,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 +622,8 @@ namespace smt { SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent)); parent->set_mark(); if (parent->is_cgc_enabled()) { + if (!parent->is_eq()) // we don't track generations of equalities. + 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 +631,20 @@ 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()); + SASSERT(!n->is_eq()); + + // Callers are responsible for this. Sticky updates are too expensive to accommodate no-ops. + SASSERT(generation < get_generation(n)); + + set_generation(n, 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 +662,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 generation_cache_idx = 0; for (unsigned i = 0; i < num_r1_parents; ++i) { enode* parent = r1_parents[i]; if (!parent->is_marked()) @@ -659,25 +684,39 @@ namespace smt { assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs))); } // 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()) { + // Look up the generation cache + unsigned parent_generation = 0; // Just use generation 0 for equalities + if (!parent->is_eq()) { + auto [p, g] = m_r1_parent_generations[generation_cache_idx++]; + SASSERT(p == parent); + parent_generation = g; + } + auto [parent_prime, used_commutativity] = m_cg_table.insert(parent); if (parent_prime == parent) { SASSERT(parent); - SASSERT(parent->is_cgr()); + SASSERT(parent->is_cgr()); SASSERT(m_cg_table.contains_ptr(parent)); + parent->m_generation = 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); + 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 +724,7 @@ namespace smt { r2_parents.push_back(parent); } } + m_r1_parent_generations.reset(); } /** @@ -940,6 +980,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 +998,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 +1014,52 @@ namespace smt { // restore parents of r2 r2->m_parents.shrink(r2_num_parents); + unsigned generation_cache_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 - )) { + (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 (generation_cache_idx < m_r1_parent_generations.size()) { + std::tie(p, parent_generation) = m_r1_parent_generations[generation_cache_idx]; + } + if (p == parent) { + generation_cache_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] = m_cg_table.insert(parent); + (void)used_commutativity; parent->m_cg = parent_cg; + if (parent_cg == parent) + // parent is (again) the congruence root: restore its generation. + parent->m_generation = gen; } } } + 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 +1094,28 @@ 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) { + 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 +1379,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 +2342,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 191afdeac6..f0105ff633 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,7 +160,8 @@ 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; + vector> m_r1_parent_generations; // temporary field used to cache generations between remove_parents_from_cg_table and reinsert_parents_into_cg_table struct new_eq { enode * m_lhs; enode * m_rhs; @@ -615,6 +620,26 @@ 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; + + return get_cg_root(e)->m_generation; + } + + unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) { + unsigned max = 0; + for (unsigned i = 0; i < num_enodes; ++i) { + unsigned curr = get_generation(enodes[i]); + if (curr > max) + max = curr; + } + return max; + } + + void set_generation(enode * e, unsigned generation); + /** \brief Return true if the logical context internalized universal quantifiers. */ @@ -1131,12 +1156,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); + + 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 +1176,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 +1226,18 @@ 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 { + if (!n->uses_cg_table()) + return n; + // Fast path: if e is already the congruence root, avoid table lookup. + // This is important for performance, since get_cg_root is called on every generation lookup. + if (n->is_cgr()) + return n; + 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 c4af96369b..7e630f8a7d 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -21,7 +21,7 @@ Revision History: #include "smt/smt_enode.h" namespace smt { - + /** \brief Initialize an enode in the given memory position. */ @@ -65,8 +65,8 @@ namespace smt { } 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, - bool cgc_enabled, bool update_children_parent) { + unsigned generation, 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); @@ -131,20 +131,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 +147,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,16 +294,6 @@ namespace smt { } } - unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) { - unsigned max = 0; - for (unsigned i = 0; i < num_enodes; ++i) { - unsigned curr = enodes[i]->get_generation(); - if (curr > max) - max = curr; - } - return max; - } - void unmark_enodes(unsigned num_enodes, enode * const * enodes) { for (unsigned i = 0; i < num_enodes; ++i) enodes[i]->unset_mark(); diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 30a2b512af..1ba3d76b39 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -64,7 +64,7 @@ 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_generation; //!< Cached generation of the congruence class. Valid when is_cgr(), or when the enode does not use the cg_table (constants/leaves/true-eq nodes), where it directly stores the enode's generation. unsigned m_func_decl_id; //!< Id generated by the congruence table for fast indexing. @@ -102,7 +102,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; @@ -142,8 +142,8 @@ namespace smt { } 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); + unsigned generation, 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 +314,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 +397,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; @@ -459,8 +457,6 @@ namespace smt { bool aux; return congruent(n1, n2, aux); } - - unsigned get_max_generation(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 77fc5c0d84..3e8e5bb0fc 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -102,8 +102,60 @@ 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; + + if (0 < m_generation && m_generation < get_generation(e)) { + if (e->uses_cg_table()) + set_generation_sticky(e, m_generation); + else + set_generation(e, m_generation); + } + } + + 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; + + // The class generation is stored in the congruence root's m_generation field. + enode * cgr = get_cg_root(e); + cgr->m_generation = 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) { + 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->m_generation)); + + if (e1_generation >= e2->m_generation) + return; // no-op + + e2->m_generation = e1_generation; } void context::ts_visit_child(expr * n, bool gate_ctx, svector & todo, bool & visited) { @@ -1025,6 +1077,9 @@ namespace smt { auto [e_prime, used_commutativity] = m_cg_table.insert(e); if (e != e_prime) { e->m_cg = 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); push_new_congruence(e, e_prime, used_commutativity); } else { @@ -1042,6 +1097,7 @@ namespace smt { m_decl2enodes[decl_id].push_back(e); } } + 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 +1122,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 +1137,7 @@ 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); } /** diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 72dc51f8f0..56b8dfe759 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 62fab4b14c..c43028b40d 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1238,7 +1238,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)); } } } @@ -1256,7 +1256,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)); } } } @@ -1312,7 +1312,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)); } } } @@ -1434,7 +1434,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 (!use_term_enum) continue; @@ -1573,7 +1573,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)); } } } @@ -1702,7 +1702,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 455ea83c74..1a1e9a748b 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -249,9 +249,7 @@ 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) { @@ -264,7 +262,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) { @@ -285,7 +282,7 @@ namespace smt { out << "\n"; } } - + bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, @@ -724,8 +721,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 ad54d185b0..34f6b3843f 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 = m_context.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(), 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)) {