lean2/src/numerics/mpq.cpp
Leonardo de Moura c581990f67 Clean white-spaces
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-19 10:29:33 -07:00

104 lines
2.4 KiB
C++

/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "mpq.h"
namespace lean {
int cmp(mpq const & a, mpz const & b) {
if (a.is_integer()) {
return mpz_cmp(mpq_numref(a.m_val), mpq::zval(b));
}
else {
static thread_local mpz tmp;
mpz_mul(mpq::zval(tmp), mpq_denref(a.m_val), mpq::zval(b));
return mpz_cmp(mpq_numref(a.m_val), mpq::zval(tmp));
}
}
void mpq::floor() {
if (is_integer())
return;
bool neg = is_neg();
mpz_tdiv_q(mpq_numref(m_val), mpq_numref(m_val), mpq_denref(m_val));
mpz_set_ui(mpq_denref(m_val), 1);
if (neg)
mpz_sub_ui(mpq_numref(m_val), mpq_numref(m_val), 1);
}
void mpq::ceil() {
if (is_integer())
return;
bool pos = is_pos();
mpz_tdiv_q(mpq_numref(m_val), mpq_numref(m_val), mpq_denref(m_val));
mpz_set_ui(mpq_denref(m_val), 1);
if (pos)
mpz_add_ui(mpq_numref(m_val), mpq_numref(m_val), 1);
}
mpz floor(mpq const & a) {
if (a.is_integer())
return a.get_numerator();
mpz r;
mpz_tdiv_q(mpq::zval(r), mpq_numref(a.m_val), mpq_denref(a.m_val));
if (a.is_neg())
--r;
return r;
}
mpz ceil(mpq const & a) {
if (a.is_integer())
return a.get_numerator();
mpz r;
mpz_tdiv_q(mpq::zval(r), mpq_numref(a.m_val), mpq_denref(a.m_val));
if (a.is_pos())
++r;
return r;
}
extern void display(std::ostream & out, __mpz_struct const * v);
std::ostream & operator<<(std::ostream & out, mpq const & v) {
if (v.is_integer()) {
display(out, mpq_numref(v.m_val));
}
else {
display(out, mpq_numref(v.m_val));
out << "/";
display(out, mpq_denref(v.m_val));
}
return out;
}
void display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
mpz n1, d1, v1;
numerator(n1, a);
denominator(d1, a);
if (a.is_neg()) {
out << "-";
neg(n1);
}
v1 = n1 / d1;
out << v1;
n1 = rem(n1, d1);
if (n1.is_zero())
return;
out << ".";
for (unsigned i = 0; i < prec; i++) {
n1 *= 10;
v1 = n1 / d1;
lean_assert(v1 < 10);
out << v1;
n1 = rem(n1, d1);
if (n1.is_zero())
return;
}
out << "?";
}
}
void pp(lean::mpq const & v) { std::cout << v << std::endl; }