mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

avoid some bignum overhead in addmul

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-14 11:20:05 -07:00
parent 53e49eb428
commit 7387fc9dec
2 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/static_matrix_def.h
View file

@ -23,6 +23,10 @@ Revision History:
#include "math/lp/static_matrix.h" #include "math/lp/static_matrix.h"
namespace lp { namespace lp {
// each assignment for this matrix should be issued only once!!! // 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 <typename T, typename X> template <typename T, typename X>
void static_matrix<T, X>::init_row_columns(unsigned m, unsigned n) { void static_matrix<T, X>::init_row_columns(unsigned m, unsigned n) {
lp_assert(m_rows.size() == 0 && m_columns.size() == 0); lp_assert(m_rows.size() == 0 && m_columns.size() == 0);
@ -54,14 +58,14 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
for (const auto & iv : m_rows[i]) { for (const auto & iv : m_rows[i]) {
unsigned j = iv.var(); unsigned j = iv.var();
if (j == pivot_col) continue; if (j == pivot_col) continue;
T alv = alpha * iv.coeff();
lp_assert(!is_zero(iv.coeff())); lp_assert(!is_zero(iv.coeff()));
int j_offs = m_vector_of_row_offsets[j]; int j_offs = m_vector_of_row_offsets[j];
if (j_offs == -1) { // it is a new element if (j_offs == -1) { // it is a new element
T alv = alpha * iv.coeff();
add_new_element(ii, j, alv); add_new_element(ii, j, alv);
} }
else { else {
rowii[j_offs].coeff() += alv; addmul(rowii[j_offs].coeff(), iv.coeff(), alpha);
} }
} }
// clean the work vector // clean the work vector

4
src/util/rational.h
View file

@ -335,6 +335,10 @@ public:
operator+=(k); operator+=(k);
else if (c.is_minus_one()) else if (c.is_minus_one())
operator-=(k); operator-=(k);
else if (k.is_one())
operator+=(c);
else if (k.is_minus_one())
operator-=(c);
else { else {
rational tmp(k); rational tmp(k);
tmp *= c; tmp *= c;