From 2788b8f49d5ced32278dac7f193f8fce2219bf24 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 2 Jul 2025 15:11:32 +0000
Subject: [PATCH] Optimize get_constructor_by_name: use func_decl* parameter,
 add linear search optimization for small datatypes, and ensure non-null
 postcondition

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/datatype_decl_plugin.cpp |  4 ++--
 src/ast/datatype_decl_plugin.h   | 30 ++++++++++++++++++++++--------
 2 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 53882b158..3daceb88c 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -1077,7 +1077,7 @@ namespace datatype {
         sort * datatype = con->get_range();
         def const& d = get_def(datatype);
         // 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) {
             for (accessor const* a : *c) {
                 func_decl_ref fn = a->instantiate(datatype);
@@ -1105,7 +1105,7 @@ namespace datatype {
         def const& dd = get_def(datatype);
         symbol r;
         // 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) {
             r = c->recognizer();
         }
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 5f260f115..7876f10c6 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -197,15 +197,29 @@ namespace datatype {
         util& u() const { return m_util; }
         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; }
-        constructor* get_constructor_by_name(symbol const& name) const {
-            // 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);
-                }
-            }
+        constructor* get_constructor_by_name(func_decl* con) const {
+            symbol const& name = con->get_name();
             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;
         }
         def* translate(ast_translation& tr, util& u);