mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 23:43:15 +00:00
Code Activity

Optimize get_constructor_by_name: use func_decl* parameter, add linear search optimization for small datatypes, and ensure non-null postcondition

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-07-02 15:11:32 +00:00
parent dfdc31ae3b
commit 2788b8f49d
2 changed files with 24 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/datatype_decl_plugin.cpp
View file

@ -1077,7 +1077,7 @@ namespace datatype {
sort * datatype = con->get_range(); sort * datatype = con->get_range();
def const& d = get_def(datatype); def const& d = get_def(datatype);
// Use O(1) lookup instead of O(n) linear search // Use O(1) lookup instead of O(n) linear search
constructor* c = d.get_constructor_by_name(con->get_name()); constructor* c = d.get_constructor_by_name(con);
if (c) { if (c) {
for (accessor const* a : *c) { for (accessor const* a : *c) {
func_decl_ref fn = a->instantiate(datatype); func_decl_ref fn = a->instantiate(datatype);
@ -1105,7 +1105,7 @@ namespace datatype {
def const& dd = get_def(datatype); def const& dd = get_def(datatype);
symbol r; symbol r;
// Use O(1) lookup instead of O(n) linear search // Use O(1) lookup instead of O(n) linear search
constructor* c = dd.get_constructor_by_name(con->get_name()); constructor* c = dd.get_constructor_by_name(con);
if (c) { if (c) {
r = c->recognizer(); r = c->recognizer();
} }

30
src/ast/datatype_decl_plugin.h
View file

@ -197,15 +197,29 @@ namespace datatype {
util& u() const { return m_util; } util& u() const { return m_util; }
param_size::size* sort_size() { return m_sort_size; } param_size::size* sort_size() { return m_sort_size; }
void set_sort_size(param_size::size* p) { auto* q = m_sort_size; m_sort_size = p; if (p) p->inc_ref(); if (q) q->dec_ref(); m_sort = nullptr; } void set_sort_size(param_size::size* p) { auto* q = m_sort_size; m_sort_size = p; if (p) p->inc_ref(); if (q) q->dec_ref(); m_sort = nullptr; }
constructor* get_constructor_by_name(symbol const& name) const { constructor* get_constructor_by_name(func_decl* con) const {
// Lazy initialization of name-to-constructor map for O(1) lookups symbol const& name = con->get_name();
if (m_name2constructor.empty() && !m_constructors.empty()) {
for (constructor* c : m_constructors) {
m_name2constructor.insert(c->name(), c);
}
}
constructor* result = nullptr; constructor* result = nullptr;
m_name2constructor.find(name, result);
// For small datatypes (< 10 constructors), use linear search instead of hash table
if (m_constructors.size() < 10) {
for (constructor* c : m_constructors) {
if (c->name() == name) {
result = c;
break;
}
}
} else {
// Lazy initialization of name-to-constructor map for O(1) lookups
if (m_name2constructor.empty() && !m_constructors.empty()) {
for (constructor* c : m_constructors) {
m_name2constructor.insert(c->name(), c);
}
}
m_name2constructor.find(name, result);
}
SASSERT(result); // Post-condition: get_constructor_by_name returns a non-null result
return result; return result;
} }
def* translate(ast_translation& tr, util& u); def* translate(ast_translation& tr, util& u);