michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(numerics): rename power operator to pow, the idea is to follow the C/C++ name convention for the power operator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-21 17:23:56 -07:00
parent f1d9312521
commit e208309abd
6 changed files with 14 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tests/util/numerics/mpz.cpp
View file

@ -32,7 +32,7 @@ static void tst1() {
lean_assert_eq(mpz(-10) % mpz(-3), 2);
lean_assert_eq(mpz(-10) % mpz(3), 2);
mpz big;
big = power(mpz(10), 10000);
big = pow(mpz(10), 10000);
std::ostringstream out;
out << big;
std::string s = out.str();

10
src/tests/util/sexpr.cpp
View file

@ -107,11 +107,11 @@ static void tst2() {
lean_assert(a == mpq(1, 3));
lean_assert(mpq(1, 3) == a);
lean_assert(mpq(2, 3) != a);
a = power(mpz(2), 100);
lean_assert(a == sexpr(power(mpz(2), 100)));
lean_assert(a == power(mpz(2), 100));
lean_assert(power(mpz(2), 100) == a);
lean_assert(mpq(power(mpz(2), 100)) != a);
a = pow(mpz(2), 100);
lean_assert(a == sexpr(pow(mpz(2), 100)));
lean_assert(a == pow(mpz(2), 100));
lean_assert(pow(mpz(2), 100) == a);
lean_assert(mpq(pow(mpz(2), 100)) != a);
lean_assert(sexpr(1, 2) != sexpr(2, 1));
lean_assert(sexpr(1, 2) != sexpr(1, sexpr(2, nil())));
lean_assert(sexpr(1, 2) == sexpr(1, sexpr(2)));

1
src/util/numerics/mpbq.h
View file

@ -179,6 +179,7 @@ public:
friend void power(mpbq & a, mpbq const & b, unsigned k);
friend void _power(mpbq & a, mpbq const & b, unsigned k) { power(a, b, k); }
friend mpbq pow(mpbq a, unsigned k) { power(a, a, k); return a; }
/**
\brief Return the magnitude of a = b/2^k.

10
src/util/numerics/mpfp.h
View file

@ -481,11 +481,11 @@ public:
void power(mpz_t const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow_z(m_val, m_val, b, rnd); }
void power(mpz const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow_z(m_val, m_val, b.m_val, rnd); }
friend mpfp power(mpfp a, mpfp const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a;; }
friend mpfp power(mpfp a, unsigned long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a;; }
friend mpfp power(mpfp a, long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a;; }
friend mpfp power(mpfp a, mpz_t const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a;; }
friend mpfp power(mpfp a, mpz const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a;; }
friend mpfp pow(mpfp a, mpfp const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, unsigned long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, mpz_t const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, mpz const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend std::ostream & operator<<(std::ostream & out, mpfp const & v);
};

2
src/util/numerics/mpq.h
View file

@ -205,7 +205,7 @@ public:
friend void power(mpq & a, mpq const & b, unsigned k);
friend void _power(mpq & a, mpq const & b, unsigned k) { power(a, b, k); }
friend mpq power(mpq a, unsigned k) { power(a, a, k); return a; }
friend mpq pow(mpq a, unsigned k) { power(a, a, k); return a; }
friend std::ostream & operator<<(std::ostream & out, mpq const & v);

2
src/util/numerics/mpz.h
View file

@ -204,7 +204,7 @@ public:
friend void power(mpz & a, mpz const & b, unsigned k) { mpz_pow_ui(a.m_val, b.m_val, k); }
friend void _power(mpz & a, mpz const & b, unsigned k) { power(a, b, k); }
friend mpz power(mpz const & a, unsigned k) { mpz r; power(r, a, k); return r; }
friend mpz pow(mpz a, unsigned k) { power(a, a, k); return a; }
friend void rootrem(mpz & root, mpz & rem, mpz const & a, unsigned k) { mpz_rootrem(root.m_val, rem.m_val, a.m_val, k); }
// root <- a^{1/k}, return true iff the result is an integer