[WIP] Refactor AST construction APIs to use std::initializer_list

[Copilot]

Plan: Adopt std::initializer_list for Cleaner AST Construction APIs

Phase 1: Add New std::initializer_list Overloads

• Add mk_add(std::initializer_list<expr*>) to src/ast/arith_decl_plugin.h
• Add mk_mul(std::initializer_list<expr*>) to src/ast/arith_decl_plugin.h
• Add mk_sub(std::initializer_list<expr*>) to src/ast/arith_decl_plugin.h
• Add mk_or(std::initializer_list<expr*>) to src/ast/ast.h
• Add mk_xor(std::initializer_list<expr*>) to src/ast/ast.h
• Add mk_and(std::initializer_list<expr*>) to src/ast/ast.h (delegates to existing std::span overload)

Phase 2: Refactor Existing Overloads to Use initializer_list

• Refactor mk_concat(expr*, expr*) in src/ast/bv_decl_plugin.h to call mk_concat({arg1, arg2})
• Refactor mk_bv_and(expr*, expr*) in src/ast/bv_decl_plugin.h to call mk_bv_and({x, y})
• Refactor mk_bv_or(expr*, expr*) in src/ast/bv_decl_plugin.h to call mk_bv_or({x, y})
• Refactor mk_bv_xor(expr*, expr*) in src/ast/bv_decl_plugin.h to call mk_bv_xor({x, y})
• Refactor mk_band(unsigned, expr*, expr*) in src/ast/arith_decl_plugin.h to call mk_band(n, {arg1, arg2})
• Refactor mk_shl(unsigned, expr*, expr*) in src/ast/arith_decl_plugin.h to call mk_shl(n, {arg1, arg2})
• Refactor mk_ashr(unsigned, expr*, expr*) in src/ast/arith_decl_plugin.h to call mk_ashr(n, {arg1, arg2})
• Refactor mk_lshr(unsigned, expr*, expr*) in src/ast/arith_decl_plugin.h to call mk_lshr(n, {arg1, arg2})
• Refactor mk_or(expr*, expr*, expr*, expr*) in src/ast/ast.h to call mk_or({a, b, c, d})

Phase 3: Build and Test

• Build the code to ensure compilation succeeds
• Run unit tests to verify functionality
• Request code review
• Run CodeQL security checks

Original prompt

---

This section details on the original issue you should resolve

<issue_title>[Conventions] Adopt std::initializer_list for cleaner AST construction APIs</issue_title>
<issue_description>This refactoring modernizes the AST construction APIs by consistently adopting std::initializer_list(expr*) for functions that build expressions with multiple arguments.

Summary of Changes

1. Added std::initializer_list Overloads

Added modern initializer_list overloads to the following functions:

Arithmetic operations (src/ast/arith_decl_plugin.h):

• mk_add(std::initializer_list(expr*)) - Line 477
• mk_mul(std::initializer_list(expr*)) - Line 489
• mk_sub(std::initializer_list(expr*)) - Line 484

Boolean operations (src/ast/ast.h):

• mk_or(std::initializer_list(expr*)) - Line 2208
• mk_xor(std::initializer_list(expr*)) - Line 2204
• mk_and(std::initializer_list(expr*)) - Line 2211 (delegates to existing std::span overload)

2. Refactored Existing Overloads to Use initializer_list

Eliminated temporary array creation in convenience overloads by delegating to initializer_list versions:

Bitvector operations (src/ast/bv_decl_plugin.h):

• mk_concat(expr*, expr*) - Now calls mk_concat({arg1, arg2})
• mk_bv_and(expr*, expr*) - Now calls mk_bv_and({x, y})
• mk_bv_or(expr*, expr*) - Now calls mk_bv_or({x, y})
• mk_bv_xor(expr*, expr*) - Now calls mk_bv_xor({x, y})

Arithmetic bitwise operations (src/ast/arith_decl_plugin.h):

• mk_band(unsigned, expr*, expr*) - Now calls mk_band(n, {arg1, arg2})
• mk_shl(unsigned, expr*, expr*) - Now calls mk_shl(n, {arg1, arg2})
• mk_ashr(unsigned, expr*, expr*) - Now calls mk_ashr(n, {arg1, arg2})
• mk_lshr(unsigned, expr*, expr*) - Now calls mk_lshr(n, {arg1, arg2})

Boolean operations (src/ast/ast.h):

• mk_or(expr*, expr*, expr*, expr*) - Now calls mk_or({a, b, c, d})

Benefits

1. Cleaner call sites - Future code can use brace-initialization:

   // Before:
   expr* args[3] = { a, b, c };
   m.mk_add(3, args);
   
   // After:
   m.mk_add({a, b, c});

2. Type safety - Size is implicit in initializer_list, eliminating potential size/pointer mismatches

3. Reduced code size - Eliminated 8 inline temporary array declarations in the API headers

4. Consistent API pattern - Matches existing initializer_list overloads (mk_concat, mk_bv_or/and/xor already had them)

5. Zero overhead - std::initializer_list has same performance as array+size, just cleaner syntax

6. Modern C++ idiom - Uses C++11 standard library feature for cleaner, more expressive code

API Compatibility

• Fully backward compatible - All existing array+size overloads remain unchanged
• No breaking changes - Only adds new overloads and refactors internal implementations
• Overload resolution - Compiler selects initializer_list for brace-initialized arguments, array+size for existing code

Files Modified

• src/ast/arith_decl_plugin.h - 7 changes (3 new overloads, 4 refactored)
• src/ast/bv_decl_plugin.h - 4 changes (all refactored)
• src/ast/ast.h - 4 changes (3 new overloads, 1 refactored)

Total: 15 function changes across 3 header files

Example Usage

Future call sites can now use:

// Arithmetic
auto* sum = arith.mk_add({a, b, c});
auto* prod = arith.mk_mul({x, y, z});

// Boolean  
auto* conjunction = m.mk_and({p, q, r});
auto* disjunction = m.mk_or({p, q, r, s});

// Bitvector
auto* bv_concat = bv.mk_concat({bv1, bv2, bv3});
auto* bv_and = bv.mk_bv_and({x, y, z});

Testing

• No functional changes - all implementations delegate to existing array+size functions
• Existing tests cover all functionality
• New overloads use same code paths as container adapter overloads (ptr_vector, ref_vector, etc.)

Related Work

This continues the modernization pattern established in previous work:

• mk_concat, mk_bv_or, mk_bv_and, mk_bv_xor already had initializer_list overloads (lines 503, 509, 511, 513 in bv_decl_plugin.h)
• mk_and has std::span overload (modern alternative, line 2210 in ast.h)
• This change completes the pattern across arithmetic and boolean operations

AI generated by Code Conventions Analyzer

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

• Fixes [Conventions] Adopt std::initializer_list for cleaner AST construction APIs #8511

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.