From 89af9df02d284cde46c9eed0cb5ee958160d235d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Jul 2022 23:22:24 -0700 Subject: [PATCH] add IEnumerable for distinct Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 764beb470..8896904dd 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -938,6 +938,15 @@ namespace Microsoft.Z3 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } + /// + /// Creates a distinct term. + /// + public BoolExpr MkDistinct(IEnumerable args) + { + Debug.Assert(args != null); + return MkDistinct(args.ToArray()); + } + /// /// Mk an expression representing not(a). ///