68     if (m_manager.is_zero(a.m_num)) {  in normalize()
75     unsigned k = m_manager.power_of_two_multiple(a.m_num);  in normalize()
78     m_manager.machine_div2k(a.m_num, k);  in normalize()
87     if (m_manager.is_zero(a.m_num))  in magnitude_lb()
89     if (m_manager.is_pos(a.m_num))  in magnitude_lb()
90         return m_manager.log2(a.m_num) - a.m_k;  in magnitude_lb()
91     return m_manager.mlog2(a.m_num) - a.m_k + 1;  in magnitude_lb()
95     if (m_manager.is_zero(a.m_num))  in magnitude_ub()
97     if (m_manager.is_pos(a.m_num))  in magnitude_ub()
98         return m_manager.log2(a.m_num) - a.m_k + 1;  in magnitude_ub()
99     return m_manager.mlog2(a.m_num) - a.m_k;  in magnitude_ub()
104         m_manager.mul2k(a.m_num, 1);  in mul2()
113         m_manager.mul2k(a.m_num, k - a.m_k);  in mul2k()
128         m_manager.add(a.m_num, b.m_num, r.m_num);  in add()
132         m_manager.mul2k(a.m_num, b.m_k - a.m_k, m_tmp);  in add()
133         m_manager.add(b.m_num, m_tmp, r.m_num);  in add()
138         m_manager.mul2k(b.m_num, a.m_k - b.m_k, m_tmp);  in add()
139         m_manager.add(a.m_num, m_tmp, r.m_num);  in add()
155         m_manager.add(a.m_num, b, r.m_num);  in add()
160         m_manager.add(a.m_num, m_tmp, r.m_num);  in add()
177         m_manager.sub(a.m_num, b.m_num, r.m_num);  in sub()
181         m_manager.mul2k(a.m_num, b.m_k - a.m_k, m_tmp);  in sub()
182         m_manager.sub(m_tmp, b.m_num, r.m_num);  in sub()
187         m_manager.mul2k(b.m_num, a.m_k - b.m_k, m_tmp);  in sub()
188         m_manager.sub(a.m_num, m_tmp, r.m_num);  in sub()
205         m_manager.sub(a.m_num, b, r.m_num);  in sub()
210         m_manager.sub(a.m_num, m_tmp, r.m_num);  in sub()
225     m_manager.mul(a.m_num, b.m_num, r.m_num);  in mul()
242     m_manager.mul(a.m_num, b, r.m_num);  in mul()
257     m_manager.power(a.m_num, k, a.m_num);  in power()
261     bool r = m_manager.root(a.m_num, n);  in root_lower()
263         m_manager.dec(a.m_num);  in root_lower()
269     else if (m_manager.is_neg(a.m_num)) {  in root_lower()
283     bool r = m_manager.root(a.m_num, n);  in root_upper()
289     else if (m_manager.is_neg(a.m_num)) {  in root_upper()
318         return m_manager.lt(a.m_num, b.m_num);  in lt()
321         m_manager.mul2k(a.m_num, b.m_k - a.m_k, m_tmp);  in lt()
322         return m_manager.lt(m_tmp, b.m_num);  in lt()
326         m_manager.mul2k(b.m_num, a.m_k - b.m_k, m_tmp);  in lt()
327         return m_manager.lt(a.m_num, m_tmp);  in lt()
332     if (m_manager.is_nonpos(a.m_num))  in lt_1div2k()
341         return m_manager.lt(a.m_num, m_tmp);  in lt_1div2k()
347         return m_manager.eq(a.m_num, b.numerator());  in eq()
349     m_manager.mul(a.m_num, b.denominator(), m_tmp2);  in eq()
355         return m_manager.lt(a.m_num, b.numerator());  in lt()
356     m_manager.mul(a.m_num, b.denominator(), m_tmp);  in lt()
363         return m_manager.le(a.m_num, b.numerator());  in le()
364     m_manager.mul(a.m_num, b.denominator(), m_tmp);  in le()
371         return m_manager.lt(a.m_num, b);  in lt()
373     return m_manager.lt(a.m_num, m_tmp);  in lt()
378         return m_manager.le(a.m_num, b);  in le()
380     return m_manager.le(a.m_num, m_tmp);  in le()
385     buffer << m_manager.to_string(a.m_num);  in to_string()
394     out << m_manager.to_string(a.m_num);  in display()
403     out << m_manager.to_string(a.m_num);  in display_pp()
413         m_manager.display_smt2(out, a.m_num, decimal);  in display_smt2()
417         m_manager.display_smt2(out, a.m_num, decimal);  in display_smt2()
430         return out << m_manager.to_string(a.m_num);  in display_decimal()
436     if (m_manager.is_neg(a.m_num))  in display_decimal()
438     m_manager.set(v1, a.m_num);  in display_decimal()
467     if (m_manager.is_neg(a.m_num) != m_manager.is_neg(b.m_num))   in display_decimal()
469     if (m_manager.is_neg(a.m_num))  in display_decimal()
471     m_manager.set(v1, a.m_num);  in display_decimal()
473     m_manager.set(v2, b.m_num);  in display_decimal()
580         m_manager.set(r, lower.m_num);  in select_integer()
584         m_manager.set(r, upper.m_num);  in select_integer()
601         m_manager.set(r, upper.m_num);  in select_integer()
626         m_manager.set(r, lower.m_num);  in select_integer()
841     bool sgn  = m_manager.is_neg(a.m_num);  in approx()
844     m_manager.abs(a.m_num);  in approx()
845     m_manager.machine_div2k(a.m_num, shift);  in approx()
847         m_manager.inc(a.m_num);  in approx()
849         m_manager.neg(a.m_num);  in approx()
865     if (m_manager.is_power_of_two(b.m_num, k_prime)) {  in approx_div()
868         m_manager.set(c.m_num, a.m_num);  in approx_div()
873             m_manager.mul(c.m_num, pw2, c.m_num);  in approx_div()
878     else if (m_manager.divides(b.m_num, a.m_num)) {  in approx_div()
880         m_manager.div(a.m_num, b.m_num, c.m_num);  in approx_div()
885             m_manager.mul2k(c.m_num, b.m_k - a.m_k);  in approx_div()
895         m_manager.set(abs_a, a.m_num);  in approx_div()
897         m_manager.set(abs_b, b.m_num);  in approx_div()
909         m_manager.div(norm_a, abs_b, c.m_num);  in approx_div()
911             m_manager.inc(c.m_num);  in approx_div()
913             m_manager.neg(c.m_num);  in approx_div()