diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 3b9ae912ef..2e20545475 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -30,6 +30,7 @@ set(CLANG_ONLY_WARNINGS "-Wignored-qualifiers" "-Wnoctad-maybe-unsupported" "-Wdeprecated-copy-with-user-provided-copy" + "-Wgnu-anonymous-struct" ) set(MSVC_WARNINGS "/W3") diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 7240d60e86..46fa054250 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -452,8 +452,8 @@ namespace euf { undo_add_th_var(p.r1, p.r2_num_parents); break; case update_record::tag_t::is_replace_th_var: - SASSERT(p.r1->get_th_var(p.m_th_id) != null_theory_var); - p.r1->replace_th_var(p.m_old_th_var, p.m_th_id); + SASSERT(p.r1->get_th_var(p.m_th.m_th_id) != null_theory_var); + p.r1->replace_th_var(p.m_th.m_old_th_var, p.m_th.m_th_id); break; case update_record::tag_t::is_new_th_eq: m_new_th_eqs.pop_back(); @@ -490,7 +490,7 @@ namespace euf { } break; case update_record::tag_t::is_plugin_undo: - m_plugins[p.m_th_id]->undo(); + m_plugins[p.m_th.m_th_id]->undo(); break; default: UNREACHABLE(); diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 6abcd38e1c..bae18e043d 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -137,7 +137,7 @@ namespace euf { struct { unsigned m_th_id : 8; unsigned m_old_th_var : 24; - }; + } m_th; unsigned qhead; bool m_inconsistent; signed char m_lbl_hash; @@ -154,7 +154,7 @@ namespace euf { update_record(enode* n, unsigned id, add_th_var) : tag(tag_t::is_add_th_var), r1(n), n1(nullptr), r2_num_parents(id) {} update_record(enode* n, theory_id id, theory_var v, replace_th_var) : - tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th_id(id), m_old_th_var(v) {} + tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th(id, v) {} update_record(new_th_eq) : tag(tag_t::is_new_th_eq), r1(nullptr), n1(nullptr), r2_num_parents(0) {} update_record(unsigned qh, new_th_eq_qhead): @@ -174,7 +174,7 @@ namespace euf { update_record(enode* n, set_relevant) : tag(tag_t::is_set_relevant), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {} update_record(unsigned th_id, plugin_undo) : - tag(tag_t::is_plugin_undo), r1(nullptr), n1(nullptr), m_th_id(th_id) {} + tag(tag_t::is_plugin_undo), r1(nullptr), n1(nullptr), m_th(th_id) {} }; ast_manager& m; svector m_to_merge; diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp index 8148fe7d9d..4ce83cfeb9 100644 --- a/src/ast/euf/euf_mam.cpp +++ b/src/ast/euf/euf_mam.cpp @@ -1874,7 +1874,7 @@ namespace euf { enode_vector * m_to_recycle; enode * const * m_it; enode * const * m_end; - }; + } m_rest; }; }; @@ -2212,32 +2212,33 @@ namespace euf { backtrack_point & bp = m_backtrack_stack[m_top]; bp.m_instr = c; bp.m_old_max_generation = m_max_generation; + auto& bp_rest = bp.m_rest; if (best_v == nullptr) { TRACE(mam_bug, tout << "m_top: " << m_top << ", m_backtrack_stack.size(): " << m_backtrack_stack.size() << "\n"; tout << *c << "\n";); - bp.m_to_recycle = nullptr; - bp.m_it = ctx.get_egraph().enodes_of(lbl).begin(); - bp.m_end = ctx.get_egraph().enodes_of(lbl).end(); + bp_rest.m_to_recycle = nullptr; + bp_rest.m_it = ctx.get_egraph().enodes_of(lbl).begin(); + bp_rest.m_end = ctx.get_egraph().enodes_of(lbl).end(); } else { SASSERT(!best_v->empty()); - bp.m_to_recycle = best_v; - bp.m_it = best_v->begin(); - bp.m_end = best_v->end(); + bp_rest.m_to_recycle = best_v; + bp_rest.m_it = best_v->begin(); + bp_rest.m_end = best_v->end(); } // find application with the right number of arguments - for (; bp.m_it != bp.m_end; ++bp.m_it) { - enode * curr = *bp.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + enode * curr = *bp_rest.m_it; if (curr->num_args() == expected_num_args && ctx.is_relevant(curr)) break; } - if (bp.m_it == bp.m_end) { - recycle_enode_vector(bp.m_to_recycle); + if (bp_rest.m_it == bp_rest.m_end) { + recycle_enode_vector(bp_rest.m_to_recycle); return nullptr; } m_top++; - update_max_generation(*(bp.m_it), nullptr); - return *(bp.m_it); + update_max_generation(*(bp_rest.m_it), nullptr); + return *(bp_rest.m_it); } void interpreter::display_reg(std::ostream & out, unsigned reg) { @@ -2812,8 +2813,8 @@ namespace euf { // Cleanup before exiting while (m_top != 0) { backtrack_point & bp = m_backtrack_stack[m_top - 1]; - if (bp.m_instr->m_opcode == CONTINUE && bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp.m_instr->m_opcode == CONTINUE && bp.m_rest.m_to_recycle) + recycle_enode_vector(bp.m_rest.m_to_recycle); m_top--; } #ifdef _PROFILE_MAM @@ -2910,10 +2911,11 @@ namespace euf { m_pc = bp.m_instr->m_next; goto main_loop; - case CONTINUE: - ++bp.m_it; - for (; bp.m_it != bp.m_end; ++bp.m_it) { - m_app = *bp.m_it; + case CONTINUE: { + auto &bp_rest = bp.m_rest; + ++bp_rest.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + m_app = *bp_rest.m_it; const cont * c = static_cast(bp.m_instr); // bp.m_it may reference an enode in [begin_enodes_of(lbl), end_enodes_of(lbl)) // This enodes are not necessarily relevant. @@ -2939,11 +2941,11 @@ namespace euf { } } // continue failed - if (bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp_rest.m_to_recycle) + recycle_enode_vector(bp_rest.m_to_recycle); m_top--; goto backtrack; - + } default: UNREACHABLE(); } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 485228f059..61a94361eb 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1833,7 +1833,7 @@ namespace { enode_vector * m_to_recycle; enode * const * m_it; enode * const * m_end; - }; + } m_rest; }; }; @@ -2194,35 +2194,36 @@ namespace { bp.m_instr = c; bp.m_old_max_generation = m_max_generation; bp.m_old_used_enodes_size = m_used_enodes.size(); + auto& bp_rest = bp.m_rest; if (best_v == nullptr) { TRACE(mam_bug, tout << "m_top: " << m_top << ", m_backtrack_stack.size(): " << m_backtrack_stack.size() << "\n"; tout << *c << "\n";); - bp.m_to_recycle = nullptr; - bp.m_it = m_context.begin_enodes_of(lbl); - bp.m_end = m_context.end_enodes_of(lbl); + bp_rest.m_to_recycle = nullptr; + bp_rest.m_it = m_context.begin_enodes_of(lbl); + bp_rest.m_end = m_context.end_enodes_of(lbl); } else { SASSERT(!best_v->empty()); - bp.m_to_recycle = best_v; - bp.m_it = best_v->begin(); - bp.m_end = best_v->end(); + bp_rest.m_to_recycle = best_v; + bp_rest.m_it = best_v->begin(); + bp_rest.m_end = best_v->end(); } // find application with the right number of arguments - for (; bp.m_it != bp.m_end; ++bp.m_it) { - enode * curr = *bp.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + enode * curr = *bp_rest.m_it; if (curr->get_num_args() == expected_num_args && m_context.is_relevant(curr)) break; } - if (bp.m_it == bp.m_end) { + if (bp_rest.m_it == bp_rest.m_end) { if (best_v) { - bp.m_to_recycle = nullptr; + bp_rest.m_to_recycle = nullptr; recycle_enode_vector(best_v); } return nullptr; } m_top++; - update_max_generation(*(bp.m_it), nullptr); - return *(bp.m_it); + update_max_generation(*(bp_rest.m_it), nullptr); + return *(bp_rest.m_it); } #ifdef _TRACE @@ -2723,8 +2724,8 @@ namespace { // Cleanup before exiting while (m_top != 0) { backtrack_point & bp = m_backtrack_stack[m_top - 1]; - if (bp.m_instr->m_opcode == CONTINUE && bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp.m_instr->m_opcode == CONTINUE && bp.m_rest.m_to_recycle) + recycle_enode_vector(bp.m_rest.m_to_recycle); m_top--; } #ifdef _PROFILE_MAM @@ -2811,10 +2812,11 @@ namespace { m_pc = m_b->m_next; goto main_loop; - case CONTINUE: - ++bp.m_it; - for (; bp.m_it != bp.m_end; ++bp.m_it) { - m_app = *bp.m_it; + case CONTINUE: { + auto &bp_rest = bp.m_rest; + ++bp_rest.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + m_app = *bp_rest.m_it; const cont * c = static_cast(bp.m_instr); // bp.m_it may reference an enode in [begin_enodes_of(lbl), end_enodes_of(lbl)) // This enodes are not necessarily relevant. @@ -2840,11 +2842,11 @@ namespace { } } // continue failed - if (bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp_rest.m_to_recycle) + recycle_enode_vector(bp_rest.m_to_recycle); m_top--; goto backtrack; - + } default: UNREACHABLE(); } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index c1bed6fdb8..fae8ee9720 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1281,8 +1281,8 @@ namespace smt { switch (elem.m_kind) { case tp_elem::EQUALITY: { - enode * lhs = elem.m_lhs; - enode * rhs = elem.m_rhs; + enode * lhs = elem.m_pair.m_lhs; + enode * rhs = elem.m_pair.m_rhs; if (m_eq2proof.contains(lhs, rhs)) m_todo_pr.pop_back(); else if (visit_eq_justications(lhs, rhs)) { diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h index 54e91ba941..1a10873d79 100644 --- a/src/smt/smt_conflict_resolution.h +++ b/src/smt/smt_conflict_resolution.h @@ -91,10 +91,10 @@ namespace smt { struct { enode * m_lhs; enode * m_rhs; - }; + } m_pair; }; tp_elem(literal l):m_kind(LITERAL), m_lidx(l.index()) {} - tp_elem(enode * lhs, enode * rhs):m_kind(EQUALITY), m_lhs(lhs), m_rhs(rhs) {} + tp_elem(enode * lhs, enode * rhs):m_kind(EQUALITY), m_pair(lhs, rhs) {} tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) { SASSERT(js);} };