Add rational::next_power_of_two

src/util/mpq.cpp

@@ -316,6 +316,12 @@ unsigned mpq_manager<SYNCH>::prev_power_of_two(mpq const & a) {
     return prev_power_of_two(_tmp);
 }
 
+template<bool SYNCH>
+unsigned mpq_manager<SYNCH>::next_power_of_two(mpq const & a) {
+    _scoped_numeral<mpz_manager<SYNCH> > _tmp(*this);
+    ceil(a, _tmp);
+    return next_power_of_two(_tmp);
+}
 
 template<bool SYNCH>
 template<bool SUB>

src/util/mpq.h

@@ -848,6 +848,14 @@ public:
     unsigned prev_power_of_two(mpz const & a) { return mpz_manager<SYNCH>::prev_power_of_two(a); }
     unsigned prev_power_of_two(mpq const & a);
 
+    /**
+       \brief Return the smallest k s.t. a <= 2^k.
+
+       \remark Return 0 if a is not positive.
+    */
+    unsigned next_power_of_two(mpz const & a) { return mpz_manager<SYNCH>::next_power_of_two(a); }
+    unsigned next_power_of_two(mpq const & a);
+
     bool is_int_perfect_square(mpq const & a, mpq & r) {
         SASSERT(is_int(a));
         reset_denominator(r);

src/util/mpz.cpp

@@ -2288,6 +2288,19 @@ unsigned mpz_manager<SYNCH>::bitsize(mpz const & a) {
         return mlog2(a) + 1;
 }
 
+template<bool SYNCH>
+unsigned mpz_manager<SYNCH>::next_power_of_two(mpz const & a) {
+    if (is_nonpos(a))
+        return 0;
+    if (is_one(a))
+        return 0;
+    unsigned shift;
+    if (is_power_of_two(a, shift))
+        return shift;
+    else
+        return log2(a) + 1;
+}
+
 template<bool SYNCH>
 bool mpz_manager<SYNCH>::is_perfect_square(mpz const & a, mpz & root) {
     if (is_neg(a))

src/util/mpz.h

@@ -692,6 +692,13 @@ public:
        \remark Return 0 if a is not positive.
     */
     unsigned prev_power_of_two(mpz const & a) { return log2(a); }
+
+    /**
+       \brief Return the smallest k s.t. a <= 2^k.
+
+       \remark Return 0 if a is not positive.
+    */
+    unsigned next_power_of_two(mpz const & a);
     
     /**
        \brief Return true if a^{1/n} is an integer, and store the result in a.

src/util/rational.h

@@ -489,6 +489,18 @@ public:
         return get_num_digits(rational(10));
     }
 
+    /**
+     * \brief Return the biggest k s.t. 2^k <= a.
+     * \remark Return 0 if a is not positive.
+     */
+    unsigned prev_power_of_two() const { return m().prev_power_of_two(m_val); }
+
+    /**
+     * \brief Return the smallest k s.t. a <= 2^k.
+     * \remark Return 0 if a is not positive.
+     */
+    unsigned next_power_of_two() const { return m().next_power_of_two(m_val); }
+
     bool get_bit(unsigned index) const {
         return m().get_bit(m_val, index);
     }