From a51c6d125de4b28a389474cbd75ca3d4095a4f47 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Dec 2012 13:39:34 -0800 Subject: [PATCH] Add support for Python Fraction object Signed-off-by: Leonardo de Moura --- src/api/python/z3.py | 10 ++++++++++ src/api/python/z3num.py | 9 +++++++++ 2 files changed, 19 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 9b1d5f1f0..c138bcd62 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -44,6 +44,7 @@ from z3core import * from z3types import * from z3consts import * from z3printer import * +from fractions import Fraction import sys import io @@ -2523,6 +2524,15 @@ class RatNumRef(ArithRef): """ return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) + def as_fraction(self): + """Return a Z3 rational as a Python Fraction object. + + >>> v = RealVal("1/5") + >>> v.as_fraction() + Fraction(1, 5) + """ + return Fraction(self.numerator_as_long(), self.denominator_as_long()) + class AlgebraicNumRef(ArithRef): """Algebraic irrational values.""" diff --git a/src/api/python/z3num.py b/src/api/python/z3num.py index 581536e44..75cabbb27 100644 --- a/src/api/python/z3num.py +++ b/src/api/python/z3num.py @@ -8,6 +8,7 @@ from z3 import * from z3core import * from z3printer import * +from fractions import Fraction def _to_numeral(num, ctx=None): if isinstance(num, Numeral): @@ -170,6 +171,14 @@ class Numeral: assert(self.is_integer()) return long(Z3_get_numeral_string(self.ctx_ref(), self.as_ast())) + def as_fraction(self): + """ Return a numeral (that is a rational) as a Python Fraction. + >>> Numeral("1/5").as_fraction() + Fraction(1, 5) + """ + assert(self.is_rational()) + return Fraction(self.numerator().as_long(), self.denominator().as_long()) + def approx(self, precision=10): """Return a numeral that approximates the numeral `self`. The result `r` is such that |r - self| <= 1/10^precision