Add support for Python Fraction object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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."""
 

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