1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 f2n.h 7 8 Abstract: 9 10 Template for wrapping a float-like API as a numeral-like API. 11 The basic idea is to have the rounding mode as an implicit argument. 12 13 Author: 14 15 Leonardo de Moura (leonardo) 2012-07-30. 16 17 Revision History: 18 19 --*/ 20 #pragma once 21 22 #include "util/mpf.h" 23 24 template<typename fmanager> 25 class f2n { 26 public: 27 typedef typename fmanager::numeral numeral; 28 struct exception {}; 29 30 private: 31 fmanager & m_manager; 32 mpf_rounding_mode m_mode; 33 unsigned m_ebits; 34 unsigned m_sbits; 35 numeral m_tmp1; 36 numeral m_one; 37 check(numeral const & n)38 void check(numeral const & n) { if (!m().is_regular(n)) throw exception(); } 39 40 public: field()41 static bool field() { return true; } precise()42 static bool precise() { return false; } 43 m_manager(m)44 f2n(fmanager & m, unsigned ebits = 11, unsigned sbits = 53):m_manager(m), m_mode(MPF_ROUND_TOWARD_POSITIVE), m_ebits(ebits), m_sbits(sbits) { 45 m_manager.set(m_one, ebits, sbits, 1); 46 } 47 f2n(f2n && other)48 f2n(f2n && other) : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits), 49 m_tmp1(std::move(other.m_tmp1)), m_one(std::move(other.m_one)) {} 50 ~f2n()51 ~f2n() { 52 m().del(m_tmp1); 53 m().del(m_one); 54 } 55 set_rounding_mode(mpf_rounding_mode m)56 void set_rounding_mode(mpf_rounding_mode m) { m_mode = m; } rounding_mode()57 mpf_rounding_mode rounding_mode() const { return m_mode; } round_to_plus_inf()58 void round_to_plus_inf() { m_mode = MPF_ROUND_TOWARD_POSITIVE; } round_to_minus_inf()59 void round_to_minus_inf() { m_mode = MPF_ROUND_TOWARD_NEGATIVE; } set_rounding(bool to_plus_inf)60 void set_rounding(bool to_plus_inf) { if (to_plus_inf) round_to_plus_inf(); else round_to_minus_inf(); } ebits()61 unsigned ebits() const { return m_ebits; } sbits()62 unsigned sbits() const { return m_sbits; } 63 m()64 fmanager & m() const { return m_manager; } 65 to_double(numeral & x)66 double to_double(numeral & x) const { return m().to_double(x); } 67 del(numeral & x)68 void del(numeral & x) { m().del(x); } 69 abs(numeral & o)70 void abs(numeral & o) { m().abs(o); } abs(numeral const & x,numeral & o)71 void abs(numeral const & x, numeral & o) { m().abs(x, o); } 72 neg(numeral & o)73 void neg(numeral & o) { m().neg(o); } neg(numeral const & x,numeral & o)74 void neg(numeral const & x, numeral & o) { m().neg(x, o); } 75 is_zero(numeral const & x)76 bool is_zero(numeral const & x) { return m().is_zero(x); } is_neg(numeral const & x)77 bool is_neg(numeral const & x) { return m().is_neg(x) && !m().is_zero(x); /* it is not clear whether actual hardware returns true for is_neg(0-) */ } is_pos(numeral const & x)78 bool is_pos(numeral const & x) { return m().is_pos(x) && !m().is_zero(x); } is_nonneg(numeral const & x)79 bool is_nonneg(numeral const & x) { return !is_neg(x); } is_nonpos(numeral const & x)80 bool is_nonpos(numeral const & x) { return !is_pos(x); } 81 set(numeral & o,int value)82 void set(numeral & o, int value) { m().set(o, m_ebits, m_sbits, value); check(o); } set(numeral & o,int n,int d)83 void set(numeral & o, int n, int d) { m().set(o, m_ebits, m_sbits, m_mode, n, d); check(o); } set(numeral & o,double x)84 void set(numeral & o, double x) { m().set(o, m_ebits, m_sbits, x); check(o); } set(numeral & o,unsigned value)85 void set(numeral & o, unsigned value) { m().set(o, m_ebits, m_sbits, (double)value); check(o); } set(numeral & o,numeral const & x)86 void set(numeral & o, numeral const & x) { m().set(o, x); check(o); } set(numeral & o,mpq const & x)87 void set(numeral & o, mpq const & x) { m().set(o, m_ebits, m_sbits, m_mode, x); check(o); } reset(numeral & o)88 void reset(numeral & o) { m().reset(o, m_ebits, m_sbits); } swap(numeral & x,numeral & y)89 static void swap(numeral & x, numeral & y) { x.swap(y); } 90 add(numeral const & x,numeral const & y,numeral & o)91 void add(numeral const & x, numeral const & y, numeral & o) { m().add(m_mode, x, y, o); check(o); } sub(numeral const & x,numeral const & y,numeral & o)92 void sub(numeral const & x, numeral const & y, numeral & o) { m().sub(m_mode, x, y, o); check(o); } mul(numeral const & x,numeral const & y,numeral & o)93 void mul(numeral const & x, numeral const & y, numeral & o) { m().mul(m_mode, x, y, o); check(o); } div(numeral const & x,numeral const & y,numeral & o)94 void div(numeral const & x, numeral const & y, numeral & o) { m().div(m_mode, x, y, o); check(o); } inv(numeral & o)95 void inv(numeral & o) { numeral a; set(a, 1); div(a, o, o); del(a); check(o); } inv(numeral const & x,numeral & o)96 void inv(numeral const & x, numeral & o) { set(o, x); inv(o); } inc(numeral & x)97 void inc(numeral & x) { add(x, m_one, x); } dec(numeral & x)98 void dec(numeral & x) { sub(x, m_one, x); } 99 power(numeral const & a,unsigned p,numeral & b)100 void power(numeral const & a, unsigned p, numeral & b) { 101 unsigned mask = 1; 102 numeral power; 103 set(power, a); 104 set(b, 1); 105 while (mask <= p) { 106 if (mask & p) 107 mul(b, power, b); 108 mul(power, power, power); 109 mask = mask << 1; 110 } 111 del(power); 112 check(b); 113 } 114 115 // Store the floor of a into b. Return true if a is an integer. 116 // Throws an exception if the result cannot be computed precisely. floor(numeral const & a,numeral & b)117 void floor(numeral const & a, numeral & b) { 118 SASSERT(m().is_regular(a)); 119 // Claim: If a is a regular float, then floor(a) is an integer that can be precisely represented. 120 // Justification: (for the case a is nonnegative) 121 // If 0 <= a > 2^sbits(), then a is an integer, and floor(a) == a 122 // If 0 <= a <= 2^sbits(), then floor(a) is representable since every integer less than 2^sbit 123 m().round_to_integral(MPF_ROUND_TOWARD_NEGATIVE, a, m_tmp1); 124 SASSERT(m().is_regular(m_tmp1)); 125 if (m().le(m_tmp1, a)) { 126 m().set(b, m_tmp1); 127 } 128 else { 129 // the rounding mode doesn't matter for the following operation. 130 m().sub(MPF_ROUND_TOWARD_NEGATIVE, m_tmp1, m_one, b); 131 } 132 SASSERT(m().is_regular(b)); 133 } 134 ceil(numeral const & a,numeral & b)135 void ceil(numeral const & a, numeral & b) { 136 SASSERT(m().is_regular(a)); 137 // See comment in floor 138 m().round_to_integral(MPF_ROUND_TOWARD_POSITIVE, a, m_tmp1); 139 SASSERT(m().is_regular(m_tmp1)); 140 if (m().ge(m_tmp1, a)) { 141 m().set(b, m_tmp1); 142 } 143 else { 144 // the rounding mode doesn't matter for the following operation. 145 m().add(MPF_ROUND_TOWARD_NEGATIVE, m_tmp1, m_one, b); 146 } 147 SASSERT(m().is_regular(b)); 148 } 149 prev_power_of_two(numeral const & a)150 unsigned prev_power_of_two(numeral const & a) { return m().prev_power_of_two(a); } 151 eq(numeral const & x,numeral const & y)152 bool eq(numeral const & x, numeral const & y) { return m().eq(x, y); } lt(numeral const & x,numeral const & y)153 bool lt(numeral const & x, numeral const & y) { return m().lt(x, y); } le(numeral const & x,numeral const & y)154 bool le(numeral const & x, numeral const & y) { return m().le(x, y); } gt(numeral const & x,numeral const & y)155 bool gt(numeral const & x, numeral const & y) { return m().gt(x, y); } ge(numeral const & x,numeral const & y)156 bool ge(numeral const & x, numeral const & y) { return m().ge(x, y); } 157 is_int(numeral const & x)158 bool is_int(numeral const & x) { return m().is_int(x); } is_one(numeral const & x)159 bool is_one(numeral const & x) { return m().is_one(x); } is_minus_one(numeral const & x)160 bool is_minus_one(numeral const & x) { numeral & _x = const_cast<numeral &>(x); m().neg(_x); bool r = m().is_one(_x); m().neg(_x); return r; } 161 to_string(numeral const & a)162 std::string to_string(numeral const & a) { return m().to_string(a); } to_rational_string(numeral const & a)163 std::string to_rational_string(numeral const & a) { return m().to_rational_string(a); } display(std::ostream & out,numeral const & a)164 void display(std::ostream & out, numeral const & a) { out << to_string(a); } display_decimal(std::ostream & out,numeral const & a,unsigned k)165 void display_decimal(std::ostream & out, numeral const & a, unsigned k) { m().display_decimal(out, a, k); } display_smt2(std::ostream & out,numeral const & a,bool decimal)166 void display_smt2(std::ostream & out, numeral const & a, bool decimal) { m().display_smt2(out, a, decimal); } 167 }; 168 169