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-07-01 09:44:05 -07:00
parent dc241b85b9
commit 39dc236e01
2 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_context.h
View file

@ -635,6 +635,16 @@ namespace smt {
return *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);
/**

10
src/smt/smt_enode.cpp
View file

@ -293,16 +293,6 @@ namespace smt {
}
}
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 = ctx.get_generation(enodes[i]);
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();