mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

remove EnumToNative as it drops reference counts, fixes #5713

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-16 03:22:54 -08:00
parent 2be93870c8
commit 2caa7e6e45
2 changed files with 21 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -980,7 +980,8 @@ namespace Microsoft.Z3
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
CheckContextMatch<BoolExpr>(t);
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
var ands = t.ToArray();
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.ArrayToNative(ands)));
}
/// <summary>
@ -1005,7 +1006,8 @@ namespace Microsoft.Z3
Debug.Assert(t.All(a => a != null));
CheckContextMatch(t);
return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
var ts = t.ToArray();
return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
#endregion
@ -1032,7 +1034,8 @@ namespace Microsoft.Z3
Debug.Assert(t.All(a => a != null));
CheckContextMatch(t);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
var ts = t.ToArray();
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
@ -1044,7 +1047,8 @@ namespace Microsoft.Z3
Debug.Assert(t.All(a => a != null));
CheckContextMatch<ArithExpr>(t);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
var ts = t.ToArray();
return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
@ -1056,7 +1060,8 @@ namespace Microsoft.Z3
Debug.Assert(t.All(a => a != null));
CheckContextMatch<ArithExpr>(t);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
var ts = t.ToArray();
return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
@ -2749,10 +2754,11 @@ namespace Microsoft.Z3
/// </summary>
public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k)
{
Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Count(),
AST.EnumToNative(args), k));
Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray();
return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) ts.Length,
AST.ArrayToNative(ts), k));
}
/// <summary>
@ -2760,10 +2766,11 @@ namespace Microsoft.Z3
/// </summary>
public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k)
{
Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Count(),
AST.EnumToNative(args), k));
Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray();
return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) ts.Length,
AST.ArrayToNative(ts), k));
}
/// <summary>

16
src/api/dotnet/Z3Object.cs
View file

@ -131,24 +131,10 @@ namespace Microsoft.Z3
return an;
}
internal static IntPtr[] EnumToNative<T>(IEnumerable<T> a) where T : Z3Object
{
if (a == null) return null;
IntPtr[] an = new IntPtr[a.Count()];
int i = 0;
foreach (var ai in a)
{
if (ai != null) an[i] = ai.NativeObject;
++i;
}
return an;
}
internal static uint ArrayLength(Z3Object[] a)
{
return (a == null)?0:(uint)a.Length;
}
#endregion
#endregion
}
}