mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

.NET API: Added MkMul from IEnumerable.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-08-09 16:36:32 +01:00
parent 03aa6914a3
commit ff3c630207
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1055,6 +1055,19 @@ namespace Microsoft.Z3
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)t.Length, AST.ArrayToNative(t)));
} }
/// <summary>
/// Create an expression representing <c>t[0] * t[1] * ...</c>.
/// </summary>
public ArithExpr MkMul(IEnumerable<ArithExpr> t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<ArithExpr>() != null);
CheckContextMatch(t);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
}
/// <summary> /// <summary>
/// Create an expression representing <c>t[0] - t[1] - ...</c>. /// Create an expression representing <c>t[0] - t[1] - ...</c>.
/// </summary> /// </summary>