From 0b20a4ebf4b8e3e0188ccbb5dad9b51a88966f04 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Sat, 9 Apr 2022 21:46:21 +0200
Subject: [PATCH] Added rewriting distinct with bitvectors to false if bit-size
 is too low (#5956)

* Fixed problem with registering bitvector functions

* Added rewriting distinct with bitvectors to false if bit-size is too low

* Removed debug output

* Incorporated Nikolaj's comments

* Simplifications
---
 src/ast/rewriter/bv_rewriter.cpp | 15 +++++++++++++++
 src/ast/rewriter/bv_rewriter.h   |  3 ++-
 src/ast/rewriter/th_rewriter.cpp | 20 +++++++++++---------
 3 files changed, 28 insertions(+), 10 deletions(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 073885c21..1fdd7bd14 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2803,6 +2803,21 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu
     return BR_FAILED;
 }
 
+br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
+    if (num_args <= 1) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    unsigned sz = get_bv_size(args[0]);
+    // check if num_args > 2^sz
+    if (sz >= 32) 
+        return BR_FAILED;
+    if (num_args <= 1u << sz)
+        return BR_FAILED;
+    result = m().mk_false();
+    return BR_DONE;     
+}
+
 br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result) {
     SASSERT(num == 2);
     unsigned bv_sz;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 7f0c67540..88d952c06 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -180,7 +180,8 @@ public:
 
     bool is_urem_any(expr * e, expr * & dividend,  expr * & divisor);
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
-    br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resul);
+    br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
+    br_status mk_distinct(unsigned num_args, expr * const * args, expr_ref & result);
 
     bool hi_div0() const { return m_hi_div0; }
 
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 22d6a83b7..9cf9fc810 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -60,7 +60,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     expr_substitution * m_subst = nullptr;
     unsigned long long  m_max_memory; // in bytes
     bool                m_new_subst = false;
-    unsigned            m_max_steps = UINT_MAX;    
+    unsigned            m_max_steps = UINT_MAX;
     bool                m_pull_cheap_ite = true;
     bool                m_flat = true;
     bool                m_cache_all = false;
@@ -180,7 +180,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 // theory dispatch for =
                 SASSERT(num == 2);
                 family_id s_fid = args[0]->get_sort()->get_family_id();
-                if (s_fid == m_a_rw.get_fid()) 
+                if (s_fid == m_a_rw.get_fid())
                     st = m_a_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_bv_rw.get_fid())
                     st = m_bv_rw.mk_eq_core(args[0], args[1], result);
@@ -193,10 +193,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 else if (s_fid == m_seq_rw.get_fid())
                     st = m_seq_rw.mk_eq_core(args[0], args[1], result);
                 if (st != BR_FAILED)
-                    return st;     
-            }
-            if (k == OP_EQ) {
-                SASSERT(num == 2);
+                    return st;
                 st = apply_tamagotchi(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;
@@ -210,16 +207,21 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                     return st;
             }
             if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
-                st = m_seq_rw.mk_bool_app(f, num, args, result); 
+                st = m_seq_rw.mk_bool_app(f, num, args, result);
                 if (st != BR_FAILED)
                     return st;
             }
-            if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) && 
+            if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
                 to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
                 st = m_seq_rw.mk_eq_core(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;
             }
+            if (k == OP_DISTINCT && num > 0 && m_bv_rw.is_bv(args[0])) {
+               st = m_bv_rw.mk_distinct(num, args, result);
+               if (st != BR_FAILED)
+                    return st;
+            }
 
             return m_b_rw.mk_app_core(f, num, args, result);
         }
@@ -250,7 +252,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         if (fid == m_seq_rw.get_fid())
             return m_seq_rw.mk_app_core(f, num, args, result);
         if (fid == m_char_rw.get_fid())
-            return m_char_rw.mk_app_core(f, num, args, result);        
+            return m_char_rw.mk_app_core(f, num, args, result);
         if (fid == m_rec_rw.get_fid())
             return m_rec_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;