From ff3c630207886e32451d018f8970b1ff6c90c59f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 9 Aug 2016 16:36:32 +0100 Subject: [PATCH] .NET API: Added MkMul from IEnumerable. --- src/api/dotnet/Context.cs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index cf235b4af..b37dc12d7 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -1055,6 +1055,19 @@ namespace Microsoft.Z3 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } + /// + /// Create an expression representing t[0] * t[1] * .... + /// + public ArithExpr MkMul(IEnumerable t) + { + Contract.Requires(t != null); + Contract.Requires(Contract.ForAll(t, a => a != null)); + Contract.Ensures(Contract.Result() != null); + + CheckContextMatch(t); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t))); + } + /// /// Create an expression representing t[0] - t[1] - .... ///