mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add missing MkSub to NativeContext
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7ded856bb1
commit
7f1893d781
|
@ -100,6 +100,17 @@ namespace Microsoft.Z3
|
|||
return Native.Z3_mk_mul(nCtx, (uint)(ts?.Length ?? 0), ts);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create an expression representing <c>t[0] - t[1] - ...</c>.
|
||||
/// </summary>
|
||||
public Z3_ast MkSub(params Z3_ast[] t)
|
||||
{
|
||||
Debug.Assert(t != null);
|
||||
Debug.Assert(t.All(a => a != IntPtr.Zero));
|
||||
var ts = t.ToArray();
|
||||
return Native.Z3_mk_sub(nCtx, (uint)(ts?.Length ?? 0), ts);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create an expression representing <c>t1 / t2</c>.
|
||||
/// </summary>
|
||||
|
|
Loading…
Reference in a new issue