diff --git a/docs/.doctrees/environment.pickle b/docs/.doctrees/environment.pickle index 2cb7233..bafb806 100644 Binary files a/docs/.doctrees/environment.pickle and b/docs/.doctrees/environment.pickle differ diff --git a/docs/.doctrees/index.doctree b/docs/.doctrees/index.doctree index 624c770..c7a170b 100644 Binary files a/docs/.doctrees/index.doctree and b/docs/.doctrees/index.doctree differ diff --git a/docs/_sources/index.txt b/docs/_sources/index.txt index f4d8499..beabcd0 100644 --- a/docs/_sources/index.txt +++ b/docs/_sources/index.txt @@ -5,9 +5,18 @@ PyMPF .. toctree:: :maxdepth: 2 +========= +Rationals +========= + +.. automodule:: mpf.rationals + :members: + :special-members: + === MPF === .. automodule:: mpf.floats :members: + :special-members: diff --git a/docs/genindex.html b/docs/genindex.html index f79430f..ffcf8c3 100644 --- a/docs/genindex.html +++ b/docs/genindex.html @@ -52,10 +52,142 @@

Navigation

Index

- F + _ + | C + | F + | I | M + | N + | P + | Q + | R + | S + | T + | U
+

_

+ + + +
+ +
__abs__() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+ +
__add__() (mpf.rationals.Rational method) +
+ + +
__eq__() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+ +
__ge__() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+ +
__gt__() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+ +
__le__() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+
+ +
__lt__() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+ +
__mul__() (mpf.rationals.Rational method) +
+ + +
__ne__() (mpf.rationals.Rational method) +
+ + +
__neg__() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+ +
__pow__() (mpf.rationals.Rational method) +
+ + +
__sub__() (mpf.rationals.Rational method) +
+ + +
__truediv__() (mpf.rationals.Rational method) +
+ + +
__weakref__ (mpf.floats.MPF attribute) +
+ +
+ +
(mpf.rationals.Rational attribute) +
+ +
+
+ +

C

+ + +
+ +
compatible() (mpf.floats.MPF method) +
+ +
+

F

+ +
@@ -63,6 +195,146 @@

F

fp_add() (in module mpf.floats)
+ +
fp_div() (in module mpf.floats) +
+ + +
fp_fma() (in module mpf.floats) +
+ + +
fp_from_float() (in module mpf.floats) +
+ + +
fp_from_int() (in module mpf.floats) +
+ + +
fp_from_sbv() (in module mpf.floats) +
+ + +
fp_from_ubv() (in module mpf.floats) +
+ + +
fp_max() (in module mpf.floats) +
+ + +
fp_min() (in module mpf.floats) +
+ + +
fp_mul() (in module mpf.floats) +
+ +
+ +
fp_nextDown() (in module mpf.floats) +
+ + +
fp_nextUp() (in module mpf.floats) +
+ + +
fp_rem() (in module mpf.floats) +
+ + +
fp_roundToIntegral() (in module mpf.floats) +
+ + +
fp_sqrt() (in module mpf.floats) +
+ + +
fp_sub() (in module mpf.floats) +
+ + +
fp_to_int() (in module mpf.floats) +
+ + +
fp_to_sbv() (in module mpf.floats) +
+ + +
fp_to_ubv() (in module mpf.floats) +
+ + +
from_rational() (mpf.floats.MPF method) +
+ +
+ +

I

+ + +
+ +
isFinite() (mpf.floats.MPF method) +
+ + +
isInfinite() (mpf.floats.MPF method) +
+ + +
isIntegral() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+ +
isNaN() (mpf.floats.MPF method) +
+ + +
isNegative() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+
+ +
isNormal() (mpf.floats.MPF method) +
+ + +
isPositive() (mpf.floats.MPF method) +
+ + +
isSubnormal() (mpf.floats.MPF method) +
+ + +
isZero() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
@@ -70,9 +342,217 @@

M

+ +
+
MPF (class in mpf.floats) +
+ +
+
mpf.floats (module)
+ +
mpf.rationals (module) +
+ +
+ +

N

+ + +
+ +
new_mpf() (mpf.floats.MPF method) +
+ +
+ +

P

+ + +
+ +
pack() (mpf.floats.MPF method) +
+ +
+ +

Q

+ + + +
+ +
q_from_decimal_fragments() (in module mpf.rationals) +
+ + +
q_pow2() (in module mpf.rationals) +
+ + +
q_round_rna() (in module mpf.rationals) +
+ + +
q_round_rne() (in module mpf.rationals) +
+ +
+ +
q_round_rtn() (in module mpf.rationals) +
+ + +
q_round_rtp() (in module mpf.rationals) +
+ + +
q_round_rtz() (in module mpf.rationals) +
+ + +
q_round_to_nearest() (in module mpf.rationals) +
+ +
+ +

R

+ + +
+ +
Rational (class in mpf.rationals) +
+ +
+ +

S

+ + + +
+ +
set_infinite() (mpf.floats.MPF method) +
+ + +
set_nan() (mpf.floats.MPF method) +
+ + +
set_sign_bit() (mpf.floats.MPF method) +
+ + +
set_zero() (mpf.floats.MPF method) +
+ + +
smtlib_eq() (in module mpf.floats) +
+ + +
smtlib_from_binary_interchange() (mpf.floats.MPF method) +
+ + +
smtlib_from_float() (mpf.floats.MPF method) +
+ + +
smtlib_from_int() (mpf.floats.MPF method) +
+ +
+ +
smtlib_from_real() (mpf.floats.MPF method) +
+ + +
smtlib_from_sbv() (mpf.floats.MPF method) +
+ + +
smtlib_from_ubv() (mpf.floats.MPF method) +
+ + +
smtlib_literal() (mpf.floats.MPF method) +
+ + +
smtlib_literals() (mpf.floats.MPF method) +
+ + +
smtlib_random_literal() (mpf.floats.MPF method) +
+ + +
smtlib_sort() (mpf.floats.MPF method) +
+ + +
smtlib_to_int() (mpf.floats.MPF method) +
+ + +
smtlib_to_real() (mpf.floats.MPF method) +
+ +
+ +

T

+ + + +
+ +
to_decimal_string() (mpf.rationals.Rational method) +
+ + +
to_int() (mpf.floats.MPF method) +
+ + +
to_python_float() (mpf.floats.MPF method) +
+ +
+ +
(mpf.rationals.Rational method) +
+ +
+
+ +
to_python_int() (mpf.rationals.Rational method) +
+ + +
to_python_string() (mpf.floats.MPF method) +
+ + +
to_rational() (mpf.floats.MPF method) +
+ + +
to_smtlib() (mpf.rationals.Rational method) +
+ +
+ +

U

+ +
+ +
unpack() (mpf.floats.MPF method) +
+
diff --git a/docs/index.html b/docs/index.html index 17644be..3f9e6f5 100644 --- a/docs/index.html +++ b/docs/index.html @@ -51,33 +51,727 @@

