mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 17:32:45 +00:00
Code Activity

Move get_max_generation to smt::context

Browse source
This commit is contained in:
Can Cebeci 2026-06-30 17:12:22 -07:00
parent 03572a61f8
commit dc241b85b9
3 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/mam.cpp
View file

@ -2541,7 +2541,7 @@ namespace {
case YIELD1:
m_bindings[0] = m_registers[static_cast<const yield *>(m_pc)->m_bindings[0]];
#define ON_MATCH(NUM) \
m_max_generation = std::max(m_max_generation, get_max_generation(m_context, 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; \
} \

2
src/smt/smt_enode.h
View file

@ -456,8 +456,6 @@ namespace smt {
bool aux;
return congruent(n1, n2, aux);
}
unsigned get_max_generation(context & ctx, unsigned num_enodes, enode * const * enodes);
void unmark_enodes(unsigned num_enodes, enode * const * enodes);

2
src/smt/smt_quick_checker.cpp
View file

@ -235,7 +235,7 @@ 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_context, 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