55 lines
1.5 KiB
Python
55 lines
1.5 KiB
Python
from collections.abc import Callable
|
|
from gmpy2 import mpq
|
|
|
|
MAX_BITS = 32
|
|
|
|
class REAL:
|
|
# x = z + sum(2 ** -(i + 1) for i in A)
|
|
# Needed arguments: z in Q and A subset N
|
|
def __init__(self, z: int, f: Callable[[int], bool]):
|
|
self.decide = f
|
|
self.const = z
|
|
|
|
@staticmethod
|
|
def __long_division(p: int, q: int, bits: int = MAX_BITS) -> list[int]:
|
|
bnry = []
|
|
rem = p % q
|
|
|
|
for i in range(bits):
|
|
# Fill with 0 when finished
|
|
if rem == 0:
|
|
bnry.extend([0] * (bits - len(bnry)))
|
|
break
|
|
|
|
# Shift remainder left by 1 bit
|
|
rem *= 2 # Shift <=> Doubling
|
|
|
|
# Determine bit value
|
|
if rem >= q:
|
|
bnry.append(1)
|
|
rem -= q
|
|
else:
|
|
bnry.append(0)
|
|
return bnry
|
|
|
|
@staticmethod
|
|
def from_int(x: int):
|
|
return REAL(z=x, f=lambda i: False)
|
|
|
|
@staticmethod
|
|
def from_rational(x: mpq):
|
|
quot = x.numerator // x.denominator
|
|
rem = x.numerator % x.denominator
|
|
|
|
bnry = REAL.__long_division(rem, x.denominator)
|
|
decide = lambda n: (0 <= n < len(bnry) and bnry[n] == 1)
|
|
return REAL(z=quot, f=decide)
|
|
|
|
|
|
def as_str(self, n: int) -> str:
|
|
bnry_str = ''
|
|
for i in range(n):
|
|
bnry_str += '1' if self.decide(i) else '0'
|
|
# Binary depiction of z not applied here
|
|
return f"x = {self.const} + {bnry_str}"
|