Extend code-conventions-analyzer workflow with Z3-specific C++ modernization patterns (#8187)

* Initial plan

* Update code-conventions-analyzer workflow with modern C++ preferences

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

.github/workflows/code-conventions-analyzer.md

@@ -94,10 +94,11 @@ Z3 uses C++20 (as specified in `.clang-format`). Look for opportunities to use:
 
 **C++20 features:**
 - Concepts for template constraints (where appropriate)
-- `std::span` for array views
+- `std::span` for array views (especially for array pointer + size parameters)
 - Three-way comparison operator (`<=>`)
 - Ranges library
 - Coroutines (if beneficial)
+- `std::format` for string formatting (replace stringstream for exceptions)
 
 ### 3. Common Library Function Usage
 
@@ -106,6 +107,78 @@ Look for patterns where Z3 could better leverage standard library features:
 - Manual memory management that could use RAII
 - Custom container implementations vs standard containers
 - String manipulation that could use modern string APIs
+- Use `std::clamp` to truncate values to min/max instead of manual comparisons
+
+### 4. Z3-Specific Code Quality Improvements
+
+Identify opportunities specific to Z3's architecture and coding patterns:
+
+**Constructor/Destructor Optimization:**
+- Empty/trivial constructors and destructors that can be removed (= default)
+- Missing `noexcept` on non-default constructors and destructors
+- Opportunities to use compiler-generated special members
+
+**Implementation Pattern Improvements:**
+- `m_imp` (implementation pointer) pattern in classes used only within one file
+  - These should use anonymous namespace for implementation classes instead
+  - Look for classes only exported through builder/factory functions
+  - Examples: simplifiers, transformers, local utility classes
+
+**Memory Layout Optimization:**
+- Classes that can be made POD (Plain Old Data)
+- Field reordering to reduce padding and shrink class size
+  - Use `static_assert` and `sizeof` to verify size improvements
+  - Group fields by size (larger types first) for optimal packing
+
+**AST and Expression Optimization:**
+- Redundant AST creation calls (rebuilding same expression multiple times)
+- Opportunities to cache and reuse AST node references
+- Use of temporaries instead of repeated construction
+
+**Hash Table Operations:**
+- Double hash lookups (check existence + insert/retrieve)
+- Opportunities to use single-lookup patterns supported by Z3's hash tables
+- Example: `insert_if_not_there` or equivalent patterns
+
+**Smart Pointer Usage:**
+- Manual deallocation of custom allocator pointers
+- Opportunities to introduce custom smart pointers for automatic cleanup
+- Wrapping allocator-managed objects in RAII wrappers
+
+**Move Semantics:**
+- Places where `std::move` is needed but missing
+- Incorrect usage of `std::move` (moving from const references, etc.)
+- Return value optimization opportunities being blocked
+
+**Optional Value Patterns:**
+- Functions returning null + using output parameters
+- 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
+
+**Bitfield Opportunities:**
+- Structs with multiple boolean flags
+- Small integer fields that could use bitfields
+- Size reduction potential through bitfield packing
+
+**Array Parameter Patterns:**
+- Functions taking pointer + size parameters
+- Replace with `std::span` for type-safe array views
+- Improves API safety and expressiveness
+
+**Increment Operators:**
+- Usage of postfix `i++` where prefix `++i` would suffice
+- Places where the result value isn't used
+- Micro-optimization for iterator-heavy code
+
+**Exception Control Flow:**
+- Using exceptions for normal control flow
+- Alternatives: `std::expected`, `std::optional`, error codes
+- Performance and clarity improvements
 
 ## Analysis Methodology
 
@@ -113,7 +186,9 @@ Look for patterns where Z3 could better leverage standard library features:
    - `src/util/` - Core utilities and data structures
    - `src/ast/` - Abstract syntax tree implementations
    - `src/smt/` - SMT solver core
+   - `src/sat/` - SAT solver components
    - `src/api/` - Public API surface
+   - `src/tactic/` - Tactics and simplifiers (good for m_imp pattern analysis)
    - Use `glob` to find representative source files
 
 2. **Use code search tools** effectively:
@@ -126,11 +201,13 @@ Look for patterns where Z3 could better leverage standard library features:
    - Look at 10-15 representative files per major area
    - Note common patterns vs inconsistencies
    - Check both header (.h) and implementation (.cpp) files
+   - Use `sizeof` and field alignment to analyze struct sizes
 
 4. **Quantify findings**:
    - Count occurrences of specific patterns
    - Identify which areas are most affected
    - Prioritize findings by impact and prevalence
+   - Measure potential size savings for memory layout optimizations
 
 ## Deliverable: Detailed Analysis Discussion
 
@@ -220,7 +297,81 @@ For each opportunity, provide:
 - **Manual Patterns**: [Raw pointers, manual new/delete]
 - **RAII Opportunities**: [Where smart pointers could help]
 
-## 4. Priority Recommendations
+### 3.4 Value Clamping
+- **Current**: [Manual min/max comparisons]
+- **Modern**: [`std::clamp` usage opportunities]
+
+## 4. Z3-Specific Code Quality Opportunities
+
+### 4.1 Constructor/Destructor Optimization
+- **Empty Constructors/Destructors**: [Count of trivial ones that can be removed/defaulted]
+- **Missing noexcept**: [Non-default constructors/destructors without noexcept]
+- **Impact**: [Code size reduction potential]
+
+### 4.2 Implementation Pattern (m_imp) Analysis
+- **Current Usage**: [Files using m_imp pattern for internal-only classes]
+- **Opportunity**: [Classes that could use anonymous namespace instead]
+- **Criteria**: Classes only exported through builder/factory functions
+- **Examples**: [Specific simplifiers, transformers, utility classes]
+
+### 4.3 Memory Layout Optimization
+- **POD Candidates**: [Classes that can be made POD]
+- **Field Reordering**: [Classes with padding that can be reduced]
+- **Size Analysis**: [Use static_assert + sizeof results]
+- **Bitfield Opportunities**: [Structs with bool flags or small integers]
+- **Estimated Savings**: [Total size reduction across codebase]
+
+### 4.4 AST Creation Efficiency
+- **Redundant Creation**: [Examples of rebuilding same expression multiple times]
+- **Temporary Usage**: [Places where temporaries could be cached]
+- **Impact**: [Performance improvement potential]
+
+### 4.5 Hash Table Operation Optimization
+- **Double Lookups**: [Check existence + insert/get patterns]
+- **Single Lookup Pattern**: [How to use Z3's hash table APIs efficiently]
+- **Examples**: [Specific files and patterns]
+- **Performance Impact**: [Lookup reduction potential]
+
+### 4.6 Custom Smart Pointer Opportunities
+- **Manual Deallocation**: [Code manually calling custom allocator free]
+- **RAII Wrapper Needed**: [Where custom smart pointer would help]
+- **Simplification**: [Code that would be cleaner with auto cleanup]
+
+### 4.7 Move Semantics Analysis
+- **Missing std::move**: [Returns/assignments that should use move]
+- **Incorrect std::move**: [Move from const, unnecessary moves]
+- **Return Value Optimization**: [Places where RVO is blocked]
+
+### 4.8 Optional Value Pattern Modernization
+- **Current Pattern**: [Functions returning null + output parameters]
+- **Modern Pattern**: [std::optional<T> return value opportunities]
+- **API Improvements**: [Specific function signatures to update]
+- **Examples**: [File:line references with before/after]
+
+### 4.9 Exception String Construction
+- **Current**: [stringstream usage for building exception messages]
+- **Modern**: [std::format 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.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.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]
+- **Refactoring Opportunities**: [Specific patterns to replace]
+
+## 5. Priority Recommendations
 
 Ranked list of improvements by impact and effort:
 
@@ -231,7 +382,7 @@ Ranked list of improvements by impact and effort:
 
 [Continue ranking...]
 
-## 5. Sample Refactoring Examples
+## 6. Sample Refactoring Examples
 
 Provide 3-5 concrete examples of recommended refactorings:
 
@@ -252,7 +403,7 @@ Provide 3-5 concrete examples of recommended refactorings:
 
 [Repeat for other examples]
 
-## 6. Next Steps
+## 7. Next Steps
 
 - [ ] Review and prioritize these recommendations
 - [ ] Create focused issues for high-priority items
@@ -279,9 +430,14 @@ Provide 3-5 concrete examples of recommended refactorings:
   - Type safety
   - Readability
   - Performance (where measurable)
+  - Binary size (constructor/destructor removal, memory layout)
+  - Memory efficiency (POD classes, field reordering, bitfields)
 - **Be constructive**: Frame findings as opportunities, not criticisms
 - **Quantify when possible**: Use numbers to show prevalence of patterns
 - **Consider backward compatibility**: Z3 is a mature project with many users
+- **Measure size improvements**: Use `static_assert` and `sizeof` to verify memory layout optimizations
+- **Prioritize safety**: Smart pointers, `std::optional`, and `std::span` improve type safety
+- **Consider performance**: Hash table optimizations and AST caching have measurable impact
 
 ## Code Search Examples
 
@@ -310,6 +466,87 @@ grep pattern: "delete |delete\[\]" glob: "src/**/*.cpp"
 grep pattern: "^[ ]*enum [^c]" glob: "src/**/*.h"
 ```
 
+**Find empty/trivial constructors and destructors:**
+```
+grep pattern: "~[A-Za-z_]+\(\)\s*\{\s*\}" glob: "src/**/*.cpp"
+grep pattern: "[A-Za-z_]+\(\)\s*\{\s*\}" glob: "src/**/*.cpp"
+```
+
+**Find constructors/destructors without noexcept:**
+```
+grep pattern: "~[A-Za-z_]+\(\)(?!.*noexcept)" glob: "src/**/*.h"
+grep pattern: "explicit.*\(\)(?!.*noexcept)" glob: "src/**/*.h"
+```
+
+**Find m_imp pattern usage:**
+```
+grep pattern: "m_imp|m_impl" glob: "src/**/*.{h,cpp}"
+grep pattern: "class.*_imp[^a-z]" glob: "src/**/*.cpp"
+```
+
+**Find potential POD struct candidates:**
+```
+grep pattern: "struct [A-Za-z_]+ \{" glob: "src/**/*.h"
+```
+
+**Find potential bitfield opportunities (multiple bools):**
+```
+grep pattern: "bool [a-z_]+;.*bool [a-z_]+;" glob: "src/**/*.h"
+```
+
+**Find redundant AST creation:**
+```
+grep pattern: "mk_[a-z_]+\(.*mk_[a-z_]+\(" glob: "src/**/*.cpp"
+```
+
+**Find double hash lookups:**
+```
+grep pattern: "contains\(.*\).*insert\(|find\(.*\).*insert\(" glob: "src/**/*.cpp"
+```
+
+**Find manual deallocation:**
+```
+grep pattern: "dealloc\(|deallocate\(" glob: "src/**/*.cpp"
+```
+
+**Find missing std::move in returns:**
+```
+grep pattern: "return [a-z_]+;" glob: "src/**/*.cpp"
+```
+
+**Find functions returning null with output parameters:**
+```
+grep pattern: "return.*nullptr.*&" glob: "src/**/*.{h,cpp}"
+grep pattern: "bool.*\(.*\*.*\)|bool.*\(.*&" glob: "src/**/*.h"
+```
+
+**Find stringstream usage for exceptions:**
+```
+grep pattern: "stringstream.*throw|ostringstream.*throw" glob: "src/**/*.cpp"
+```
+
+**Find pointer + size parameters:**
+```
+grep pattern: "\([^,]+\*[^,]*,\s*size_t|, unsigned.*size\)" glob: "src/**/*.h"
+```
+
+**Find postfix increment:**
+```
+grep pattern: "[a-z_]+\+\+\s*[;\)]" glob: "src/**/*.cpp"
+```
+
+**Find std::clamp opportunities:**
+```
+grep pattern: "std::min\(.*std::max\(|std::max\(.*std::min\(" glob: "src/**/*.cpp"
+grep pattern: "if.*<.*\{.*=|if.*>.*\{.*=" glob: "src/**/*.cpp"
+```
+
+**Find exceptions used for control flow:**
+```
+grep pattern: "try.*\{.*for\(|try.*\{.*while\(" glob: "src/**/*.cpp"
+grep pattern: "catch.*continue|catch.*break" glob: "src/**/*.cpp"
+```
+
 ## Security and Safety
 
 - Never execute untrusted code