From 87715620d943186b1306d49ab30fbb7f7668257e Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 14 Jun 2018 16:02:19 -0700
Subject: [PATCH] Fix mk_distict in term_graph

---
 src/qe/qe_term_graph.cpp | 31 ++++++++++++++++++++++++++-----
 1 file changed, 26 insertions(+), 5 deletions(-)

diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index f12d51b9d..0f1f75b39 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -28,6 +28,13 @@ Notes:
 
 namespace qe {
 
+    namespace {
+        struct sort_lt_proc {
+            bool operator()(const expr* a, const expr *b) const {
+                return get_sort(a)->get_id() < get_sort(b)->get_id();
+            }
+        };
+    }
     namespace is_pure_ns {
         struct found{};
         struct proc {
@@ -760,15 +767,29 @@ namespace qe {
                     val2rep.insert(val, rep);
                 }
             }
-            // TBD: this ignores types, need one use of 'distinct' per sort.
-            // TBD: probably ignore distinct on values
             // TBD: ignore distinct on Booleans
             ptr_buffer<expr> reps;
             for (auto &kv : val2rep) {
-                reps.push_back(kv.m_value);
-                std::cout << mk_pp(kv.m_value, m) << "\n";
+                expr *val = kv.m_value;
+                if (!m.is_unique_value(val))
+                    reps.push_back(kv.m_value);
+            }
+
+            if (reps.size() <= 1) return;
+
+            // -- sort representatives, call mk_distinct on any range
+            // -- of the same sort longer than 1
+            std::sort(reps.c_ptr(), reps.c_ptr() + reps.size(), sort_lt_proc());
+            unsigned i = 0;
+            unsigned sz = res.size();
+            while (i < sz) {
+                sort* last_sort = get_sort(reps.get(i));
+                unsigned j = i + 1;
+                while (j < sz && last_sort == get_sort(reps.get(j))) {++j;}
+                if (j - i > 1)
+                    res.push_back(m.mk_distinct(j - i, reps.c_ptr() + i));
+                i = j;
             }
-            // res.push_back(m.mk_distinct(reps.size(), reps.c_ptr()));
         }
 
     public: