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

Fix .NET performance issues by reducing multiple enumerations in constraint methods (#7854)

Browse source 
* 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 <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2025-09-07 16:43:13 -07:00 • committed by GitHub
parent a7eed2a9f3
commit b2acbaa0c9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 39 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -867,7 +867,6 @@ 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));
CheckContextMatch(f); CheckContextMatch(f);
CheckContextMatch<Expr>(args); CheckContextMatch<Expr>(args);
return Expr.Create(this, f, args); return Expr.Create(this, f, args);
@ -879,7 +878,6 @@ namespace Microsoft.Z3
public Expr MkApp(FuncDecl f, IEnumerable<Expr> args) public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
{ {
Debug.Assert(f != null); Debug.Assert(f != null);
Debug.Assert(args == null || args.All(a => a != null));
return MkApp(f, args?.ToArray()); return MkApp(f, args?.ToArray());
} }
@ -889,7 +887,6 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public BoolExpr MkTrue() public BoolExpr MkTrue()
{ {
return new BoolExpr(this, Native.Z3_mk_true(nCtx)); return new BoolExpr(this, Native.Z3_mk_true(nCtx));
} }
@ -898,7 +895,6 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public BoolExpr MkFalse() public BoolExpr MkFalse()
{ {
return new BoolExpr(this, Native.Z3_mk_false(nCtx)); return new BoolExpr(this, Native.Z3_mk_false(nCtx));
} }
@ -907,7 +903,6 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public BoolExpr MkBool(bool value) public BoolExpr MkBool(bool value)
{ {
return value ? MkTrue() : MkFalse(); return value ? MkTrue() : MkFalse();
} }
@ -932,7 +927,6 @@ namespace Microsoft.Z3
Debug.Assert(args != null); Debug.Assert(args != null);
Debug.Assert(args.All(a => a != null)); Debug.Assert(args.All(a => a != null));
CheckContextMatch<Expr>(args); CheckContextMatch<Expr>(args);
return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(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) public BoolExpr MkNot(BoolExpr a)
{ {
Debug.Assert(a != null); Debug.Assert(a != null);
CheckContextMatch(a); CheckContextMatch(a);
return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject)); return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
} }
@ -1017,9 +1010,10 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create an expression representing <c>t1 xor t2 xor t3 ... </c>. /// Create an expression representing <c>t1 xor t2 xor t3 ... </c>.
/// </summary> /// </summary>
public BoolExpr MkXor(IEnumerable<BoolExpr> ts) public BoolExpr MkXor(IEnumerable<BoolExpr> args)
{ {
Debug.Assert(ts != null); Debug.Assert(args != null);
var ts = args.ToArray();
Debug.Assert(ts.All(a => a != null)); Debug.Assert(ts.All(a => a != null));
CheckContextMatch<BoolExpr>(ts); CheckContextMatch<BoolExpr>(ts);
@ -1033,13 +1027,13 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] and t[1] and ...</c>. /// Create an expression representing <c>t[0] and t[1] and ...</c>.
/// </summary> /// </summary>
public BoolExpr MkAnd(params BoolExpr[] t) public BoolExpr MkAnd(params BoolExpr[] ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
Debug.Assert(t.All(a => a != null)); Debug.Assert(ts.All(a => a != null));
CheckContextMatch<BoolExpr>(t); CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t))); return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
} }
/// <summary> /// <summary>
@ -1054,23 +1048,23 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] or t[1] or ...</c>. /// Create an expression representing <c>t[0] or t[1] or ...</c>.
/// </summary> /// </summary>
public BoolExpr MkOr(params BoolExpr[] t) public BoolExpr MkOr(params BoolExpr[] ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
Debug.Assert(t.All(a => a != null)); Debug.Assert(ts.All(a => a != null));
CheckContextMatch<BoolExpr>(t); CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t))); return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
} }
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] or t[1] or ...</c>. /// Create an expression representing <c>t[0] or t[1] or ...</c>.
/// </summary> /// </summary>
public BoolExpr MkOr(IEnumerable<BoolExpr> t) public BoolExpr MkOr(IEnumerable<BoolExpr> ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
return MkOr(t.ToArray()); return MkOr(ts.ToArray());
} }
#endregion #endregion
@ -1079,55 +1073,55 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] + t[1] + ...</c>. /// Create an expression representing <c>t[0] + t[1] + ...</c>.
/// </summary> /// </summary>
public ArithExpr MkAdd(params ArithExpr[] t) public ArithExpr MkAdd(params ArithExpr[] ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
Debug.Assert(t.All(a => a != null)); Debug.Assert(ts.All(a => a != null));
CheckContextMatch<ArithExpr>(t); CheckContextMatch<ArithExpr>(ts);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t))); return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
} }
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] + t[1] + ...</c>. /// Create an expression representing <c>t[0] + t[1] + ...</c>.
/// </summary> /// </summary>
public ArithExpr MkAdd(IEnumerable<ArithExpr> t) public ArithExpr MkAdd(IEnumerable<ArithExpr> ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
return MkAdd(t.ToArray()); return MkAdd(ts.ToArray());
} }
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] * t[1] * ...</c>. /// Create an expression representing <c>t[0] * t[1] * ...</c>.
/// </summary> /// </summary>
public ArithExpr MkMul(params ArithExpr[] t) public ArithExpr MkMul(params ArithExpr[] ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
Debug.Assert(t.All(a => a != null)); Debug.Assert(ts.All(a => a != null));
CheckContextMatch<ArithExpr>(t); CheckContextMatch<ArithExpr>(ts);
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>
/// Create an expression representing <c>t[0] * t[1] * ...</c>. /// Create an expression representing <c>t[0] * t[1] * ...</c>.
/// </summary> /// </summary>
public ArithExpr MkMul(IEnumerable<ArithExpr> t) public ArithExpr MkMul(IEnumerable<ArithExpr> ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
return MkMul(t.ToArray()); return MkMul(ts.ToArray());
} }
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] - t[1] - ...</c>. /// Create an expression representing <c>t[0] - t[1] - ...</c>.
/// </summary> /// </summary>
public ArithExpr MkSub(params ArithExpr[] t) public ArithExpr MkSub(params ArithExpr[] ts)
{ {
Debug.Assert(t != null); Debug.Assert(ts != null);
Debug.Assert(t.All(a => a != null)); Debug.Assert(ts.All(a => a != null));
CheckContextMatch<ArithExpr>(t); CheckContextMatch<ArithExpr>(ts);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t))); return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
} }
/// <summary> /// <summary>
@ -2824,8 +2818,8 @@ namespace Microsoft.Z3
public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k) public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k)
{ {
Debug.Assert(args != null); Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray(); var ts = args.ToArray();
CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length, return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length,
AST.ArrayToNative(ts), k)); AST.ArrayToNative(ts), k));
} }
@ -2836,8 +2830,8 @@ namespace Microsoft.Z3
public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k) public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k)
{ {
Debug.Assert(args != null); Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray(); var ts = args.ToArray();
CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length, return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length,
AST.ArrayToNative(ts), k)); AST.ArrayToNative(ts), k));
} }