mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

Fix datatype performance by optimizing get_constructor_accessors 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 18:14:54 +00:00
parent a0168d80fa
commit fcbf9a07a3
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/datatype_decl_plugin.cpp
View file

@ -1070,6 +1070,12 @@ namespace datatype {
plugin().add_ast(con); plugin().add_ast(con);
plugin().m_vectors.push_back(res); plugin().m_vectors.push_back(res);
plugin().m_constructor2accessors.insert(con, res); plugin().m_constructor2accessors.insert(con, res);
// Early return for 0-ary constructors - they have no accessors by definition
if (con->get_arity() == 0) {
return res;
}
sort * datatype = con->get_range(); sort * datatype = con->get_range();
def const& d = get_def(datatype); def const& d = get_def(datatype);
for (constructor const* c : d) { for (constructor const* c : d) {