From b2acbaa0c9fec4720d68b775edac432e63fd774e Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 7 Sep 2025 16:43:13 -0700 Subject: [PATCH] Fix .NET performance issues by reducing multiple enumerations in constraint methods (#7854) * Initial plan * Fix .NET performance issues by reducing multiple enumerations in constraint methods Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Refactor MkApp and related methods for null checks * Update null checks for MkApp method arguments * Fix assertion condition for MkApp method --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 84 ++++++++++++++++++--------------------- 1 file changed, 39 insertions(+), 45 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 4892ab4ec..9293b1a31 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -867,7 +867,6 @@ 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); @@ -879,7 +878,6 @@ namespace Microsoft.Z3 public Expr MkApp(FuncDecl f, IEnumerable args) { Debug.Assert(f != null); - Debug.Assert(args == null || args.All(a => a != null)); return MkApp(f, args?.ToArray()); } @@ -889,7 +887,6 @@ namespace Microsoft.Z3 /// public BoolExpr MkTrue() { - return new BoolExpr(this, Native.Z3_mk_true(nCtx)); } @@ -898,7 +895,6 @@ namespace Microsoft.Z3 /// public BoolExpr MkFalse() { - return new BoolExpr(this, Native.Z3_mk_false(nCtx)); } @@ -907,7 +903,6 @@ namespace Microsoft.Z3 /// public BoolExpr MkBool(bool value) { - return value ? MkTrue() : MkFalse(); } @@ -932,7 +927,6 @@ namespace Microsoft.Z3 Debug.Assert(args != null); Debug.Assert(args.All(a => a != null)); - CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -952,7 +946,6 @@ namespace Microsoft.Z3 public BoolExpr MkNot(BoolExpr a) { Debug.Assert(a != null); - CheckContextMatch(a); return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject)); } @@ -1017,9 +1010,10 @@ namespace Microsoft.Z3 /// /// Create an expression representing t1 xor t2 xor t3 ... . /// - public BoolExpr MkXor(IEnumerable ts) + public BoolExpr MkXor(IEnumerable args) { - Debug.Assert(ts != null); + Debug.Assert(args != null); + var ts = args.ToArray(); Debug.Assert(ts.All(a => a != null)); CheckContextMatch(ts); @@ -1033,13 +1027,13 @@ namespace Microsoft.Z3 /// /// Create an expression representing t[0] and t[1] and .... /// - public BoolExpr MkAnd(params BoolExpr[] t) + public BoolExpr MkAnd(params BoolExpr[] ts) { - Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); + Debug.Assert(ts != null); + Debug.Assert(ts.All(a => a != null)); - CheckContextMatch(t); - return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t))); + CheckContextMatch(ts); + return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// @@ -1054,23 +1048,23 @@ namespace Microsoft.Z3 /// /// Create an expression representing t[0] or t[1] or .... /// - public BoolExpr MkOr(params BoolExpr[] t) + public BoolExpr MkOr(params BoolExpr[] ts) { - Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); + Debug.Assert(ts != null); + Debug.Assert(ts.All(a => a != null)); - CheckContextMatch(t); - return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t))); + CheckContextMatch(ts); + return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// /// Create an expression representing t[0] or t[1] or .... /// - public BoolExpr MkOr(IEnumerable t) + public BoolExpr MkOr(IEnumerable ts) { - Debug.Assert(t != null); - return MkOr(t.ToArray()); + Debug.Assert(ts != null); + return MkOr(ts.ToArray()); } #endregion @@ -1079,55 +1073,55 @@ namespace Microsoft.Z3 /// /// Create an expression representing t[0] + t[1] + .... /// - public ArithExpr MkAdd(params ArithExpr[] t) + public ArithExpr MkAdd(params ArithExpr[] ts) { - Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); + Debug.Assert(ts != null); + Debug.Assert(ts.All(a => a != null)); - CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t))); + CheckContextMatch(ts); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// /// Create an expression representing t[0] + t[1] + .... /// - public ArithExpr MkAdd(IEnumerable t) + public ArithExpr MkAdd(IEnumerable ts) { - Debug.Assert(t != null); - return MkAdd(t.ToArray()); + Debug.Assert(ts != null); + return MkAdd(ts.ToArray()); } /// /// Create an expression representing t[0] * t[1] * .... /// - public ArithExpr MkMul(params ArithExpr[] t) + public ArithExpr MkMul(params ArithExpr[] ts) { - Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); + Debug.Assert(ts != null); + Debug.Assert(ts.All(a => a != null)); - CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); + CheckContextMatch(ts); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// /// Create an expression representing t[0] * t[1] * .... /// - public ArithExpr MkMul(IEnumerable t) + public ArithExpr MkMul(IEnumerable ts) { - Debug.Assert(t != null); - return MkMul(t.ToArray()); + Debug.Assert(ts != null); + return MkMul(ts.ToArray()); } /// /// Create an expression representing t[0] - t[1] - .... /// - public ArithExpr MkSub(params ArithExpr[] t) + public ArithExpr MkSub(params ArithExpr[] ts) { - Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); + Debug.Assert(ts != null); + Debug.Assert(ts.All(a => a != null)); - CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t))); + CheckContextMatch(ts); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// @@ -2824,8 +2818,8 @@ namespace Microsoft.Z3 public BoolExpr MkAtMost(IEnumerable args, uint k) { Debug.Assert(args != null); - CheckContextMatch(args); var ts = args.ToArray(); + CheckContextMatch(ts); return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length, AST.ArrayToNative(ts), k)); } @@ -2836,8 +2830,8 @@ namespace Microsoft.Z3 public BoolExpr MkAtLeast(IEnumerable args, uint k) { Debug.Assert(args != null); - CheckContextMatch(args); var ts = args.ToArray(); + CheckContextMatch(ts); return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length, AST.ArrayToNative(ts), k)); }