perf #6100

src/ast/ast.h

@@ -272,6 +272,7 @@ public:
 
     family_id get_family_id() const { return m_family_id; }
     decl_kind get_decl_kind() const { return m_kind; }
+    bool is_decl_of(family_id fid, decl_kind k) const { return m_family_id == fid && k == m_kind; }
     unsigned get_num_parameters() const { return m_parameters.size(); }
     parameter const & get_parameter(unsigned idx) const { return m_parameters[idx]; }
     parameter const * get_parameters() const { return m_parameters.begin(); }
@@ -577,6 +578,7 @@ public:
     decl_info * get_info() const { return m_info; }
     family_id get_family_id() const { return m_info == nullptr ? null_family_id : m_info->get_family_id(); }
     decl_kind get_decl_kind() const { return m_info == nullptr ? null_decl_kind : m_info->get_decl_kind(); }
+    bool is_decl_of(family_id fid, decl_kind k) const { return m_info && m_info->is_decl_of(fid, k); }
     unsigned get_num_parameters() const { return m_info == nullptr ? 0 : m_info->get_num_parameters(); }
     parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
     parameter const * get_parameters() const { return m_info == nullptr ? nullptr : m_info->get_parameters(); }
@@ -718,7 +720,7 @@ public:
     unsigned get_num_parameters() const { return get_decl()->get_num_parameters(); }
     parameter const& get_parameter(unsigned idx) const { return get_decl()->get_parameter(idx); }
     parameter const* get_parameters() const { return get_decl()->get_parameters(); }
-    bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
+    bool is_app_of(family_id fid, decl_kind k) const { return m_decl->is_decl_of(fid, k); }
     unsigned get_num_args() const { return m_num_args; }
     expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
     expr * const * get_args() const { return m_args; }

src/ast/bv_decl_plugin.cpp

@@ -424,7 +424,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
     // After SMT-COMP, I should find all offending modules.
     // For now, I will just simplify the numeral here.
     rational v = parameters[0].get_rational();
-    parameter p0(mod(v, rational::power_of_two(bv_size)));
+    parameter p0(mod2k(v, bv_size));
     parameter ps[2] = { std::move(p0), parameters[1] };
     sort * bv = get_bv_sort(bv_size);
     return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
@@ -642,7 +642,7 @@ void bv_decl_plugin::get_offset_term(app * a, expr * & t, rational & offset) con
         offset = decl->get_parameter(0).get_rational();
         sz     = decl->get_parameter(1).get_int();
         t      = a->get_arg(1);
-        offset = mod(offset, rational::power_of_two(sz));
+        offset = mod2k(offset, sz);
     }
     else {
         t      = a;
@@ -755,9 +755,9 @@ expr * bv_decl_plugin::get_some_value(sort * s) {
 }
 
 rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_signed) const {
-    rational r = mod(val, rational::power_of_two(bv_size));
+    rational r = mod2k(val, bv_size);
     SASSERT(!r.is_neg());
-    if (is_signed) {
+    if (is_signed) {        
         if (r >= rational::power_of_two(bv_size - 1)) {
             r -= rational::power_of_two(bv_size);
         }

src/ast/rewriter/bv_rewriter.cpp

@@ -1736,7 +1736,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
         unsigned low = 0;
         unsigned i = 0;
         while (i < sz) {
-            while (i < sz && mod(v1, two).is_one()) {
+            while (i < sz && v1.is_odd()) {
                 i++;
                 div(v1, two, v1);
             }
@@ -1745,7 +1745,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
                 exs.push_back(m_util.mk_numeral(rational::power_of_two(num_sz) - numeral(1), num_sz));
                 low = i;
             }
-            while (i < sz && mod(v1, two).is_zero()) {
+            while (i < sz && v1.is_even()) {
                 i++;
                 div(v1, two, v1);
             }

src/util/rational.h

@@ -232,11 +232,17 @@ public:
         rational::m().mod(r1.m_val, r2.m_val, r.m_val);
         return r;
     }
-
+    
     friend inline void mod(rational const & r1, rational const & r2, rational & r) {
         rational::m().mod(r1.m_val, r2.m_val, r.m_val);
     }
 
+    friend inline rational mod2k(rational const & a, unsigned k) {
+        if (a.is_nonneg() && a.is_int() && a.bitsize() <= k) 
+            return a;
+        return mod(a, power_of_two(k));
+    }
+
     friend inline rational operator%(rational const & r1, rational const & r2) {
         rational r;
         rational::m().rem(r1.m_val, r2.m_val, r.m_val);