Navigation

PyMPF

+ +
+

Rationals

+

This module defines class to deal with Rational numbers.

+
+

Todo

+

This should be a subclass of fractions.Fraction.

+
+
+
+class mpf.rationals.Rational(a=0, b=1)
+

Rational number

+

a is the numerator

+

b is the denominator

+
+
+__abs__()
+

Absolute value

+
+ +
+
+__add__(other)
+

Addition

+
+ +
+
+__eq__(other)
+

Equality

+
+ +
+
+__ge__(other)
+

>=

+
+ +
+
+__gt__(other)
+

>

+
+ +
+
+__le__(other)
+

<=

+
+ +
+
+__lt__(other)
+

<

+
+ +
+
+__mul__(other)
+

Multiplication

+
+ +
+
+__ne__(other)
+

Inequality

+
+ +
+
+__neg__()
+

Negation

+
+ +
+
+__pow__(other)
+

Exponentiation

+

The right-hand side must be an integral Rational, otherwise +AssertionError is raised.

+
+ +
+
+__sub__(other)
+

Substraction

+
+ +
+
+__truediv__(other)
+

Division

+
+ +
+
+__weakref__
+

list of weak references to the object (if defined)

+
+ +
+
+isIntegral()
+

Test if integral

+
+ +
+
+isNegative()
+

Test if negative

+

Returns false for 0.

+
+ +
+
+isZero()
+

Test if zero

+
+ +
+
+to_decimal_string()
+

Convert to decimal string

+

If the fraction does not terminate (e.g. for 1 / 3), an +exception is thrown.

+
+ +
+
+to_python_float()
+

Convert to python float

+
+ +
+
+to_python_int()
+

Convert to python int

+
+ +
+
+to_smtlib()
+

Convert to SMT-LIB Real expression

+

Returns literal for integrals, e.g. “1.0”.

+

Returns an s-expression otherwise, e.g. “(- (/ 1.0 3.0))”.

+
+ +
+ +
+
+mpf.rationals.q_from_decimal_fragments(sign, integer_part, fraction_part, exp_part)
+

Build a rational from string fragments of a decimal number.

+
+
E.g. for “1.23E-1” we have fragments for
+
sign = “” +integer_part = “1” +fraction_part = “23” +exp_part = “-1”
+
+
+ +
+
+mpf.rationals.q_pow2(n)
+

Create rational for 2^n

+

n can be negative

+
+ +
+
+mpf.rationals.q_round_rna(n)
+

Round to nearest integer, away from zero

+
+ +
+
+mpf.rationals.q_round_rne(n)
+

Round to nearest even integer

+
+ +
+
+mpf.rationals.q_round_rtn(n)
+

Round to nearest integer, towards negative

+
+ +
+
+mpf.rationals.q_round_rtp(n)
+

Round to nearest integer, towards positive

+
+ +
+
+mpf.rationals.q_round_rtz(n)
+

Round to nearest integer, towards zero

+
+ +
+
+mpf.rationals.q_round_to_nearest(n, tiebreak)
+

Round to nearest integer

+

Round n to the nearest integer

+

Calls the tiebreak*(upper, lower) function with the two +alternatives if *n is precisely between two integers.

+
+

MPF

+

This module implements IEEE floats using bitvectors as the in-memory +format, but rationals (plus rounding and special case handling) for +calculation. This allows us to directly implement the semantics +described in IEEE-754 (2008) without having to consider any of the +difficult normalisation problems.

+

The main objective is that the implementation should be simple and +simple to understand and as close to IEEE-754 and SMTLIB as possible +(as opposed to fast) since the main use is the validation of other +IEEE float implementations in SMT solvers (which have to be +fast). It is also not a replacement for libraries such as MPFR +(which is fast, but complicated and does not totally map onto IEEE +floats).

+
+
+class mpf.floats.MPF(eb, sb, bitvec=0)
+

Arbitrary precision IEEE-754 floating point number

+

eb is the number of bits for the exponent.

+

sb is the number of bits for the significand.

+

This includes the “hidden bit”, so for example to create a +single-precision floating point number we use:

+
>>> x = MPF(8, 24)
+
+
+

By default the created float is +0, however bitvec can be used +to set the initial value. The expected format is an integer +\(0 \le bitvec < 2^{eb+sb}\) corresponding to the binary +interchange format. For example to create the single precision +float representing +1:

+
>>> x = MPF(8, 24, 0x3f800000)
+>>> x.to_python_string()
+'1.0'
+
+
+
+
+__abs__()
+

Compute absolute value

+
+ +
+
+__eq__(other)
+

Test floating-point equality

+

Note that this is floating-point equality, so comparisons to +NaN always fail and -0 and +0 are considered equal.

+

If you want true equality, use smtlib_eq()

+
+ +
+
+__ge__(other)
+

Test floating-point greater than or equal

+
+ +
+
+__gt__(other)
+

Test floating-point greater than

+
+ +
+
+__le__(other)
+

Test floating-point less than or equal

+
+ +
+
+__lt__(other)
+

Test floating-point less than

+
+ +
+
+__neg__()
+

Compute inverse

+
+ +
+
+__weakref__
+

list of weak references to the object (if defined)

+
+ +
+
+compatible(other)
+

Test if another MPF has the same precision

+
+ +
+
+from_rational(rm, q)
+

Convert from rational to MPF

+

Sets the value to the nearest representable floating-point +value described by q, rounded according to rm.

+
+ +
+
+isFinite()
+

Test if value is finite

+

Returns true for zero, subnormals, or normal numbers.

+

Returns false for infinities, and not a number.

+
+ +
+
+isInfinite()
+

Test if value is infinite

+
+ +
+
+isIntegral()
+

Test if value is integral

+

Returns true if the floating-point value is an integer, and +false in all other cases (including infinities and not a +number).

+
+ +
+
+isNaN()
+

Test if value is not a number

+
+ +
+
+isNegative()
+

Test if value is negative

+

Returns always false for NaN.

+
+ +
+
+isNormal()
+

Test if value is normal

+
+ +
+
+isPositive()
+

Test if value is positive

+

Returns always false for NaN.

+
+ +
+
+isSubnormal()
+

Test if value is subnormal

+
+ +
+
+isZero()
+

Test if value is zero

+
+ +
+
+new_mpf()
+

Copy constructor

+

Returns a new MPF with the same precision and value.

+
+ +
+
+pack(S, E, T)
+

Pack sign, exponent, and significand

+

Sets the value of the floating point number, such that

+

The sign corresponds to S, the exponent is E, and the +significand is T.

+

This is the inverse of unpack().

+
+ +
+
+set_infinite(sign)
+

Set value to infinite with the given sign bit

+
+ +
+
+set_nan()
+

Set value to NaN

+
+ +
+
+set_sign_bit(sign)
+

Set sign bit

+
+ +
+
+set_zero(sign)
+

Set value to zero with the given sign bit

+
+ +
+
+smtlib_from_binary_interchange()
+

