mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Fixed Python 3.x issues.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-28 14:19:23 +00:00
parent eff776acd9
commit 15be8d424c
1 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/api/python/z3num.py
View file

@ -165,11 +165,12 @@ class Numeral:
def as_long(self): def as_long(self):
""" Return a numeral (that is an integer) as a Python long. """ Return a numeral (that is an integer) as a Python long.
>>> (Numeral(10)**20).as_long()
100000000000000000000L
""" """
assert(self.is_integer()) assert(self.is_integer())
return long(Z3_get_numeral_string(self.ctx_ref(), self.as_ast())) if sys.version_info[0] >= 3:
return int(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
else:
return long(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
def as_fraction(self): def as_fraction(self):
""" Return a numeral (that is a rational) as a Python Fraction. """ Return a numeral (that is a rational) as a Python Fraction.
@ -345,6 +346,9 @@ class Numeral:
""" """
return Numeral(Z3_algebraic_div(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx) return Numeral(Z3_algebraic_div(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx)
def __truediv__(self, other):
return self.__div__(other)
def __rdiv__(self, other): def __rdiv__(self, other):
""" Return the numeral `other / self`. """ Return the numeral `other / self`.
>>> 3 / Numeral(2) >>> 3 / Numeral(2)
@ -354,6 +358,9 @@ class Numeral:
""" """
return Numeral(Z3_algebraic_div(self.ctx_ref(), _to_numeral(other, self.ctx).ast, self.ast), self.ctx) return Numeral(Z3_algebraic_div(self.ctx_ref(), _to_numeral(other, self.ctx).ast, self.ast), self.ctx)
def __rtruediv__(self, other):
return self.__rdiv__(other)
def root(self, k): def root(self, k):
""" Return the numeral `self^(1/k)`. """ Return the numeral `self^(1/k)`.