From bcb33a5b3a3dd96f06e2c826a547aae63d58c920 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Apr 2021 21:46:31 -0700
Subject: [PATCH] remove unused functions

---
 src/sat/smt/bv_internalize.cpp | 38 +---------------------------------
 src/sat/smt/bv_solver.h        |  4 +---
 2 files changed, 2 insertions(+), 40 deletions(-)

diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index fe0629479..81c9bd3bc 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -165,10 +165,7 @@ namespace bv {
 #define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin);
 #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
 #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
-#define internalize_int(B, U)                                   \
-        ibin = [&](expr* x, expr* y) { return B(x, y); };      \
-        iun = [&](expr* x) { return U(x); };                    \
-        internalize_interp(a, ibin, iun);
+#define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);
 
         switch (a->get_decl_kind()) {
         case OP_BV_NUM:           internalize_num(a); break;
@@ -527,22 +524,6 @@ namespace bv {
         internalize_binary(a, bin);
     }
 
-    void solver::internalize_udiv(app* n) {
-        bv_rewriter_params p(s().params());
-        expr* arg1 = n->get_arg(0);
-        expr* arg2 = n->get_arg(1);
-        mk_bits(get_th_var(n));
-        if (p.hi_div0()) {
-            add_unit(eq_internalize(n, bv.mk_bv_udiv_i(arg1, arg2)));
-            return;
-        }
-        unsigned sz = bv.get_bv_size(n);
-        expr_ref zero(bv.mk_numeral(0, sz), m);
-        expr_ref eq(m.mk_eq(arg2, zero), m);
-        expr_ref udiv(m.mk_ite(eq, bv.mk_bv_udiv0(arg1), bv.mk_bv_udiv_i(arg1, arg2)), m);
-        add_unit(eq_internalize(n, udiv));
-    }
-
     void solver::internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& iun) {
         bv_rewriter_params p(s().params());
         expr* arg1 = n->get_arg(0);
@@ -557,23 +538,6 @@ namespace bv {
         expr_ref eq(m.mk_eq(arg2, zero), m);
         expr_ref ite(m.mk_ite(eq, iun(arg1), ibin(arg1, arg2)), m);
         add_unit(eq_internalize(n, ite));
-
-    }
-
-    void solver::internalize_sdiv(app* n) {
-        bv_rewriter_params p(s().params());
-        expr* arg1 = n->get_arg(0);
-        expr* arg2 = n->get_arg(1);
-        mk_bits(get_th_var(n));
-        if (p.hi_div0()) {
-            add_unit(eq_internalize(n, bv.mk_bv_sdiv_i(arg1, arg2)));
-            return;
-        }
-        unsigned sz = bv.get_bv_size(n);
-        expr_ref zero(bv.mk_numeral(0, sz), m);
-        expr_ref eq(m.mk_eq(arg2, zero), m);
-        expr_ref sdiv(m.mk_ite(eq, bv.mk_bv_sdiv0(arg1), bv.mk_bv_sdiv_i(arg1, arg2)), m);
-        add_unit(eq_internalize(n, sdiv));
     }
 
     void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) {
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index de21d2399..cf3d13751 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -239,6 +239,7 @@ namespace bv {
         void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
         void internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn);
         void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
+        void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);
         void internalize_num(app * n);       
         void internalize_concat(app * n);        
         void internalize_bv2int(app* n);
@@ -249,9 +250,6 @@ namespace bv {
         void internalize_sub(app* n);
         void internalize_extract(app* n);
         void internalize_bit2bool(app* n);
-        void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);
-        void internalize_udiv(app* n);
-        void internalize_sdiv(app* n);
         void internalize_udiv_i(app* n);
         template<bool Signed, bool Reverse, bool Negated>
         void internalize_le(app* n);