SMT-LIB function for converting from bitvector

+
+ +
+
+smtlib_from_float()
+

SMT-LIB function for converting from FloatingPoint

+
+ +
+
+smtlib_from_int()
+

SMT-LIB function for converting from Int

+
+ +
+
+smtlib_from_real()
+

SMT-LIB function for converting from Real

+
+ +
+
+smtlib_from_sbv()
+

SMT-LIB function for converting from signed bitvector

+
+ +
+
+smtlib_from_ubv()
+

SMT-LIB function for converting from unsigned bitvector

+
+ +
+
+smtlib_literal()
+

Return an SMT-LIB literal

+

Favours special cases, such as (_ +zero 8 24), otherwise +returns literals of the form (fp ...).

+
+ +
+
+smtlib_literals()
+

Return list of all possible SMTLIB literals

+

Includes:

+
    +
  • Binary interchange conversion, e.g. ((_ to_fp 8 24) #x00000000)
    • +
  • FP literal, e.g. (fp #b0 #b00 #b000)
    • +
  • Special value, e.g. (_ +zero 2 4)
    • +
+
+ +
+
+smtlib_random_literal()
+

Return an SMT-LIB literal (randomly chosen)

+

Chooses randomly from smtlib_literals().

+
+ +
+
+smtlib_sort()
+

SMT-LIB sort

+

Returns “Float16”, “Float32”, “Float64”, or “Float128” if +possible.

+

Returns “(_ FloatingPoint eb sb)” otherwise.

+
+ +
+
+smtlib_to_int()
+

SMT-LIB function for converting to Int

+
+ +
+
+smtlib_to_real()
+

SMT-LIB function for converting to Real

+
+ +
+
+to_int(rm)
+

Convert from MPF to Python int`

+

Raises AssertionError for infinities and NaN. Returns the +integer closest to the floating point, rounded according to +rm.

+
+ +
+
+to_python_float()
+

Convert from MPF to Python float`

+

Convert to python float. Do not rely on this to be precise for +now.

+
+

Todo

+

Use sys.float_info to first convert to the correct +format and then directly interpret the bit-pattern.

+
+

If you want something precise, then use +to_python_string() instead.

+
+ +
+
+to_python_string()
+

Convert from MPF to Python string`

+

Return a string describing the float. We return a decimal +string (e.g. ‘0.25’), except for the following special cases: +‘-0’, ‘Infinity’, ‘-Infinity’, and ‘NaN’.

+

The decimal string might be very long (but precise), so if you +want something compact then to_python_float() might be +more appropriate.

+
+ +
+
+to_rational()
+

Convert from MPF to Rational

+

Raises AssertionError for infinities or NaN.

+
+ +
+
+unpack()
+

Unpack into sign, exponent, and significand

+

Returns a tuple of integers (S, E, T) where S is the sign +bit, E is the exponent, and T is the significand.

+

This is the inverse of pack().

+
+ +
+
mpf.floats.fp_add(rm, left, right)

Floating-point addition

Performs a correctly rounded \(left + right\). The following special cases apply:

-
    -

  • NaN propagates

    -
    • -

  • Adding opposite infinities results in NaN, otherwise infinities propagate

    -
    • -

  • If the precise result is exactly 0 then we special case -according to Section 6.3 in IEEE-754:

    -
    -
      +
        +
      • NaN propagates
        • +
      • Adding opposite infinities results in NaN, otherwise infinities propagate
        • +
      • If the precise result is exactly 0 (i.e. 0 + 0 or a + -a) then we +special case according to Section 6.3 in IEEE-754:
        • we preserve the sign if left and right have the same sign
        • otherwise, we return -0 if the rounding mode is RTN
        • otherwise, we return +0
        -
+
+
+mpf.floats.fp_div(rm, left, right)
+

Floating-point division

+

Performs a correctly rounded \(left \div right\). The +following special cases apply:

+
    +
  • NaN propagates
    • +
  • When dividing by infinity
      +
    • NaN when dividing two infinities
      • +
    • 0 otherwise
      • +
    +
    • +
  • When dividing by zero
      +
    • NaN when dividing zero by zero
      • +
    • Infinity otherwise
      • +
    +
    • +
+
+ +
+
+mpf.floats.fp_fma(rm, x, y, z)
+

Floating-point fused multiply add

+

Performs a correctly rounded \(x * y + z\). The special cases +of fp_mul() and fp_add() apply, and in addition:

+
    +
  • On a precise 0 result the sign of zero is:
      +
    • Preserved if the sign of x * y is the same as z
      • +
    • -0 for RTN
      • +
    • +0 otherwise
      • +
    +
    • +
+
+ +
+
+mpf.floats.fp_from_float(eb, sb, rm, op)
+

Conversion from MPF to MPF (of a different precision)

+
+ +
+
+mpf.floats.fp_from_int(eb, sb, rm, op)
+

Conversion from Python integer to MPF

+
+ +
+
+mpf.floats.fp_from_sbv(eb, sb, rm, op)
+

Conversion from signed bitvector to MPF

+
+ +
+
+mpf.floats.fp_from_ubv(eb, sb, rm, op)
+

Conversion from unsigned bitvector to MPF

+
+ +
+
+mpf.floats.fp_max(left, right)
+

Floating-point maximum

+
+ +
+
+mpf.floats.fp_min(left, right)
+

Floating-point minimum

+
+ +
+
+mpf.floats.fp_mul(rm, left, right)
+

Floating-point multiplication

+

Performs a correctly rounded \(left * right\). The following +special cases apply:

+
    +
  • NaN propagates
    • +
  • Infinities propagate (for non-zero operands)
    • +
  • Multiplying by zero gives the following results
      +
    • NaN if the other operand is infinite
      • +
    • 0 of the same sign as the 0 operand
      • +
    +
    • +
+
+ +
+
+mpf.floats.fp_nextDown(op)
+

Floating-point predecessor

+
+ +
+
+mpf.floats.fp_nextUp(op)
+

Floating-point successor

+
+ +
+
+mpf.floats.fp_rem(left, right)
+

Floating-point remainder

+
+ +
+
+mpf.floats.fp_roundToIntegral(rm, op)
+

Floating-point round to integer

+
+ +
+
+mpf.floats.fp_sqrt(rm, op)
+

Floating-point square root

+
+ +
+
+mpf.floats.fp_sub(rm, left, right)
+

Floating-point substraction

+

Performs a correctly rounded \(left - right\), which is +equivalent to \(left + -right\).

+

See fp_add() for special cases.

+
+ +
+
+mpf.floats.fp_to_int(rm, op)
+

Conversion from MPF to Python integer

+
+ +
+
+mpf.floats.fp_to_sbv(op, rm, width)
+

Conversion from MPF to signed bitvector

+
+ +
+
+mpf.floats.fp_to_ubv(op, rm, width)
+

Conversion from MPF to unsigned bitvector

+
+ +
+
+mpf.floats.smtlib_eq(left, right)
+

Bit-wise equality

+
+
@@ -89,6 +783,7 @@

PyMPF

Table Of Contents

diff --git a/docs/objects.inv b/docs/objects.inv index c18ab1c..bd25c1b 100644 Binary files a/docs/objects.inv and b/docs/objects.inv differ diff --git a/docs/py-modindex.html b/docs/py-modindex.html index 2532f57..0e236d5 100644 --- a/docs/py-modindex.html +++ b/docs/py-modindex.html @@ -72,6 +72,11 @@

Python Module Index

    mpf.floats + + +     + mpf.rationals + diff --git a/docs/searchindex.js b/docs/searchindex.js index f599677..9c5711d 100644 --- a/docs/searchindex.js +++ b/docs/searchindex.js @@ -1 +1 @@ -Search.setIndex({envversion:50,filenames:["index"],objects:{"mpf.floats":{fp_add:[0,1,1,""]},mpf:{floats:[0,0,0,"-"]}},objnames:{"0":["py","module","Python module"],"1":["py","function","Python function"]},objtypes:{"0":"py:module","1":"py:function"},terms:{"case":0,"float":0,"return":0,accord:0,adding:0,addit:0,appli:0,correctli:0,exactli:0,follow:0,fp_add:0,have:0,ieee:0,infin:0,left:0,mode:0,nan:0,opposit:0,otherwis:0,perform:0,point:0,precis:0,preserv:0,propag:0,result:0,right:0,round:0,rtn:0,same:0,section:0,sign:0,special:0},titles:["PyMPF"],titleterms:{mpf:0,pympf:0}}) \ No newline at end of file +Search.setIndex({envversion:50,filenames:["index"],objects:{"mpf.floats":{MPF:[0,1,1,""],fp_add:[0,4,1,""],fp_div:[0,4,1,""],fp_fma:[0,4,1,""],fp_from_float:[0,4,1,""],fp_from_int:[0,4,1,""],fp_from_sbv:[0,4,1,""],fp_from_ubv:[0,4,1,""],fp_max:[0,4,1,""],fp_min:[0,4,1,""],fp_mul:[0,4,1,""],fp_nextDown:[0,4,1,""],fp_nextUp:[0,4,1,""],fp_rem:[0,4,1,""],fp_roundToIntegral:[0,4,1,""],fp_sqrt:[0,4,1,""],fp_sub:[0,4,1,""],fp_to_int:[0,4,1,""],fp_to_sbv:[0,4,1,""],fp_to_ubv:[0,4,1,""],smtlib_eq:[0,4,1,""]},"mpf.floats.MPF":{__abs__:[0,2,1,""],__eq__:[0,2,1,""],__ge__:[0,2,1,""],__gt__:[0,2,1,""],__le__:[0,2,1,""],__lt__:[0,2,1,""],__neg__:[0,2,1,""],__weakref__:[0,3,1,""],compatible:[0,2,1,""],from_rational:[0,2,1,""],isFinite:[0,2,1,""],isInfinite:[0,2,1,""],isIntegral:[0,2,1,""],isNaN:[0,2,1,""],isNegative:[0,2,1,""],isNormal:[0,2,1,""],isPositive:[0,2,1,""],isSubnormal:[0,2,1,""],isZero:[0,2,1,""],new_mpf:[0,2,1,""],pack:[0,2,1,""],set_infinite:[0,2,1,""],set_nan:[0,2,1,""],set_sign_bit:[0,2,1,""],set_zero:[0,2,1,""],smtlib_from_binary_interchange:[0,2,1,""],smtlib_from_float:[0,2,1,""],smtlib_from_int:[0,2,1,""],smtlib_from_real:[0,2,1,""],smtlib_from_sbv:[0,2,1,""],smtlib_from_ubv:[0,2,1,""],smtlib_literal:[0,2,1,""],smtlib_literals:[0,2,1,""],smtlib_random_literal:[0,2,1,""],smtlib_sort:[0,2,1,""],smtlib_to_int:[0,2,1,""],smtlib_to_real:[0,2,1,""],to_int:[0,2,1,""],to_python_float:[0,2,1,""],to_python_string:[0,2,1,""],to_rational:[0,2,1,""],unpack:[0,2,1,""]},"mpf.rationals":{Rational:[0,1,1,""],q_from_decimal_fragments:[0,4,1,""],q_pow2:[0,4,1,""],q_round_rna:[0,4,1,""],q_round_rne:[0,4,1,""],q_round_rtn:[0,4,1,""],q_round_rtp:[0,4,1,""],q_round_rtz:[0,4,1,""],q_round_to_nearest:[0,4,1,""]},"mpf.rationals.Rational":{__abs__:[0,2,1,""],__add__:[0,2,1,""],__eq__:[0,2,1,""],__ge__:[0,2,1,""],__gt__:[0,2,1,""],__le__:[0,2,1,""],__lt__:[0,2,1,""],__mul__:[0,2,1,""],__ne__:[0,2,1,""],__neg__:[0,2,1,""],__pow__:[0,2,1,""],__sub__:[0,2,1,""],__truediv__:[0,2,1,""],__weakref__:[0,3,1,""],isIntegral:[0,2,1,""],isNegative:[0,2,1,""],isZero:[0,2,1,""],to_decimal_string:[0,2,1,""],to_python_float:[0,2,1,""],to_python_int:[0,2,1,""],to_smtlib:[0,2,1,""]},mpf:{floats:[0,0,0,"-"],rationals:[0,0,0,"-"]}},objnames:{"0":["py","module","Python module"],"1":["py","class","Python class"],"2":["py","method","Python method"],"3":["py","attribute","Python attribute"],"4":["py","function","Python function"]},objtypes:{"0":"py:module","1":"py:class","2":"py:method","3":"py:attribute","4":"py:function"},terms:{"0x3f800000":0,"23e":0,"case":0,"class":0,"default":0,"float":0,"function":0,"int":0,"long":0,"new":0,"return":0,"true":0,__abs__:0,__add__:0,__eq__:0,__ge__:0,__gt__:0,__le__:0,__lt__:0,__mul__:0,__ne__:0,__neg__:0,__pow__:0,__sub__:0,__truediv__:0,__weakref__:0,absolut:0,accord:0,add:0,adding:0,addit:0,addition:0,all:0,allow:0,also:0,altern:0,alwai:0,ani:0,anoth:0,appli:0,appropri:0,arbitrari:0,assertionerror:0,awai:0,b000:0,b00:0,between:0,binari:0,bit:0,bitvec:0,bitvector:0,build:0,calcul:0,call:0,can:0,choos:0,chosen:0,close:0,closest:0,compact:0,comparison:0,compat:0,complic:0,comput:0,consid:0,constructor:0,convers:0,convert:0,copi:0,correct:0,correctli:0,correspond:0,creat:0,deal:0,decim:0,defin:0,denomin:0,describ:0,differ:0,difficult:0,directli:0,divid:0,divis:0,doe:0,equal:0,equaliti:0,equival:0,even:0,exactli:0,exampl:0,except:0,exp_part:0,expect:0,expon:0,exponenti:0,express:0,fail:0,fals:0,fast:0,favour:0,finit:0,first:0,float128:0,float16:0,float32:0,float64:0,float_info:0,floatingpoint:0,follow:0,form:0,format:0,fp_add:0,fp_div:0,fp_fma:0,fp_from_float:0,fp_from_int:0,fp_from_sbv:0,fp_from_ubv:0,fp_max:0,fp_min:0,fp_mul:0,fp_nextdown:0,fp_nextup:0,fp_rem:0,fp_roundtointegr:0,fp_sqrt:0,fp_sub:0,fp_to_int:0,fp_to_sbv:0,fp_to_ubv:0,fraction:0,fraction_part:0,fragment:0,from:0,from_rat:0,fuse:0,give:0,given:0,greater:0,hand:0,handl:0,have:0,hidden:0,howev:0,ieee:0,implement:0,includ:0,include:0,inequal:0,infin:0,infinit:0,infiniti:0,initi:0,instead:0,integ:0,integer_part:0,integr:0,interchang:0,interpret:0,invers:0,isfinit:0,isinfinit:0,isintegr:0,isnan:0,isneg:0,isnorm:0,isposit:0,issubnorm:0,iszero:0,left:0,less:0,lib:0,librari:0,list:0,liter:0,lower:0,main:0,map:0,maximum:0,memori:0,might:0,minimum:0,mode:0,modul:0,more:0,mpfr:0,multipl:0,multipli:0,must:0,nan:0,nearest:0,neg:0,negat:0,new_mpf:0,non:0,normal:0,normalis:0,note:0,now:0,number:0,numer:0,object:0,onto:0,operand:0,oppos:0,opposit:0,other:0,otherwis:0,pack:0,pattern:0,perform:0,plu:0,point:0,posit:0,possibl:0,precis:0,predecessor:0,preserv:0,problem:0,propag:0,python:0,q_from_decimal_frag:0,q_pow2:0,q_round_rn:0,q_round_rna:0,q_round_rtn:0,q_round_rtp:0,q_round_rtz:0,q_round_to_nearest:0,rais:0,randomli:0,real:0,refer:0,reli:0,remaind:0,replac:0,repres:0,represent:0,result:0,right:0,root:0,round:0,rtn:0,same:0,section:0,see:0,semant:0,set:0,set_infinit:0,set_nan:0,set_sign_bit:0,set_zero:0,should:0,side:0,sign:0,significand:0,simpl:0,sinc:0,singl:0,smt:0,smtlib:0,smtlib_eq:0,smtlib_from_binary_interchang:0,smtlib_from_float:0,smtlib_from_int:0,smtlib_from_r:0,smtlib_from_sbv:0,smtlib_from_ubv:0,smtlib_liter:0,smtlib_random_liter:0,smtlib_sort:0,smtlib_to_int:0,smtlib_to_r:0,solver:0,someth:0,sort:0,special:0,squar:0,string:0,subclass:0,subnorm:0,substract:0,successor:0,termin:0,test:0,than:0,thi:0,thrown:0,tiebreak:0,to_decimal_str:0,to_fp:0,to_int:0,to_python_float:0,to_python_int:0,to_python_str:0,to_rat:0,to_smtlib:0,total:0,toward:0,tupl:0,two:0,understand:0,unpack:0,unsign:0,upper:0,use:0,valid:0,valu:0,veri:0,want:0,weak:0,when:0,where:0,which:0,width:0,wise:0,without:0,x00000000:0,you:0,zero:0},titles:["PyMPF"],titleterms:{mpf:0,pympf:0,ration:0,todo:0}}) \ No newline at end of file diff --git a/index.rst b/index.rst index f4d8499..beabcd0 100644 --- a/index.rst +++ b/index.rst @@ -5,9 +5,18 @@ PyMPF .. toctree:: :maxdepth: 2 +========= +Rationals +========= + +.. automodule:: mpf.rationals + :members: + :special-members: + === MPF === .. automodule:: mpf.floats :members: + :special-members: diff --git a/mpf/floats.py b/mpf/floats.py index aec8ff9..c09f484 100644 --- a/mpf/floats.py +++ b/mpf/floats.py @@ -24,19 +24,21 @@ ## ## ############################################################################## -# This module implements IEEE floats using bitvectors as the in-memory -# format, but rationals (plus rounding and special case handling) for -# calculation. This allows us to directly implement the semantics -# described in IEEE-754 (2008) without having to consider any of the -# difficult normalisation problems. -# -# The main objective is that the implementation should be simple and -# simple to understand and as close to IEEE-754 and SMTLIB as possible -# (as opposed to fast) since the main use is the validation of other -# IEEE float implementations in SMT solvers (which have to be -# fast). It is also not a replacement for libraries such as MPFR -# (which is fast, but complicated and does not totally map onto IEEE -# floats). +""" +This module implements IEEE floats using bitvectors as the in-memory +format, but rationals (plus rounding and special case handling) for +calculation. This allows us to directly implement the semantics +described in IEEE-754 (2008) without having to consider any of the +difficult normalisation problems. + +The main objective is that the implementation should be simple and +simple to understand and as close to IEEE-754 and SMTLIB as possible +(as opposed to fast) since the main use is the validation of other +IEEE float implementations in SMT solvers (which have to be +fast). It is also not a replacement for libraries such as MPFR +(which is fast, but complicated and does not totally map onto IEEE +floats). +""" # TODO: Implement RNA in intervals @@ -63,7 +65,30 @@ class Unspecified(Exception): RM_RTN = "RTN" RM_RTZ = "RTZ" -class MPF(object): +class MPF: + """Arbitrary precision IEEE-754 floating point number + + *eb* is the number of bits for the exponent. + + *sb* is the number of bits for the significand. + + This includes the "hidden bit", so for example to create a + single-precision floating point number we use: + + >>> x = MPF(8, 24) + + By default the created float is +0, however *bitvec* can be used + to set the initial value. The expected format is an integer + :math:`0 \le bitvec < 2^{eb+sb}` corresponding to the binary + interchange format. For example to create the single precision + float representing +1: + + >>> x = MPF(8, 24, 0x3f800000) + >>> x.to_python_string() + '1.0' + + """ + ROUNDING_MODES = (RM_RNE, RM_RNA, RM_RTP, RM_RTN, RM_RTZ) ROUNDING_MODES_NEAREST = (RM_RNE, RM_RNA) ROUNDING_MODES_DIRECTED = (RM_RTP, RM_RTN, RM_RTZ) @@ -87,20 +112,37 @@ def __init__(self, eb, sb, bitvec=0): self.bv = bitvec + def __repr__(self): + return "MPF(%u, %u, 0x%x)" % (self.w, self.p, self.bv) + ###################################################################### # Constructors def new_mpf(self): + """Copy constructor + + Returns a new MPF with the same precision and value. + """ return MPF(self.w, self.p, self.bv) ###################################################################### # Internal utilities def compatible(self, other): + """Test if another MPF has the same precision""" return (self.w == other.w and self.p == other.p) def unpack(self): + """Unpack into sign, exponent, and significand + + Returns a tuple of integers (S, E, T) where *S* is the sign + bit, *E* is the exponent, and *T* is the significand. + + This is the inverse of :func:`pack`. + + """ + # TODO: remove ugly hack to convert via strings bits = "{0:b}".format(self.bv) assert len(bits) <= self.k @@ -113,6 +155,16 @@ def unpack(self): return (S, E, T) def pack(self, S, E, T): + """Pack sign, exponent, and significand + + Sets the value of the floating point number, such that + + The sign corresponds to *S*, the exponent is *E*, and the + significand is *T*. + + This is the inverse of :func:`unpack`. + + """ assert 0 <= S <= 1 assert 0 <= E <= 2 ** self.w - 1 assert 0 <= T <= 2 ** self.t - 1 @@ -142,6 +194,12 @@ def inf_boundary(self): return inf.to_python_int() def from_rational(self, rm, q): + """Convert from rational to MPF + + Sets the value to the nearest representable floating-point + value described by *q*, rounded according to *rm*. + + """ assert rm in MPF.ROUNDING_MODES inf = Rational(self.inf_boundary()) @@ -255,6 +313,10 @@ def from_rational(self, rm, q): self.set_sign_bit(sign) def to_rational(self): + """Convert from MPF to :class:`.Rational` + + Raises AssertionError for infinities or NaN. + """ S, E, T = self.unpack() if E == 2 ** self.w - 1: @@ -280,6 +342,13 @@ def to_rational(self): return v def to_int(self, rm): + """Convert from MPF to Python int` + + Raises AssertionError for infinities and NaN. Returns the + integer closest to the floating point, rounded according to + *rm*. + + """ assert rm in MPF.ROUNDING_MODES assert self.isFinite() @@ -289,6 +358,17 @@ def to_int(self, rm): return q.a def to_python_float(self): + """Convert from MPF to Python float` + + Convert to python float. Do not rely on this to be precise for + now. + + .. todo:: Use sys.float_info to first convert to the correct + format and then directly interpret the bit-pattern. + + If you want something precise, then use + :func:`to_python_string` instead. + """ if self.isNaN(): return float("NaN") elif self.isInfinite(): @@ -300,6 +380,17 @@ def to_python_float(self): return self.to_rational().to_python_float() def to_python_string(self): + """Convert from MPF to Python string` + + Return a string describing the float. We return a decimal + string (e.g. '0.25'), except for the following special cases: + '-0', 'Infinity', '-Infinity', and 'NaN'. + + The decimal string might be very long (but precise), so if you + want something compact then :func:`to_python_float` might be + more appropriate. + + """ if self.isNaN(): return "NaN" elif self.isInfinite(): @@ -316,19 +407,22 @@ def to_python_string(self): # Setters def set_zero(self, sign): + """Set value to zero with the given sign bit""" assert 0 <= sign <= 1 self.pack(sign, 0, 0) def set_infinite(self, sign): + """Set value to infinite with the given sign bit""" assert 0 <= sign <= 1 self.pack(sign, 2 ** self.w - 1, 0) def set_nan(self): + """Set value to NaN""" self.pack(1, 2 ** self.w - 1, 2 ** self.t - 1) def set_sign_bit(self, sign): - assert type(sign) is bool - + """Set sign bit""" + assert 0 <= sign <= 1 S, E, T = self.unpack() S = (1 if sign else 0) self.pack(S, E, T) @@ -367,6 +461,7 @@ def __str__(self): return rv def __abs__(self): + """Compute absolute value""" rv = self.new_mpf() S, E, T = rv.unpack() if not rv.isNaN(): @@ -375,6 +470,7 @@ def __abs__(self): return rv def __neg__(self): + """Compute inverse""" rv = self.new_mpf() S, E, T = rv.unpack() if not rv.isNaN(): @@ -383,6 +479,7 @@ def __neg__(self): return rv def __le__(self, other): + """Test floating-point less than or equal""" assert self.compatible(other) if self.isNaN() or other.isNaN(): return False @@ -390,6 +487,7 @@ def __le__(self, other): return self.partial_order() <= other.partial_order() def __lt__(self, other): + """Test floating-point less than""" assert self.compatible(other) if self.isNaN() or other.isNaN(): return False @@ -397,6 +495,7 @@ def __lt__(self, other): return self.partial_order() < other.partial_order() def __ge__(self, other): + """Test floating-point greater than or equal""" assert self.compatible(other) if self.isNaN() or other.isNaN(): return False @@ -404,6 +503,7 @@ def __ge__(self, other): return self.partial_order() >= other.partial_order() def __gt__(self, other): + """Test floating-point greater than""" assert self.compatible(other) if self.isNaN() or other.isNaN(): return False @@ -411,6 +511,14 @@ def __gt__(self, other): return self.partial_order() > other.partial_order() def __eq__(self, other): + """Test floating-point equality + + Note that this is floating-point equality, so comparisons to + NaN always fail and -0 and +0 are considered equal. + + If you want true equality, use :func:`smtlib_eq` + + """ assert self.compatible(other) if self.isNaN() or other.isNaN(): return False @@ -421,37 +529,63 @@ def __eq__(self, other): # Queries def isZero(self): + """Test if value is zero""" S, E, T = self.unpack() return E == 0 and T == 0 def isSubnormal(self): + """Test if value is subnormal""" S, E, T = self.unpack() return E == 0 and T != 0 def isNormal(self): + """Test if value is normal""" S, E, T = self.unpack() return 1 <= E <= 2 ** self.w - 2 def isNaN(self): + """Test if value is not a number""" S, E, T = self.unpack() return E == 2 ** self.w - 1 and T != 0 def isInfinite(self): + """Test if value is infinite""" S, E, T = self.unpack() return E == 2 ** self.w - 1 and T == 0 def isPositive(self): + """Test if value is positive + + Returns always false for NaN. + """ S, E, T = self.unpack() return not self.isNaN() and S == 0 def isNegative(self): + """Test if value is negative + + Returns always false for NaN. + """ S, E, T = self.unpack() return not self.isNaN() and S == 1 def isFinite(self): + """Test if value is finite + + Returns true for zero, subnormals, or normal numbers. + + Returns false for infinities, and not a number. + """ return self.isZero() or self.isSubnormal() or self.isNormal() def isIntegral(self): + """Test if value is integral + + Returns true if the floating-point value is an integer, and + false in all other cases (including infinities and not a + number). + """ + if self.isFinite(): return self.to_rational().isIntegral() else: @@ -461,6 +595,14 @@ def isIntegral(self): # SMTLIB support def smtlib_sort(self): + """SMT-LIB sort + + Returns "Float16", "Float32", "Float64", or "Float128" if + possible. + + Returns "(_ FloatingPoint *eb* *sb*)" otherwise. + + """ if self.w == 5 and self.p == 11: return "Float16" elif self.w == 8 and self.p == 24: @@ -473,30 +615,46 @@ def smtlib_sort(self): return "(_ FloatingPoint %u %u)" % (self.w, self.p) def smtlib_from_binary_interchange(self): + """SMT-LIB function for converting from bitvector""" return "(_ to_fp %u %u)" % (self.w, self.p) def smtlib_from_float(self): + """SMT-LIB function for converting from FloatingPoint""" return "(_ to_fp %u %u)" % (self.w, self.p) def smtlib_from_real(self): + """SMT-LIB function for converting from Real""" return "(_ to_fp %u %u)" % (self.w, self.p) def smtlib_from_int(self): + """SMT-LIB function for converting from Int""" return "(_ to_fp %u %u)" % (self.w, self.p) def smtlib_from_ubv(self): + """SMT-LIB function for converting from unsigned bitvector""" return "(_ to_fp_unsigned %u %u)" % (self.w, self.p) def smtlib_from_sbv(self): + """SMT-LIB function for converting from signed bitvector""" return "(_ to_fp %u %u)" % (self.w, self.p) def smtlib_to_real(self): + """SMT-LIB function for converting to Real""" return "fp.to_real" def smtlib_to_int(self): + """SMT-LIB function for converting to Int""" return "fp.to_int" def smtlib_literals(self): + """Return list of all possible SMTLIB literals + + Includes: + + * Binary interchange conversion, e.g. ((_ to_fp 8 24) #x00000000) + * FP literal, e.g. (fp #b0 #b00 #b000) + * Special value, e.g. (_ +zero 2 4) + """ choices = [] # Binary interchange @@ -539,9 +697,19 @@ def smtlib_literals(self): return choices def smtlib_literal(self): + """Return an SMT-LIB literal + + Favours special cases, such as (_ +zero 8 24), otherwise + returns literals of the form (fp ...). + + """ return self.smtlib_literals()[-1] def smtlib_random_literal(self): + """Return an SMT-LIB literal (randomly chosen) + + Chooses randomly from :func:`smtlib_literals`. + """ return random.choice(self.smtlib_literals()) def q_round(rm, n): @@ -560,17 +728,13 @@ def fp_add(rm, left, right): cases apply: * NaN propagates - * Adding opposite infinities results in NaN, otherwise infinities propagate + * If the precise result is exactly 0 (i.e. 0 + 0 or a + -a) then we + special case according to Section 6.3 in IEEE-754: - * If the precise result is exactly 0 then we special case - according to Section 6.3 in IEEE-754: - - * we preserve the sign if left and right have the same sign - - * otherwise, we return -0 if the rounding mode is RTN - - * otherwise, we return +0 + * we preserve the sign if left and right have the same sign + * otherwise, we return -0 if the rounding mode is RTN + * otherwise, we return +0 """ assert rm in MPF.ROUNDING_MODES @@ -606,6 +770,14 @@ def fp_add(rm, left, right): return rv def fp_sub(rm, left, right): + """Floating-point substraction + + Performs a correctly rounded :math:`left - right`, which is + equivalent to :math:`left + -right`. + + See :func:`fp_add` for special cases. + + """ assert rm in MPF.ROUNDING_MODES assert left.compatible(right) rv = left.new_mpf() # rv == left @@ -639,6 +811,19 @@ def fp_sub(rm, left, right): return rv def fp_mul(rm, left, right): + """Floating-point multiplication + + Performs a correctly rounded :math:`left * right`. The following + special cases apply: + + * NaN propagates + * Infinities propagate (for non-zero operands) + * Multiplying by zero gives the following results + + * NaN if the other operand is infinite + * 0 of the same sign as the 0 operand + + """ assert rm in MPF.ROUNDING_MODES assert left.compatible(right) sign = (1 if left.isNegative() ^ right.isNegative() else 0) @@ -660,6 +845,23 @@ def fp_mul(rm, left, right): return rv def fp_div(rm, left, right): + """Floating-point division + + Performs a correctly rounded :math:`left \div right`. The + following special cases apply: + + * NaN propagates + * When dividing by infinity + + * NaN when dividing two infinities + * 0 otherwise + + * When dividing by zero + + * NaN when dividing zero by zero + * Infinity otherwise + + """ assert rm in MPF.ROUNDING_MODES assert left.compatible(right) sign = (1 if left.isNegative() ^ right.isNegative() else 0) @@ -685,7 +887,17 @@ def fp_div(rm, left, right): return rv def fp_fma(rm, x, y, z): - # computes (x * y) + z + """Floating-point fused multiply add + + Performs a correctly rounded :math:`x * y + z`. The special cases + of :func:`fp_mul` and :func:`fp_add` apply, and in addition: + + * On a precise 0 result the sign of zero is: + + * Preserved if the sign of x * y is the same as z + * -0 for RTN + * +0 otherwise + """ assert rm in MPF.ROUNDING_MODES assert x.compatible(y) assert x.compatible(z) @@ -725,6 +937,7 @@ def fp_fma(rm, x, y, z): return rv def fp_sqrt(rm, op): + """Floating-point square root""" assert rm in MPF.ROUNDING_MODES # We can get away with approximating the square root to sufficient # precision because of Theorem 19 (p168) of the Handbook of @@ -779,6 +992,7 @@ def fp_sqrt(rm, op): return root def fp_rem(left, right): + """Floating-point remainder""" assert left.compatible(right) rv = left.new_mpf() @@ -798,6 +1012,7 @@ def fp_rem(left, right): return rv def fp_roundToIntegral(rm, op): + """Floating-point round to integer""" assert rm in MPF.ROUNDING_MODES rv = op.new_mpf() @@ -814,6 +1029,7 @@ def fp_roundToIntegral(rm, op): return rv def fp_min(left, right): + """Floating-point minimum""" assert left.compatible(right) if (left.isZero() and right.isZero() and left.isPositive() != right.isPositive()): @@ -827,6 +1043,7 @@ def fp_min(left, right): return left.new_mpf() def fp_max(left, right): + """Floating-point maximum""" assert left.compatible(right) if (left.isZero() and right.isZero() and left.isPositive() != right.isPositive()): @@ -840,10 +1057,12 @@ def fp_max(left, right): return left.new_mpf() def smtlib_eq(left, right): + """Bit-wise equality""" assert left.compatible(right) return (left.isNaN() and right.isNaN()) or (left.bv == right.bv) def fp_nextUp(op): + """Floating-point successor""" rv = op.new_mpf() if op.isNaN(): @@ -878,15 +1097,18 @@ def fp_nextUp(op): return rv def fp_nextDown(op): + """Floating-point predecessor""" # This is how it is defined in 5.3.1 return -fp_nextUp(-op) def fp_from_ubv(eb, sb, rm, op): + """Conversion from unsigned bitvector to MPF""" rv = MPF(eb, sb) rv.from_rational(rm, op.to_unsigned_int()) return rv def fp_to_ubv(op, rm, width): + """Conversion from MPF to unsigned bitvector""" if op.isInfinite() or op.isNaN(): raise Unspecified @@ -900,11 +1122,13 @@ def fp_to_ubv(op, rm, width): raise Unspecified def fp_from_sbv(eb, sb, rm, op): + """Conversion from signed bitvector to MPF""" rv = MPF(eb, sb) rv.from_rational(rm, op.to_signed_int()) return rv def fp_to_sbv(op, rm, width): + """Conversion from MPF to signed bitvector""" if op.isInfinite() or op.isNaN(): raise Unspecified @@ -919,12 +1143,14 @@ def fp_to_sbv(op, rm, width): # ((_ to_fp eb sb) rm op) def fp_from_int(eb, sb, rm, op): + """Conversion from Python integer to MPF""" rv = MPF(eb, sb) rv.from_rational(rm, Rational(op)) return rv # (fp.to_int rm op) def fp_to_int(rm, op): + """Conversion from MPF to Python integer""" if op.isInfinite() or op.isNaN(): raise Unspecified @@ -938,6 +1164,7 @@ def fp_to_int(rm, op): # is where you land when you read 5.4.2), but in 6.3 it says it # doesn't change. def fp_from_float(eb, sb, rm, op): + """Conversion from MPF to MPF (of a different precision)""" rv = MPF(eb, sb) if op.isNaN(): rv.set_nan() diff --git a/mpf/rationals.py b/mpf/rationals.py index b3c084e..1e4dd0a 100644 --- a/mpf/rationals.py +++ b/mpf/rationals.py @@ -23,12 +23,21 @@ ## ## ############################################################################## -# Todo: Make this a subclass of Fraction instead of re-inventing the -# wheel. +""" +This module defines class to deal with Rational numbers. + +.. todo:: This should be a subclass of fractions.Fraction. +""" import fractions class Rational(object): + """Rational number + + *a* is the numerator + + *b* is the denominator + """ def __init__(self, a=0, b=1): assert type(a) is int assert type(b) is int @@ -45,22 +54,31 @@ def __init__(self, a=0, b=1): assert type(self.b) is int def __mul__(self, other): + """Multiplication""" return Rational(self.a*other.a, self.b*other.b) def __truediv__(self, other): + """Division""" return Rational(self.a*other.b, self.b*other.a) def __add__(self, other): + """Addition""" return Rational(self.a*other.b + other.a*self.b, self.b*other.b) def __sub__(self, other): + """Substraction""" return Rational(self.a*other.b - other.a*self.b, self.b*other.b) def __pow__(self, other): + """Exponentiation + + The right-hand side must be an integral Rational, otherwise + AssertionError is raised. + """ assert other.isIntegral() a = fractions.Fraction(self.a, self.b) @@ -69,9 +87,11 @@ def __pow__(self, other): return Rational(p.numerator, p.denominator) def __abs__(self): + """Absolute value""" return Rational(abs(self.a), self.b) def __neg__(self): + """Negation""" return Rational(-self.a, self.b) def __repr__(self): @@ -81,40 +101,60 @@ def __repr__(self): return "Rational(%i, %u)" % (self.a, self.b) def __lt__(self, other): + """<""" return self.a*other.b < other.a*self.b def __le__(self, other): + """<=""" return self.a*other.b <= other.a*self.b def __eq__(self, other): + """Equality""" return self.a*other.b == other.a*self.b def __ne__(self, other): + """Inequality""" return self.a*other.b != other.a*self.b def __gt__(self, other): + """>""" return self.a*other.b > other.a*self.b def __ge__(self, other): + """>=""" return self.a*other.b >= other.a*self.b def isZero(self): + """Test if zero""" return self.a == 0 def isNegative(self): + """Test if negative + + Returns false for 0. + """ return self.a < 0 def isIntegral(self): + """Test if integral""" return (self.a % self.b) == 0 def to_python_int(self): + """Convert to python int""" assert self.isIntegral() return self.a def to_python_float(self): + """Convert to python float""" return float(fractions.Fraction(self.a, self.b)) def to_smtlib(self): + """Convert to SMT-LIB Real expression + + Returns literal for integrals, e.g. "1.0". + + Returns an s-expression otherwise, e.g. "(- (/ 1.0 3.0))". + """ tmp = "%u.0" % abs(self.a) if self.b != 1: tmp = "(/ %s %u.0)" % (tmp, self.b) @@ -123,6 +163,12 @@ def to_smtlib(self): return tmp def to_decimal_string(self): + """Convert to decimal string + + If the fraction does not terminate (e.g. for 1 / 3), an + exception is thrown. + + """ if self.b > 2: b = self.b while b > 1: @@ -154,12 +200,24 @@ def to_decimal_string(self): return rv def q_pow2(n): + """Create rational for 2^n + + *n* can be negative + """ if n >= 0: return Rational(2**n) else: return Rational(1, 2**(-n)) def q_round_to_nearest(n, tiebreak): + """Round to nearest integer + + Round *n* to the nearest integer + + Calls the *tiebreak*(upper, lower) function with the two + alternatives if *n* is precisely between two integers. + + """ lower = (n.a - (n.a % n.b)) / n.b upper = lower + 1 assert Rational(lower) <= n <= Rational(upper) @@ -172,6 +230,7 @@ def q_round_to_nearest(n, tiebreak): return Rational(tiebreak(lower, upper)) def q_round_rne(n): + """Round to nearest even integer""" def tiebreak(lower, upper): if lower % 2 == 0: return lower @@ -181,6 +240,7 @@ def tiebreak(lower, upper): return q_round_to_nearest(n, tiebreak) def q_round_rna(n): + """Round to nearest integer, away from zero""" def tiebreak(lower, upper): if abs(lower) > abs(upper): return lower @@ -189,6 +249,7 @@ def tiebreak(lower, upper): return q_round_to_nearest(n, tiebreak) def q_round_rtz(n): + """Round to nearest integer, towards zero""" i = Rational(abs(n.a) / n.b) if n.isNegative(): return -i @@ -196,6 +257,7 @@ def q_round_rtz(n): return i def q_round_rtp(n): + """Round to nearest integer, towards positive""" if n.isIntegral(): return n i = abs(n.a) / n.b @@ -205,6 +267,7 @@ def q_round_rtp(n): return Rational(i + 1) def q_round_rtn(n): + """Round to nearest integer, towards negative""" if n.isIntegral(): return n i = abs(n.a) / n.b @@ -214,8 +277,7 @@ def q_round_rtn(n): return Rational(i) def q_from_decimal_fragments(sign, integer_part, fraction_part, exp_part): - """ - Build a rational from fragments of a decimal number. + """Build a rational from string fragments of a decimal number. E.g. for "1.23E-1" we have fragments for sign = ""