mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 06:00:53 +00:00
Code Activity

Optimize datatype CLI performance by skipping accessor loop for 0-ary constructors

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-07-01 17:19:21 +00:00
parent cb8fcdea11
commit a0168d80fa
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/cmd_context.cpp
View file

@ -2477,11 +2477,13 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
func_decl * r = m_dt_util.get_constructor_recognizer(c); func_decl * r = m_dt_util.get_constructor_recognizer(c);
m_owner.insert(r); m_owner.insert(r);
// TRACE(new_dt_eh, tout << "new recognizer: " << r->get_name() << "\n";); // TRACE(new_dt_eh, tout << "new recognizer: " << r->get_name() << "\n";);
if (c->get_arity() > 0) {
for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) { for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) {
TRACE(new_dt_eh, tout << "new accessor: " << a->get_name() << "\n";); TRACE(new_dt_eh, tout << "new accessor: " << a->get_name() << "\n";);
m_owner.insert(a); m_owner.insert(a);
} }
} }
}
if (!m_owner.m_scopes.empty() && !m_owner.m_global_decls) { if (!m_owner.m_scopes.empty() && !m_owner.m_global_decls) {
m_owner.pm().inc_ref(pd); m_owner.pm().inc_ref(pd);
m_owner.m_psort_inst_stack.push_back(pd); m_owner.m_psort_inst_stack.push_back(pd);