From ab9aee189b7be07d6c0ad6eb218693c534b405d6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Jun 2022 13:49:52 -0700 Subject: [PATCH] perf #6100 --- src/ast/ast.h | 4 +++- src/ast/bv_decl_plugin.cpp | 8 ++++---- src/ast/rewriter/bv_rewriter.cpp | 4 ++-- src/util/rational.h | 8 +++++++- 4 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index fcf83a65c..798280d2c 100644 --- a/src/ast/ast.h +++ b/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; } diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index e6a1f3b79..76c8ec6dd 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/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); } diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 5e2d3816e..516248e24 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/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); } diff --git a/src/util/rational.h b/src/util/rational.h index 9fadfb91f..dffcc52f3 100644 --- a/src/util/rational.h +++ b/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);