mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 05:09:02 +00:00
Code Activity

Fix performance issue in MkAnd(IEnumerable) and eliminate code duplication (#7851)

Browse source 
* 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>
This commit is contained in:
Copilot 2025-09-06 19:50:38 -07:00 • committed by GitHub
parent 866393a842
commit 90e610eb23
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/api/dotnet/Context.cs
View file

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