From 90e610eb2358a581db606f583a367e803278321c Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 6 Sep 2025 19:50:38 -0700
Subject: [PATCH] Fix performance issue in MkAnd(IEnumerable) and eliminate
 code duplication (#7851)

* Initial plan

* Fix performance issue in MkAnd(IEnumerable<BoolExpr>) method

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

* Refactor IEnumerable methods to call params array variants

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>
---
 src/api/dotnet/Context.cs | 31 ++++++-------------------------
 1 file changed, 6 insertions(+), 25 deletions(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 629e96484..4892ab4ec 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -880,10 +880,7 @@ namespace Microsoft.Z3
         {
             Debug.Assert(f != null);
             Debug.Assert(args == null || args.All(a => a != null));
-
-            CheckContextMatch(f);
-            CheckContextMatch(args);
-            return Expr.Create(this, f, args.ToArray());
+            return MkApp(f, args?.ToArray());
         }
 
         #region Propositional
@@ -1051,10 +1048,7 @@ namespace Microsoft.Z3
         public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
         {
             Debug.Assert(t != null);
-            Debug.Assert(t.All(a => a != null));
-            CheckContextMatch<BoolExpr>(t);
-            var ands = t.ToArray();
-            return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.ArrayToNative(ands)));
+            return MkAnd(t.ToArray());
         }
 
         /// <summary>
@@ -1076,11 +1070,7 @@ namespace Microsoft.Z3
         public BoolExpr MkOr(IEnumerable<BoolExpr> t)
         {
             Debug.Assert(t != null);
-            Debug.Assert(t.All(a => a != null));
-
-            CheckContextMatch(t);
-            var ts = t.ToArray();
-            return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
+            return MkOr(t.ToArray());
         }
 
         #endregion
@@ -1104,11 +1094,7 @@ namespace Microsoft.Z3
         public ArithExpr MkAdd(IEnumerable<ArithExpr> t)
         {
             Debug.Assert(t != null);
-            Debug.Assert(t.All(a => a != null));
-
-            CheckContextMatch(t);
-            var ts = t.ToArray();
-            return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
+            return MkAdd(t.ToArray());
         }
 
         /// <summary>
@@ -1120,8 +1106,7 @@ namespace Microsoft.Z3
             Debug.Assert(t.All(a => a != null));
 
             CheckContextMatch<ArithExpr>(t);
-            var ts = t.ToArray();
-            return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
+            return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
         /// <summary>
@@ -1130,11 +1115,7 @@ namespace Microsoft.Z3
         public ArithExpr MkMul(IEnumerable<ArithExpr> t)
         {
             Debug.Assert(t != null);
-            Debug.Assert(t.All(a => a != null));
-
-            CheckContextMatch<ArithExpr>(t);
-            var ts = t.ToArray();
-            return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
+            return MkMul(t.ToArray());
         }
 
         /// <summary>