From 4c95bb4dd901f0ba33d025538233c6598b165554 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 28 Mar 2014 08:51:50 -0700
Subject: [PATCH] add 'distinct' to C++ API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/c++/z3++.h        | 12 ++++++++++++
 src/api/dotnet/Context.cs |  2 ++
 src/api/dotnet/Expr.cs    |  1 +
 3 files changed, 15 insertions(+)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index c75acc5e2..8f228cdba 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -652,6 +652,8 @@ namespace z3 {
             return expr(c.ctx(), r);
         }
 
+        friend expr distinct(expr_vector const& args);
+
         friend expr operator==(expr const & a, expr const & b) {
             check_context(a, b);
             Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
@@ -1065,6 +1067,16 @@ namespace z3 {
         array<Z3_app> vars(xs);  
         Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
     }
+
+
+    inline expr distinct(expr_vector const& args) {
+        assert(args.size() > 0);
+        context& ctx = args[0].ctx();
+        array<Z3_ast> _args(args);
+        Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
+        ctx.check_error();
+        return expr(ctx, r);
+    }
     
     class func_entry : public object {
         Z3_func_entry m_entry;
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index ae8b233d1..47294244a 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -916,6 +916,8 @@ namespace Microsoft.Z3
             CheckContextMatch(t);
             return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
+
+
         #endregion
 
         #region Arithmetic
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index b2927e2c3..49b46edeb 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -320,6 +320,7 @@ namespace Microsoft.Z3
         /// Indicates whether the term is an implication
         /// </summary>
         public bool IsImplies { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
+
         #endregion
 
         #region Arithmetic Terms