fix #3994 remove bogus option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 17, 2020 · 040d4b8 · 040d4b8
1 parent 767dff4
commit 040d4b8
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 21 deletions.
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
@@ -33,7 +33,6 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_urem_simpl = p.bv_urem_simpl();
     m_blast_eq_value = p.blast_eq_value();
     m_split_concat_eq = p.split_concat_eq();
-    m_udiv2mul = p.udiv2mul();
     m_bvnot2arith = p.bvnot2arith();
     m_bvnot_simpl = p.bv_not_simpl();
     m_bv_sort_ac = p.bv_sort_ac();
@@ -1046,8 +1045,6 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
 
     TRACE("bv_udiv", tout << "hi_div0: " << hi_div0 << "\n";);
 
-    TRACE("udiv2mul", tout << mk_ismt2_pp(arg2, m()) << " udiv2mul: " << m_udiv2mul << "\n";);
-
     if (is_numeral(arg2, r2, bv_size)) {
         r2 = m_util.norm(r2, bv_size);
         if (r2.is_zero()) {
@@ -1080,14 +1077,6 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
             return BR_REWRITE1;
         }
 
-        if (m_udiv2mul) {
-            TRACE("udiv2mul", tout << "using udiv2mul\n";);
-            numeral inv_r2;
-            if (m_util.mult_inverse(r2, bv_size, inv_r2)) {
-                result = m().mk_app(get_fid(), OP_BMUL, mk_numeral(inv_r2, bv_size), arg1);
-                return BR_REWRITE1;
-            }
-        }
 
         result = m().mk_app(get_fid(), OP_BUDIV_I, arg1, arg2);
         return BR_DONE;

diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
@@ -59,7 +59,6 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_mkbv2num;
     bool       m_ite2id;
     bool       m_split_concat_eq;
-    bool       m_udiv2mul;
     bool       m_bvnot2arith;
     bool       m_bv_sort_ac;
     bool       m_trailing;

diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg
@@ -1,8 +1,7 @@
 def_module_params(module_name='rewriter',
                   class_name='bv_rewriter_params',
                   export=True,
-                  params=(("udiv2mul", BOOL, False, "convert constant udiv to mul"),
-                          ("split_concat_eq", BOOL, False, "split equalities of the form (= (concat t1 t2) t3)"),
+                  params=(("split_concat_eq", BOOL, False, "split equalities of the form (= (concat t1 t2) t3)"),
                           ("bit2bool", BOOL, True, "try to convert bit-vector terms of size 1 into Boolean terms"),
                           ("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"),
                           ("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
@@ -913,12 +913,12 @@ namespace smt {
             enode * parent = *it;
             if (parent->is_cgc_enabled()) {
                 CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent),
-                       tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" <<
-                       parent->get_owner_id() << ", parents: \n";
-                       for (unsigned i = 0; i < r2->m_parents.size(); i++) {
-                           tout << "#" << r2->m_parents[i]->get_owner_id() << " ";
-                       }
-                       display(tout););
+                       tout << "old num_parents: " << r2_num_parents 
+                            << "\nnum_parents: " << r2->m_parents.size() 
+                            << "\nparent: #" << parent->get_owner_id() 
+                            << "\nparents: ";
+                       for (enode* p : r2->m_parents) tout << "#" << p->get_owner_id() << " ";
+                       display(tout << "\n"););
                 SASSERT(parent->is_cgr());
                 SASSERT(m_cg_table.contains_ptr(parent));
                 m_cg_table.erase(parent);
@@ -930,7 +930,7 @@ namespace smt {
             curr->m_root = r1;
             curr = curr->m_next;
         }
-        while(curr != r1);
+        while (curr != r1);
 
         // restore parents of r2
         r2->m_parents.shrink(r2_num_parents);
@@ -939,6 +939,7 @@ namespace smt {
         for (enode * parent : enode::parents(r1)) {
             TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";);
             if (parent->is_cgc_enabled()) {
+
                 enode * cg = parent->m_cg;
                 if (!parent->is_true_eq() &&
                     (parent == cg ||           // parent was root of the congruence class before and after the merge