[WIP] Refactor mk_or and mk_and helpers to use std::initializer_list

[Copilot]

Refactor mk_or and mk_and helpers to use std::initializer_list

Plan:

• Explore repository structure and understand current implementation
• Add #include <initializer_list> to ast.h
• Refactor 4-arg mk_or to use initializer_list in ast.h (line 2213)
  • Note: Kept original 4-arg version for backward compatibility
  • Added new initializer_list version for cleaner call sites
• Refactor mk_and helper to use initializer_list in ast_util.h (line 106)
• Refactor mk_or helper to use initializer_list in ast_util.h (line 128)
• Update mk_or to use std::span in ast_util.cpp (line 180)
• Build the code to ensure no compilation errors (build successful!)
• Run basic tests to verify functionality
• Run code review
• Run security checks with CodeQL

Original prompt

---

This section details on the original issue you should resolve

<issue_title>[Conventions] Refactor mk_or and mk_and helpers to use std::initializer_list</issue_title>
<issue_description>## Summary

This refactoring modernizes several AST construction APIs to use std::initializer_list(expr*) instead of temporary array declarations, resulting in cleaner call sites and improved type safety.

Changes Made

1. Added std::initializer_list include to ast.h

#include (span)
#include (initializer_list)

2. Refactored 4-arg mk_or to use initializer_list (ast.h)

Before:

app * mk_or(expr* a, expr* b, expr* c, expr* d) { 
    expr* args[4] = { a, b, c, d }; 
    return mk_app(basic_family_id, OP_OR, 4, args); 
}

After:

app * mk_or(std::initializer_list(expr*) args) { 
    return mk_app(basic_family_id, OP_OR, static_cast(unsigned)(args.size()), args.begin()); 
}

3. Refactored mk_and helper to use initializer_list (ast_util.h)

Before:

inline expr * mk_and(ast_manager & m, expr* a, expr* b) { 
    expr* args[2] = { a, b }; 
    return mk_and(m, 2, args); 
}

After:

inline expr * mk_and(ast_manager & m, std::initializer_list(expr*) args) { 
    return mk_and(m, static_cast(unsigned)(args.size()), args.begin()); 
}

4. Refactored mk_or helper to use initializer_list (ast_util.h)

Before:

inline expr * mk_or(ast_manager & m, expr* a, expr* b) { 
    expr* args[2] = { a, b }; 
    return mk_or(m, 2, args); 
}

After:

inline expr * mk_or(ast_manager & m, std::initializer_list(expr*) args) { 
    return mk_or(m, static_cast(unsigned)(args.size()), args.begin()); 
}

5. Updated mk_or to use std::span for consistency (ast_util.cpp)

Before:

return m.mk_or(num_args, args);

After:

return m.mk_or(std::span(expr* const)(args, num_args));

This matches the existing pattern used in mk_and (line 167), ensuring API consistency.

Benefits

1. Cleaner call sites: No need to create temporary arrays

   • Before: expr* args[4] = {a, b, c, d}; m.mk_or(4, args);
   • After: m.mk_or({a, b, c, d});

2. Type safety: Size is implicit, no mismatch possible

   • The compiler enforces correct size based on brace-init list

3. Modern C++ idiom: std::initializer_list is C++11 standard

   • Aligns with Z3's C++20 compilation target

4. Zero overhead: Compilers optimize initializer_list to same code as array

   • No runtime performance impact

5. API consistency: mk_or now uses std::span matching mk_and

   • Unified approach across similar functions

Files Modified

• src/ast/ast.h - Added initializer_list include and mk_or overload
• src/ast/ast_util.h - Refactored mk_and and mk_or helpers
• src/ast/ast_util.cpp - Updated mk_or to use std::span

Backward Compatibility

• Existing code using 2-arg, 3-arg forms continues to work unchanged
• The variadic mk_or now accepts any number of arguments via brace-initialization
• All existing overloads (span, vector, buffer) remain available

Call Site Improvements

This refactoring enables cleaner code at call sites:

// Example from bool_rewriter.cpp (lines 783-787)
// Can now be written more concisely:
args.push_back(m().mk_or({c1, c2, m().mk_eq(e1, e2)}));
args.push_back(m().mk_or({nc1, nc2, m().mk_eq(t1, t2)}));
args.push_back(m().mk_or({nc1, c2, m().mk_eq(t1, e2)}));
args.push_back(m().mk_or({c1, nc2, m().mk_eq(e1, t2)}));

Testing

• No functional changes to logic
• All existing call sites continue to work
• New overload provides additional convenience

Related Work

This continues the modernization effort from previous PRs:

• std::span adoption for mk_or and mk_and (merged)
• std::initializer_list for mk_concat and arithmetic operations (merged)
• Consistent container adapters across AST construction APIs

AI generated by Code Conventions Analyzer

Comments on the Issue (you are @copilot in this section)

• Fixes [Conventions] Refactor mk_or and mk_and helpers to use std::initializer_list #8523

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.