From f936c92efc111639de507def47b5612b7843e98e Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 14 Jun 2018 22:27:57 -0700
Subject: [PATCH] Improve distinct constraint generation

still many more optimizations possible
---
 src/qe/qe_mbi.cpp        | 12 ++++++------
 src/qe/qe_term_graph.cpp | 18 +++++++++++++++++-
 2 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 60fb0f6f0..86fc1ac3c 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -315,10 +315,10 @@ namespace qe {
     }
 
     app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) {
-                arith_util a(m);
-                app_ref_vector avars(m);
-                is_arith_var_proc _proc(avars, m_shared);        
-        for_each_expr(_proc, lits);                
+        arith_util a(m);
+        app_ref_vector avars(m);
+        is_arith_var_proc _proc(avars, m_shared);
+        for_each_expr(_proc, lits);
         return avars;
     }
 
@@ -358,8 +358,8 @@ namespace qe {
             tg.set_vars(m_shared, false);
             tg.add_lits(lits);
             lits.reset();
-            //lits.append(tg.project(*mdl));
-            lits.append(tg.project());
+            lits.append(tg.project(*mdl));
+            //lits.append(tg.project());
             TRACE("qe", tout << "project: " << lits << "\n";);
             return mbi_sat;
         }
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index 95518d7fc..510868366 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -28,6 +28,16 @@ Notes:
 
 namespace qe {
 
+    static expr_ref mk_neq(ast_manager &m, expr *e1, expr *e2) {
+        expr *t = nullptr;
+        // x != !x  == true
+        if ((m.is_not(e1, t) && t == e2) || (m.is_not(e2, t) && t == e1))
+            return expr_ref(m.mk_true(), m);
+        else if (m.are_distinct(e1, e2))
+            return expr_ref(m.mk_true(), m);
+        return expr_ref(m.mk_not(m.mk_eq(e1, e2)), m);
+    }
+
     namespace {
         struct sort_lt_proc {
             bool operator()(const expr* a, const expr *b) const {
@@ -791,10 +801,16 @@ namespace qe {
                 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)
+                if (j - i == 2) {
+                    expr_ref d(m);
+                    d = mk_neq(m, reps.get(i), reps.get(i+1));
+                    if (!m.is_true(d)) res.push_back(d);
+                }
+                else if (j - i > 2)
                     res.push_back(m.mk_distinct(j - i, reps.c_ptr() + i));
                 i = j;
             }
+            TRACE("qe", tout << "after distinct: " << res << "\n";);
         }
 
     public: