mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

add back old multiplication for comparison

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-09 14:33:32 -07:00
parent de454db58c
commit 567fbac27f
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/util/mpq.cpp
View file

@ -346,6 +346,7 @@ void mpq_manager<SYNCH>::lin_arith_op(mpq const& a, mpq const& b, mpq& c, mpz& g
template<bool SYNCH>
void mpq_manager<SYNCH>::rat_mul(mpq const & a, mpq const & b, mpq & c, mpz& g1, mpz& g2, mpz& tmp1, mpz& tmp2) {
#if 1
gcd(a.m_den, b.m_num, g1);
gcd(a.m_num, b.m_den, g2);
div(a.m_num, g2, tmp1);
@ -354,6 +355,11 @@ void mpq_manager<SYNCH>::rat_mul(mpq const & a, mpq const & b, mpq & c, mpz& g1,
div(b.m_den, g2, tmp1);
div(a.m_den, g1, tmp2);
mul(tmp1, tmp2, c.m_den);
#else
mul(a.m_num, b.m_num, c.m_num);
mul(a.m_den, b.m_den, c.m_den);
normalize(c);
#endif
}
template<bool SYNCH>