From 6d5f050ed1ad65fa8ebbad67c21c466c7c44fe59 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 11 Jan 2026 17:44:59 -0800 Subject: [PATCH] Convert internal class enums to enum class for type safety (#8158) * Initial plan * Convert plain enums to enum class in EUF module - Convert eq_status in euf::ac_plugin to enum class - Convert undo_kind in euf::ac_plugin to enum class - Convert undo_t in euf::arith_plugin to enum class - Convert to_merge_t in euf::egraph to enum class - Update all usage sites to use scoped enum syntax Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Convert more plain enums to enum class - Convert state enum in substitution class - Convert instruction enum in generic_model_converter class - Convert eq_type enum in bit2int class - Update all usage sites to use scoped enum syntax Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .../converters/generic_model_converter.cpp | 10 ++--- src/ast/converters/generic_model_converter.h | 4 +- src/ast/euf/euf_ac_plugin.cpp | 38 +++++++++---------- src/ast/euf/euf_ac_plugin.h | 6 +-- src/ast/euf/euf_arith_plugin.h | 2 +- src/ast/euf/euf_egraph.cpp | 8 ++-- src/ast/euf/euf_egraph.h | 10 ++--- src/ast/rewriter/bit2int.cpp | 16 ++++---- src/ast/rewriter/bit2int.h | 2 +- src/ast/substitution/substitution.cpp | 8 ++-- src/ast/substitution/substitution.h | 4 +- 11 files changed, 54 insertions(+), 54 deletions(-) diff --git a/src/ast/converters/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp index ed73106b2..9d8389e78 100644 --- a/src/ast/converters/generic_model_converter.cpp +++ b/src/ast/converters/generic_model_converter.cpp @@ -32,7 +32,7 @@ Notes: void generic_model_converter::add(func_decl * d, expr* e) { VERIFY(e); VERIFY(d->get_range() == e->get_sort()); - m_entries.push_back(entry(d, e, m, ADD)); + m_entries.push_back(entry(d, e, m, instruction::ADD)); } void generic_model_converter::operator()(model_ref & md) { @@ -138,9 +138,9 @@ void generic_model_converter::convert_initialize_value(vectorget_decl()) convert_initialize_value(e.m_def, i, var2value); break; @@ -203,14 +203,14 @@ void generic_model_converter::get_units(obj_map& units) { for (unsigned i = m_entries.size(); i-- > 0;) { entry const& e = m_entries[i]; switch (e.m_instruction) { - case HIDE: + case instruction::HIDE: tmp = m.mk_const(e.m_f); if (units.contains(tmp)) { m.dec_ref(tmp); units.remove(tmp); } break; - case ADD: + case instruction::ADD: if (e.m_f->get_arity() == 0 && m.is_bool(e.m_f->get_range())) { tmp = m.mk_const(e.m_f); if (units.contains(tmp)) { diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h index 88c70bef0..e176243c0 100644 --- a/src/ast/converters/generic_model_converter.h +++ b/src/ast/converters/generic_model_converter.h @@ -23,7 +23,7 @@ Notes: class generic_model_converter : public model_converter { public: - enum instruction { HIDE, ADD }; + enum class instruction { HIDE, ADD }; struct entry { func_decl_ref m_f; expr_ref m_def; @@ -44,7 +44,7 @@ public: void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } - void hide(func_decl * f) { m_entries.push_back(entry(f, nullptr, m, HIDE)); } + void hide(func_decl * f) { m_entries.push_back(entry(f, nullptr, m, instruction::HIDE)); } void add(func_decl * d, expr* e); diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index 431147097..89d25b154 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/src/ast/euf/euf_ac_plugin.cpp @@ -154,64 +154,64 @@ namespace euf { for (auto arg : ns) { arg->shared.push_back(idx); m_node_trail.push_back(arg); - push_undo(is_add_shared_index); + push_undo(undo_kind::is_add_shared_index); } m_shared_nodes.setx(n->get_id(), true, false); sort(monomial(m)); m_shared_todo.insert(idx); m_shared.push_back({ n, m, justification::axiom(get_id()) }); - push_undo(is_register_shared); + push_undo(undo_kind::is_register_shared); } void ac_plugin::push_scope_eh() { - push_undo(is_push_scope); + push_undo(undo_kind::is_push_scope); } void ac_plugin::undo() { auto k = m_undo.back(); m_undo.pop_back(); switch (k) { - case is_queue_eq: { + case undo_kind::is_queue_eq: { m_queued.pop_back(); break; } - case is_add_node: { + case undo_kind::is_add_node: { auto* n = m_node_trail.back(); m_node_trail.pop_back(); m_nodes[n->n->get_id()] = nullptr; n->~node(); break; } - case is_push_scope: { + case undo_kind::is_push_scope: { m_active.reset(); m_passive.reset(); m_units.reset(); m_queue_head = 0; break; } - case is_add_monomial: { + case undo_kind::is_add_monomial: { m_monomials.pop_back(); break; } - case is_add_shared_index: { + case undo_kind::is_add_shared_index: { auto n = m_node_trail.back(); m_node_trail.pop_back(); n->shared.pop_back(); break; } - case is_add_eq_index: { + case undo_kind::is_add_eq_index: { auto n = m_node_trail.back(); m_node_trail.pop_back(); n->eqs.pop_back(); break; } - case is_register_shared: { + case undo_kind::is_register_shared: { auto s = m_shared.back(); m_shared_nodes[s.n->get_id()] = false; m_shared.pop_back(); break; } - case is_update_shared: { + case undo_kind::is_update_shared: { auto [id, s] = m_update_shared_trail.back(); m_shared[id] = s; m_update_shared_trail.pop_back(); @@ -345,7 +345,7 @@ namespace euf { if (l == r) return; m_queued.push_back({ l, r }); - push_undo(is_queue_eq); + push_undo(undo_kind::is_queue_eq); } bool ac_plugin::init_equation(eq eq, bool is_active) { @@ -376,7 +376,7 @@ namespace euf { if (!n->n->is_marked2()) { n->eqs.push_back(eq_id); n->n->mark2(); - push_undo(is_add_eq_index); + push_undo(undo_kind::is_add_eq_index); m_node_trail.push_back(n); for (auto s : n->shared) m_shared_todo.insert(s); @@ -387,7 +387,7 @@ namespace euf { if (!n->n->is_marked2()) { n->eqs.push_back(eq_id); n->n->mark2(); - push_undo(is_add_eq_index); + push_undo(undo_kind::is_add_eq_index); m_node_trail.push_back(n); for (auto s : n->shared) m_shared_todo.insert(s); @@ -541,7 +541,7 @@ namespace euf { unsigned ac_plugin::to_monomial(enode* e, ptr_vector const& ms) { unsigned id = m_monomials.size(); m_monomials.push_back({ ms, bloom(), e }); - push_undo(is_add_monomial); + push_undo(undo_kind::is_add_monomial); return id; } @@ -581,7 +581,7 @@ namespace euf { if (m_nodes.size() > id && m_nodes[id]) return m_nodes[id]; auto* r = node::mk(get_region(), n); - push_undo(is_add_node); + push_undo(undo_kind::is_add_node); m_nodes.setx(id, r, nullptr); m_node_trail.push_back(r); if (is_op(n)) { @@ -1137,7 +1137,7 @@ namespace euf { n->eqs.push_back(eq); m_node_trail.push_back(n); n->n->mark2(); - push_undo(is_add_eq_index); + push_undo(undo_kind::is_add_eq_index); } } for (auto n : old_r) @@ -1435,13 +1435,13 @@ namespace euf { n->shared.push_back(idx); m_shared_todo.insert(idx); m_node_trail.push_back(n); - push_undo(is_add_shared_index); + push_undo(undo_kind::is_add_shared_index); } } for (auto n : monomial(old_m)) n->n->unmark2(); m_update_shared_trail.push_back({ idx, s }); - push_undo(is_update_shared); + push_undo(undo_kind::is_update_shared); m_shared[idx].m = new_m; m_shared[idx].j = j; TRACE(plugin_verbose, tout << "shared simplified to " << m_pp_ll(*this, monomial(new_m)) << "\n"); diff --git a/src/ast/euf/euf_ac_plugin.h b/src/ast/euf/euf_ac_plugin.h index 2aa49c9f3..99d01791c 100644 --- a/src/ast/euf/euf_ac_plugin.h +++ b/src/ast/euf/euf_ac_plugin.h @@ -56,7 +56,7 @@ namespace euf { uint64_t m_filter = 0; }; - enum eq_status { + enum class eq_status { is_processed_eq, is_passive_eq, is_to_simplify_eq, is_reducing_eq, is_dead_eq }; @@ -65,7 +65,7 @@ namespace euf { eq(unsigned l, unsigned r, justification j): l(l), r(r), j(j) {} unsigned l, r; // refer to monomials - eq_status status = is_to_simplify_eq; + eq_status status = eq_status::is_to_simplify_eq; justification j; // justification for equality }; @@ -146,7 +146,7 @@ namespace euf { // backtrackable state - enum undo_kind { + enum class undo_kind { is_queue_eq, is_add_monomial, is_add_node, diff --git a/src/ast/euf/euf_arith_plugin.h b/src/ast/euf/euf_arith_plugin.h index 63f92a3f2..fddb951dd 100644 --- a/src/ast/euf/euf_arith_plugin.h +++ b/src/ast/euf/euf_arith_plugin.h @@ -25,7 +25,7 @@ namespace euf { class egraph; class arith_plugin : public plugin { - enum undo_t { undo_add, undo_mul }; + enum class undo_t { undo_add, undo_mul }; arith_util a; svector m_undo; ac_plugin m_add, m_mul; diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 3f4f355f0..5ad79cd84 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -661,14 +661,14 @@ namespace euf { for (; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) { auto const& w = m_to_merge[i]; switch (w.t) { - case to_merge_plain: - case to_merge_comm: + case to_merge_t::to_merge_plain: + case to_merge_t::to_merge_comm: merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++)); break; - case to_justified: + case to_merge_t::to_justified: merge(w.a, w.b, w.j); break; - case to_add_literal: + case to_merge_t::to_add_literal: add_literal(w.a, w.b); break; } diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index ba0712e3b..6abcd38e1 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -88,15 +88,15 @@ namespace euf { typedef ptr_vector trail_stack; - enum to_merge_t { to_merge_plain, to_merge_comm, to_justified, to_add_literal }; + enum class to_merge_t { to_merge_plain, to_merge_comm, to_justified, to_add_literal }; struct to_merge { enode* a, * b; to_merge_t t; justification j; - bool commutativity() const { return t == to_merge_comm; } - to_merge(enode* a, enode* b, bool c) : a(a), b(b), t(c ? to_merge_comm : to_merge_plain) {} - to_merge(enode* a, enode* b, justification j): a(a), b(b), t(to_justified), j(j) {} - to_merge(enode* p, enode* ante): a(p), b(ante), t(to_add_literal) {} + bool commutativity() const { return t == to_merge_t::to_merge_comm; } + to_merge(enode* a, enode* b, bool c) : a(a), b(b), t(c ? to_merge_t::to_merge_comm : to_merge_t::to_merge_plain) {} + to_merge(enode* a, enode* b, justification j): a(a), b(b), t(to_merge_t::to_justified), j(j) {} + to_merge(enode* p, enode* ante): a(p), b(ante), t(to_merge_t::to_add_literal) {} }; struct stats { diff --git a/src/ast/rewriter/bit2int.cpp b/src/ast/rewriter/bit2int.cpp index 5037776d0..3bf921fae 100644 --- a/src/ast/rewriter/bit2int.cpp +++ b/src/ast/rewriter/bit2int.cpp @@ -138,14 +138,14 @@ bool bit2int::mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result) { align_sizes(tmp1, tmp2); SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2)); switch(ty) { - case lt: + case eq_type::lt: tmp3 = m_rewriter.mk_ule(tmp2, tmp1); result = m.mk_not(tmp3); break; - case le: + case eq_type::le: result = m_rewriter.mk_ule(tmp1, tmp2); break; - case eq: + case eq_type::eq: result = m.mk_eq(tmp1, tmp2); break; } @@ -313,7 +313,7 @@ void bit2int::visit(app* n) { is_bv_poly(e2, pos2, neg2) && mk_add(pos1, neg2, tmp1) && mk_add(neg1, pos2, tmp2) && - mk_comp(eq, tmp1, tmp2, result)) { + mk_comp(eq_type::eq, tmp1, tmp2, result)) { cache_result(n, result); } else if (m_arith_util.is_le(n) && @@ -321,7 +321,7 @@ void bit2int::visit(app* n) { is_bv_poly(e2, pos2, neg2) && mk_add(pos1, neg2, tmp1) && mk_add(neg1, pos2, tmp2) && - mk_comp(le, tmp1, tmp2, result)) { + mk_comp(eq_type::le, tmp1, tmp2, result)) { cache_result(n, result); } else if (m_arith_util.is_lt(n) && @@ -329,7 +329,7 @@ void bit2int::visit(app* n) { is_bv_poly(e2, pos2, neg2) && mk_add(pos1, neg2, tmp1) && mk_add(neg1, pos2, tmp2) && - mk_comp(lt, tmp1, tmp2, result)) { + mk_comp(eq_type::lt, tmp1, tmp2, result)) { cache_result(n, result); } else if (m_arith_util.is_ge(n) && @@ -337,7 +337,7 @@ void bit2int::visit(app* n) { is_bv_poly(e2, pos2, neg2) && mk_add(pos1, neg2, tmp1) && mk_add(neg1, pos2, tmp2) && - mk_comp(le, tmp2, tmp1, result)) { + mk_comp(eq_type::le, tmp2, tmp1, result)) { cache_result(n, result); } else if (m_arith_util.is_gt(n) && @@ -345,7 +345,7 @@ void bit2int::visit(app* n) { is_bv_poly(e2, pos2, neg2) && mk_add(pos1, neg2, tmp1) && mk_add(neg1, pos2, tmp2) && - mk_comp(lt, tmp2, tmp1, result)) { + mk_comp(eq_type::lt, tmp2, tmp1, result)) { cache_result(n, result); } else if (m_arith_util.is_mod(n) && diff --git a/src/ast/rewriter/bit2int.h b/src/ast/rewriter/bit2int.h index 8fa66e3e6..133fcc2bf 100644 --- a/src/ast/rewriter/bit2int.h +++ b/src/ast/rewriter/bit2int.h @@ -27,7 +27,7 @@ class bit2int { protected: typedef rational numeral; - enum eq_type { + enum class eq_type { lt, le, eq diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index db88b0d6b..03ebc21a9 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -26,7 +26,7 @@ substitution::substitution(ast_manager & m): m_manager(m), m_refs(m), m_new_exprs(m), - m_state(CLEAN) { + m_state(state::CLEAN) { } void substitution::reset() { @@ -44,7 +44,7 @@ void substitution::reset_cache() { m_apply_cache.reset(); m_new_exprs.reset(); - m_state = CLEAN; + m_state = state::CLEAN; } void substitution::pop_scope(unsigned num_scopes) { @@ -79,10 +79,10 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e // It is incorrect to cache results between different calls if we are applying a substitution // modulo a substitution s -> t. - if (m_state == INSERT || s != expr_offset(nullptr,0)) + if (m_state == state::INSERT || s != expr_offset(nullptr,0)) reset_cache(); - m_state = APPLY; + m_state = state::APPLY; unsigned j; expr * e = nullptr; diff --git a/src/ast/substitution/substitution.h b/src/ast/substitution/substitution.h index 98a9379e2..71d64499e 100644 --- a/src/ast/substitution/substitution.h +++ b/src/ast/substitution/substitution.h @@ -60,7 +60,7 @@ class substitution { // keep track of how substitution state was last updated. - enum state { CLEAN, APPLY, INSERT }; + enum class state { CLEAN, APPLY, INSERT }; state m_state; #ifdef Z3DEBUG @@ -137,7 +137,7 @@ public: m_vars.push_back(var_offset(v_idx, offset)); m_refs.push_back(t.get_expr()); m_subst.insert(v_idx, offset, t); - m_state = INSERT; + m_state = state::INSERT; } void insert(var * v, unsigned offset, expr_offset const & t) { insert(v->get_idx(), offset, t); } void insert(expr_offset v, expr_offset const & t) {