From 7387fc9dec37248791a2a62bcabe86a4ea6a4a31 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2020 11:20:05 -0700 Subject: [PATCH] avoid some bignum overhead in addmul Signed-off-by: Nikolaj Bjorner --- src/math/lp/static_matrix_def.h | 8 ++++++-- src/util/rational.h | 4 ++++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index b48e24388..de86f1758 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -23,6 +23,10 @@ Revision History: #include "math/lp/static_matrix.h" namespace lp { // each assignment for this matrix should be issued only once!!! + +inline void addmul(double& r, double a, double b) { r += a*b; } +inline void addmul(mpq& r, mpq const& a, mpq const& b) { r.addmul(a, b); } + template void static_matrix::init_row_columns(unsigned m, unsigned n) { lp_assert(m_rows.size() == 0 && m_columns.size() == 0); @@ -54,14 +58,14 @@ template bool static_matrix::pivot_row_to_row_giv for (const auto & iv : m_rows[i]) { unsigned j = iv.var(); if (j == pivot_col) continue; - T alv = alpha * iv.coeff(); lp_assert(!is_zero(iv.coeff())); int j_offs = m_vector_of_row_offsets[j]; if (j_offs == -1) { // it is a new element + T alv = alpha * iv.coeff(); add_new_element(ii, j, alv); } else { - rowii[j_offs].coeff() += alv; + addmul(rowii[j_offs].coeff(), iv.coeff(), alpha); } } // clean the work vector diff --git a/src/util/rational.h b/src/util/rational.h index 0f2a2a1b7..f37336e4d 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -335,6 +335,10 @@ public: operator+=(k); else if (c.is_minus_one()) operator-=(k); + else if (k.is_one()) + operator+=(c); + else if (k.is_minus_one()) + operator-=(c); else { rational tmp(k); tmp *= c;