The MkAnd(IEnumerable<BoolExpr> t) method in Context.cs had significant performance issues due to multiple redundant enumerations of the input collection:

1. t.All(a => a != null) - First enumeration to check for nulls
2. CheckContextMatch<BoolExpr>(t) - Second enumeration for context validation
3. t.ToArray() - Third enumeration to create array
4. t.Count() - Fourth enumeration to get count after array was already created

This was particularly problematic when calling MkAnd with large collections, as each enumeration has O(n) complexity.

Changes Made

Performance Fix

• Convert to array once with t.ToArray() (single enumeration)
• Use ands.Length instead of t.Count() to eliminate redundant enumeration
• Use array-based CheckContextMatch((Z3Object[])ands) for efficiency
• Move null check to operate on array instead of original enumerable

Code Duplication Elimination

Following feedback to eliminate duplicated functionality, refactored all IEnumerable methods to delegate to their corresponding params array variants:

• MkAnd(IEnumerable<BoolExpr>) → calls MkAnd(params BoolExpr[])
• MkOr(IEnumerable<BoolExpr>) → calls MkOr(params BoolExpr[])
• MkAdd(IEnumerable<ArithExpr>) → calls MkAdd(params ArithExpr[])
• MkMul(IEnumerable<ArithExpr>) → calls MkMul(params ArithExpr[])
• MkApp(FuncDecl, IEnumerable<Expr>) → calls MkApp(FuncDecl, params Expr[])

Before:

public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
{
    Debug.Assert(t != null);
    Debug.Assert(t.All(a => a != null));           // 1st enumeration
    CheckContextMatch<BoolExpr>(t);                 // 2nd enumeration  
    var ands = t.ToArray();                         // 3rd enumeration
    return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.ArrayToNative(ands))); // 4th enumeration
}

After:

public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
{
    Debug.Assert(t != null);
    return MkAnd(t.ToArray());                      // Single enumeration, delegates to params version
}

This approach:

• Reduces the method from 4 enumerations to 1 enumeration
• Eliminates code duplication between IEnumerable and params array variants
• Ensures consistent validation logic across all method variants
• Follows the same delegation pattern already used by MkDistinct
• Preserves identical validation behavior and functionality

Testing

• All existing Z3 unit tests pass
• .NET assembly builds successfully
• Performance test with 5000 expressions completes efficiently
• Solver integration confirms results remain valid
• Comprehensive verification of delegation pattern implementation

Fixes #7850.

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.