From a7def9e65d0738b462ca999ec1afe0c0c8cf47f2 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Fri, 16 Jan 2026 09:35:42 +0000
Subject: [PATCH] bot: restore std::format

---
 .../workflows/code-conventions-analyzer.md    | 43 ++++++++++++++++---
 1 file changed, 37 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/code-conventions-analyzer.md b/.github/workflows/code-conventions-analyzer.md
index 6330ba965..d27d5c24b 100644
--- a/.github/workflows/code-conventions-analyzer.md
+++ b/.github/workflows/code-conventions-analyzer.md
@@ -98,6 +98,7 @@ Z3 uses C++20 (as specified in `.clang-format`). Look for opportunities to use:
 - Three-way comparison operator (`<=>`)
 - Ranges library
 - Coroutines (if beneficial)
+- `std::format` for string formatting (replace stringstream for exceptions)
 
 ### 3. Common Library Function Usage
 
@@ -146,6 +147,23 @@ Identify opportunities specific to Z3's architecture and coding patterns:
 - Redundant AST creation calls (rebuilding same expression multiple times)
 - Opportunities to cache and reuse AST node references
 - Use of temporaries instead of repeated construction
+- **Nested API calls with non-deterministic argument evaluation**
+  - Detect expressions where multiple arguments to an API call are themselves API calls
+  - C++ does **not guarantee evaluation order of function arguments**, which can lead to:
+    - Platform-dependent performance differences
+    - Unintended allocation or reference-counting patterns
+    - Hard-to-reproduce profiling results
+  - Prefer storing intermediate results in temporaries to enforce evaluation order and improve clarity
+  - Example:
+    ```cpp
+    // Avoid
+    auto* v = m.mk_and(m.mk_or(a, b), m.mk_or(c, d));
+
+    // Prefer
+    auto* o1 = m.mk_or(a, b);
+    auto* o2 = m.mk_or(c, d);
+    auto* v  = m.mk_and(o1, o2);
+    ```
 
 **Hash Table Operations:**
 - Double hash lookups (check existence + insert/retrieve)
@@ -167,6 +185,13 @@ Identify opportunities specific to Z3's architecture and coding patterns:
 - Replace with `std::optional<T>` return values
 - Cleaner API that avoids pointer/reference output parameters
 
+**Exception String Construction:**
+- Using `stringstream` to build exception messages
+- Unnecessary string copies when raising exceptions
+- Replace with `std::format` for cleaner, more efficient code
+- Constant arguments should be merged into the string
+- Use `std::formatter` to avoid creating temporary strings
+
 **Bitfield Opportunities:**
 - Structs with multiple boolean flags
 - Small integer fields that could use bitfields
@@ -396,10 +421,10 @@ For each opportunity, provide:
 - **Bitfield Opportunities**: [Structs with bool flags or small integers]
 - **Estimated Savings**: [Total size reduction across codebase]
 
-### 4.4 AST Creation Efficiency
+### 4.4 AST Creation Efficiency and Determinism
 - **Redundant Creation**: [Examples of rebuilding same expression multiple times]
-- **Temporary Usage**: [Places where temporaries could be cached]
-- **Impact**: [Performance improvement potential]
+- **Temporary Usage**: [Places where temporaries could be cached and order of creation determinized]
+- **Impact**: [Performance improvement potential and determinism across platforms]
 
 ### 4.5 Hash Table Operation Optimization
 - **Double Lookups**: [Check existence + insert/get patterns]
@@ -423,18 +448,24 @@ For each opportunity, provide:
 - **API Improvements**: [Specific function signatures to update]
 - **Examples**: [File:line references with before/after]
 
-### 4.9 Array Parameter Modernization
+### 4.9 Exception String Construction
+- **Current**: [stringstream usage for building exception messages]
+- **Modern**: [std::format and std::formater opportunities]
+- **String Copies**: [Unnecessary copies when raising exceptions]
+- **Examples**: [Specific exception construction sites]
+
+### 4.10 Array Parameter Modernization
 - **Current**: [Pointer + size parameter pairs]
 - **Modern**: [std::span usage opportunities]
 - **Type Safety**: [How span improves API safety]
 - **Examples**: [Function signatures to update]
 
-### 4.10 Increment Operator Patterns
+### 4.11 Increment Operator Patterns
 - **Postfix Usage**: [Count of i++ where result is unused]
 - **Prefix Preference**: [Places to use ++i instead]
 - **Iterator Loops**: [Heavy iterator usage areas]
 
-### 4.11 Exception Control Flow
+### 4.12 Exception Control Flow
 - **Current Usage**: [Exceptions used for normal control flow]
 - **Modern Alternatives**: [std::expected, std::optional, error codes]
 - **Performance**: [Impact of exception-based control flow]