From 620c11932b10d5218069668c2ef766ffe7c6b84f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@hotmail.com>
Date: Mon, 27 Apr 2015 11:10:37 -0700
Subject: [PATCH] type check distinct operator. fixes #62

Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
---
 src/ast/ast.cpp  | 11 +++++++++++
 src/ast/ast.h    |  2 +-
 src/test/api.cpp |  3 ++-
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 6780145d9..3a6275e33 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1043,6 +1043,13 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_DISTINCT: {
         func_decl_info info(m_family_id, OP_DISTINCT);
         info.set_pairwise();
+        for (unsigned i = 1; i < arity; i++) {        
+            if (domain[i] != domain[0]) {
+                std::ostringstream buffer;
+                buffer << "Sort mismatch between first argument and argument " << (i+1);
+                throw ast_exception(buffer.str().c_str());
+            }
+        }
         return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info);
     }
     default:
@@ -2338,6 +2345,10 @@ quantifier * ast_manager::update_quantifier(quantifier * q, bool is_forall, unsi
                          num_patterns == 0 ? q->get_no_patterns() : 0);
 }
 
+app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) {
+    return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args);
+}
+
 app * ast_manager::mk_distinct_expanded(unsigned num_args, expr * const * args) {
     if (num_args < 2)
         return mk_true();
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 93f456965..a5f5c286f 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2000,7 +2000,7 @@ public:
     app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); }
     app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); }
     app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); }
-    app * mk_distinct(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args); }
+    app * mk_distinct(unsigned num_args, expr * const * args);
     app * mk_distinct_expanded(unsigned num_args, expr * const * args);
     app * mk_true() { return m_true; }
     app * mk_false() { return m_false; }
diff --git a/src/test/api.cpp b/src/test/api.cpp
index 6230528a1..234d1192c 100644
--- a/src/test/api.cpp
+++ b/src/test/api.cpp
@@ -460,8 +460,9 @@ static void test_mk_distinct() {
   Z3_sort bv8 = Z3_mk_bv_sort(ctx, 8);
   Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32);
   Z3_ast args[] = { Z3_mk_int64(ctx, 0, bv8), Z3_mk_int64(ctx, 0, bv32) };
-  Z3_mk_distinct(ctx, 2, args);
+  Z3_ast d = Z3_mk_distinct(ctx, 2, args);
   SASSERT(cb_called);
+  
 }
 
 void tst_api() {