diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index dd6a1f4b0e..fab8563bcd 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -568,7 +568,9 @@ 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()) @@ -620,7 +622,7 @@ 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 need to worry about generations of equalities. + 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)); @@ -633,12 +635,12 @@ namespace smt { // Goes out of scope when n is garbage collected. void context::set_generation_sticky(enode * n, unsigned generation) { SASSERT(n->uses_cg_table()); - enode * cgr = get_cg_root(n); - SASSERT(cgr); - // Callers are responsible for this. Sticky updates are too expensive to accommodate no-ops. - SASSERT(generation < cgr->m_generation); + SASSERT(!n->is_eq()); - cgr->m_generation = generation; + // 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); } @@ -660,7 +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 cgc_enabled_idx = 0; + unsigned generation_cache_idx = 0; for (unsigned i = 0; i < num_r1_parents; ++i) { enode* parent = r1_parents[i]; if (!parent->is_marked()) @@ -687,18 +689,19 @@ namespace smt { } } 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[cgc_enabled_idx++]; + 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(m_cg_table.contains_ptr(parent)); - // parent is (again) the congruence root: cache its class generation on the enode. parent->m_generation = parent_generation; r2_parents.push_back(parent); @@ -1011,7 +1014,7 @@ namespace smt { // restore parents of r2 r2->m_parents.shrink(r2_num_parents); - unsigned cgr_parent_idx = 0; + unsigned generation_cache_idx = 0; // try to reinsert parents of r1 that are not cgr for (enode * parent : enode::parents(r1)) { @@ -1029,11 +1032,11 @@ namespace smt { } 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 (generation_cache_idx < m_r1_parent_generations.size()) { + std::tie(p, parent_generation) = m_r1_parent_generations[generation_cache_idx]; } if (p == parent) { - cgr_parent_idx++; + generation_cache_idx++; gen = parent_generation; } else { SASSERT(m_cg_table.contains_ptr(parent)); @@ -1049,9 +1052,7 @@ namespace smt { (void)used_commutativity; parent->m_cg = parent_cg; if (parent_cg == parent) - // parent is (again) the congruence root: restore its cached class generation. - // In the congruent case (parent_cg != parent) a subsequent - // undo_merge_cgc_generations restores the generation, so the dummy is fine. + // parent is (again) the congruence root: restore its generation. parent->m_generation = gen; } } @@ -1106,9 +1107,7 @@ namespace smt { 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. - + 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)) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index cece66fad5..000de5da14 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -161,8 +161,7 @@ namespace smt { enode_vector m_empty_vector; cg_table m_cg_table; enode_generation_table m_sticky_generation_updates; - vector> m_r1_parent_generations; // generations of parents removed from m_cg_table while merging r1 - + 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; @@ -626,14 +625,6 @@ namespace smt { if (e->is_eq()) return 0; - if (!e->uses_cg_table()) - return e->m_generation; - - // The class generation is cached on the congruence root's m_generation field. - // Fast path: if e is already the congruence root, read it directly. Otherwise - // locate the congruence root through the cg_table and read its cached value. - if (e->is_cgr()) - return e->m_generation; return get_cg_root(e)->m_generation; } @@ -1237,8 +1228,11 @@ namespace smt { enode * get_cg_root(enode * n) const { SASSERT(n->get_num_args() > 0); - if (!n->uses_cg_table()) - return n->get_cg(); + SASSERT(n->uses_cg_table() || n->is_cgr()); + // 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; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 05b458c544..a0a7db122d 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -106,12 +106,11 @@ namespace smt { 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 (0 < m_generation && m_generation < get_generation(e)) { if (e->uses_cg_table()) set_generation_sticky(e, m_generation); else - e->m_generation = m_generation; // Sticky by default. Won't unmerge + set_generation(e, m_generation); } } @@ -120,14 +119,9 @@ namespace smt { if (e->is_eq()) return; - if (e->uses_cg_table()) { - // The class generation is cached on the congruence root's m_generation field. - enode * cgr = e->is_cgr() ? e : get_cg_root(e); - SASSERT(cgr); - cgr->m_generation = generation; - } else { - e->m_generation = generation; - } + // 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 { @@ -151,12 +145,10 @@ namespace smt { }; void context::merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2) { - // 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)); - // The class generation is cached on the congruence root e2's m_generation field. // 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));