Skip to content

Commit 3f6a57e

Browse files
NikolajBjornerCanCebeciCan Cebeci
authored
Improve generation accounting (#10008) (#10009)
Details in original PR: #10007 --------- --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Can Cebeci <can.cebeci99@gmail.com> Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
1 parent c56b2cb commit 3f6a57e

12 files changed

Lines changed: 267 additions & 115 deletions

‎src/smt/mam.cpp‎

Lines changed: 14 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,6 @@ namespace {
215215
unsigned short m_num_args;
216216
unsigned m_ireg;
217217
unsigned m_oreg;
218-
unsigned m_curr_max_generation = 0;
219218
};
220219

221220
struct get_cgr : public instruction {
@@ -1881,47 +1880,33 @@ namespace {
18811880
m_pool.recycle(v);
18821881
}
18831882

1884-
void update_max_generation(enode * n, enode * prev, enode * min_gen_match=nullptr) {
1885-
unsigned new_gen = min_gen_match ? min_gen_match->get_generation() : n->get_generation();
1886-
1887-
m_max_generation = std::max(m_max_generation, new_gen);
1883+
void update_max_generation(enode * n, enode * prev) {
1884+
m_max_generation = std::max(m_max_generation, m_context.get_generation(n));
18881885

18891886
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
18901887
m_used_enodes.push_back(std::make_tuple(prev, n));
18911888
}
18921889

1893-
void get_f_app(func_decl* lbl, unsigned num_expected_args, enode* curr, enode*& matching_cgr, enode*& min_gen_match) {
1894-
if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args) {
1895-
if (curr->is_cgr() && !matching_cgr)
1896-
matching_cgr = curr;
1897-
1898-
if (!min_gen_match || min_gen_match->get_generation() > curr->get_generation()) {
1899-
min_gen_match = curr;
1900-
}
1901-
}
1902-
}
1903-
19041890
// We have to provide the number of expected arguments because we have flat-assoc applications such as +.
19051891
// Flat-assoc applications may have arbitrary number of arguments.
19061892
enode * get_first_f_app(func_decl * lbl, unsigned num_expected_args, enode * curr) {
19071893
enode * first = curr;
1908-
enode *matching_cgr = nullptr, *min_gen_match = nullptr;
19091894
do {
1910-
get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match);
1895+
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
1896+
update_max_generation(curr, first);
1897+
return curr;
1898+
}
19111899
curr = curr->get_next();
19121900
}
19131901
while (curr != first);
1914-
if (matching_cgr)
1915-
update_max_generation(matching_cgr, first, min_gen_match);
1916-
return matching_cgr;
1902+
return nullptr;
19171903
}
19181904

19191905
enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
19201906
curr = curr->get_next();
19211907
while (curr != first) {
1922-
if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr()) {
1923-
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
1924-
m_used_enodes.push_back(std::make_tuple(first, curr));
1908+
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
1909+
update_max_generation(curr, first);
19251910
return curr;
19261911
}
19271912
curr = curr->get_next();
@@ -2065,7 +2050,7 @@ namespace {
20652050
void get_min_max_top_generation(unsigned& min, unsigned& max) {
20662051
SASSERT(!m_pattern_instances.empty());
20672052
if (m_min_top_generation.empty()) {
2068-
min = max = m_pattern_instances[0]->get_generation();
2053+
min = max = m_context.get_generation(m_pattern_instances[0]);
20692054
m_min_top_generation.push_back(min);
20702055
m_max_top_generation.push_back(max);
20712056
}
@@ -2074,7 +2059,7 @@ namespace {
20742059
max = m_max_top_generation.back();
20752060
}
20762061
for (unsigned i = m_min_top_generation.size(); i < m_pattern_instances.size(); ++i) {
2077-
unsigned curr = m_pattern_instances[i]->get_generation();
2062+
unsigned curr = m_context.get_generation(m_pattern_instances[i]);
20782063
min = std::min(min, curr);
20792064
m_min_top_generation.push_back(min);
20802065
max = std::max(max, curr);
@@ -2315,7 +2300,8 @@ namespace {
23152300
m_min_top_generation.reset();
23162301
m_max_top_generation.reset();
23172302
m_pattern_instances.push_back(n);
2318-
m_max_generation = n->get_generation();
2303+
2304+
m_max_generation = m_context.get_generation(n);
23192305

23202306
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) {
23212307
m_used_enodes.reset();
@@ -2492,7 +2478,6 @@ namespace {
24922478
m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation; \
24932479
m_backtrack_stack[m_top].m_old_used_enodes_size = m_curr_used_enodes_size; \
24942480
m_backtrack_stack[m_top].m_curr = m_app; \
2495-
const_cast<bind*>(static_cast<const bind*>(m_pc))->m_curr_max_generation = m_max_generation; \
24962481
m_top++;
24972482

24982483
BIND_COMMON();
@@ -2556,7 +2541,7 @@ namespace {
25562541
case YIELD1:
25572542
m_bindings[0] = m_registers[static_cast<const yield *>(m_pc)->m_bindings[0]];
25582543
#define ON_MATCH(NUM) \
2559-
m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \
2544+
m_max_generation = std::max(m_max_generation, m_context.get_max_generation(NUM, m_bindings.begin())); \
25602545
if (m_context.get_cancel_flag()) { \
25612546
return false; \
25622547
} \
@@ -2760,7 +2745,6 @@ namespace {
27602745
#define BBIND_COMMON() m_b = static_cast<const bind*>(bp.m_instr); \
27612746
m_n1 = m_registers[m_b->m_ireg]; \
27622747
m_app = get_next_f_app(m_b->m_label, m_b->m_num_args, m_n1, bp.m_curr); \
2763-
m_max_generation = m_b->m_curr_max_generation; \
27642748
if (!m_app) { \
27652749
m_top--; \
27662750
goto backtrack; \
@@ -3972,10 +3956,6 @@ namespace {
39723956
}
39733957
return;
39743958
}
3975-
DEBUG_CODE(
3976-
for (unsigned i = 0; i < num_bindings; ++i) {
3977-
SASSERT(bindings[i]->get_generation() <= max_generation);
3978-
});
39793959

39803960
#endif
39813961
unsigned min_gen = 0, max_gen = 0;

‎src/smt/smt_case_split_queue.cpp‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1012,7 +1012,7 @@ namespace {
10121012
stack.pop_back();
10131013

10141014
if (m_context.e_internalized(curr)) {
1015-
gen = m_context.get_enode(curr)->get_generation();
1015+
gen = m_context.get_generation(m_context.get_enode(curr));
10161016
if (gen > maxgen)
10171017
maxgen = gen;
10181018
if (gen < mingen)
@@ -1046,7 +1046,7 @@ namespace {
10461046
void operator()(expr * e) {
10471047
if (m_context.e_internalized(e)) {
10481048
enode * n = m_context.get_enode(e);
1049-
n->set_generation(&m_context, m_generation);
1049+
m_context.set_generation(n, m_generation);
10501050
}
10511051
}
10521052
};
@@ -1069,7 +1069,8 @@ namespace {
10691069
stack.pop_back();
10701070

10711071
if (m_context.e_internalized(curr)) {
1072-
unsigned curr_gen = m_context.get_enode(curr)->get_generation();
1072+
enode * n = m_context.get_enode(curr);
1073+
unsigned curr_gen = m_context.get_generation(n);
10731074
if (curr_gen > gen) {
10741075
// Lower it.
10751076
set_generation_rec(e, gen);

0 commit comments

Comments
 (0)