Z3 |

Public Member Functions
RatNumRef Class Reference
Inheritance diagram for RatNumRef:

## Public Member Functions
def | numerator (self)
def | denominator (self)
def | numerator_as_long (self)
def | denominator_as_long (self)
def | is_int (self)
def | is_real (self)
def | is_int_value (self)
def | as_long (self)
def | as_decimal (self, prec)
def | as_string (self)
def | as_fraction (self)
Public Member Functions inherited from ArithRef
def | sort (self)
def | is_int (self)
def | is_real (self)
def | __add__ (self, other)
def | __radd__ (self, other)
def | __mul__ (self, other)
def | __rmul__ (self, other)
def | __sub__ (self, other)
def | __rsub__ (self, other)
def | __pow__ (self, other)
def | __rpow__ (self, other)
def | __div__ (self, other)
def | __truediv__ (self, other)
def | __rdiv__ (self, other)
def | __rtruediv__ (self, other)
def | __mod__ (self, other)
def | __rmod__ (self, other)
def | __neg__ (self)
def | __pos__ (self)
def | __le__ (self, other)
def | __lt__ (self, other)
def | __gt__ (self, other)
def | __ge__ (self, other)
Public Member Functions inherited from ExprRef
def | as_ast (self)
def | get_id (self)
def | sort (self)
def | sort_kind (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __ne__ (self, other)
def | params (self)
def | decl (self)
def | num_args (self)
def | arg (self, idx)
def | children (self)
Public Member Functions inherited from AstRef
def | __init__ (self, ast, ctx=None)
def | __del__ (self)
def | __deepcopy__ (self, memo={})
def | __str__ (self)
def | __repr__ (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (self)
def | sexpr (self)
def | as_ast (self)
def | get_id (self)
def | ctx_ref (self)
def | eq (self, other)
def | translate (self, target)
def | __copy__ (self)
def | hash (self)
Public Member Functions inherited from Z3PPObject
def | use_pp (self)

## Additional Inherited Members
Data Fields inherited from AstRef
| ast
| ctx

## Detailed Description

    Rational values.

Definition at line 2954 of file z3py.py.

## Member Function Documentation

## ◆ as_decimal()

def as_decimal | ( |  | self,
|  |  | prec
| ) |  |

     Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.

    >>> v = RealVal("1/5")
    >>> v.as_decimal(3)
    '0.2'
    >>> v = RealVal("1/3")
    >>> v.as_decimal(3)
    '0.333?'

Definition at line 3020 of file z3py.py.

3020 def as_decimal(self, prec):
3021 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
3022
3023 >>> v = RealVal("1/5")
3024 >>> v.as_decimal(3)
3025 '0.2'
3026 >>> v = RealVal("1/3")
3027 >>> v.as_decimal(3)
3028 '0.333?'
3029 """
3030 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
3031
z3py.RealVal
def RealVal(val, ctx=None)
Definition: z3py.py:3162
Z3_get_numeral_decimal_string
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.

## ◆ as_fraction()

def as_fraction | ( |  | self | ) |

    Return a Z3 rational as a Python Fraction object.

    >>> v = RealVal("1/5")
    >>> v.as_fraction()
    Fraction(1, 5)

Definition at line 3041 of file z3py.py.

3041 def as_fraction(self):
3042 """Return a Z3 rational as a Python Fraction object.
3043
3044 >>> v = RealVal("1/5")
3045 >>> v.as_fraction()
3046 Fraction(1, 5)
3047 """
3048 return Fraction(self.numerator_as_long(), self.denominator_as_long())
3049
3050

## ◆ as_long()

def as_long | ( |  | self | ) |

Definition at line 3016 of file z3py.py.

3016 def as_long(self):
3017 _z3_assert(self.is_int_value(), "Expected integer fraction")
3018 return self.numerator_as_long()
3019

Referenced by BitVecNumRef.as_signed_long(), RatNumRef.denominator_as_long(), and RatNumRef.numerator_as_long().

## ◆ as_string()

def as_string | ( |  | self | ) |

    Return a Z3 rational numeral as a Python string.

    >>> v = Q(3,6)
    >>> v.as_string()
    '1/2'

Definition at line 3032 of file z3py.py.

3032 def as_string(self):
3033 """Return a Z3 rational numeral as a Python string.
3034
3035 >>> v = Q(3,6)
3036 >>> v.as_string()
3037 '1/2'
3038 """
3039 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
3040
z3py.Q
def Q(a, b, ctx=None)
Definition: z3py.py:3197
Z3_get_numeral_string
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.

Referenced by IntNumRef.as_long(), BitVecNumRef.as_long(), and FiniteDomainNumRef.as_long().

## ◆ denominator()

def denominator | ( |  | self | ) |

     Return the denominator of a Z3 rational numeral.

    >>> is_rational_value(Q(3,5))
    True
    >>> n = Q(3,5)
    >>> n.denominator()
    5

Definition at line 2972 of file z3py.py.

2972 def denominator(self):
2973 """ Return the denominator of a Z3 rational numeral.
2974
2975 >>> is_rational_value(Q(3,5))
2976 True
2977 >>> n = Q(3,5)
2978 >>> n.denominator()
2979 5
2980 """
2981 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
2982
z3py.is_rational_value
def is_rational_value(a)
Definition: z3py.py:2718
Z3_get_denominator
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.

Referenced by RatNumRef.denominator_as_long(), and RatNumRef.is_int_value().

## ◆ denominator_as_long()

def denominator_as_long | ( |  | self | ) |

     Return the denominator as a Python long.

    >>> v = RealVal("1/3")
    >>> v
    1/3
    >>> v.denominator_as_long()
    3

Definition at line 2996 of file z3py.py.

2996 def denominator_as_long(self):
2997 """ Return the denominator as a Python long.
2998
2999 >>> v = RealVal("1/3")
3000 >>> v
3001 1/3
3002 >>> v.denominator_as_long()
3003 3
3004 """
3005 return self.denominator().as_long()
3006

Referenced by RatNumRef.as_fraction(), and RatNumRef.is_int_value().

## ◆ is_int()

def is_int | ( |  | self | ) |

    Return `True` if `self` is an integer expression.

    >>> x = Int('x')
    >>> x.is_int()
    True
    >>> (x + 1).is_int()
    True
    >>> y = Real('y')
    >>> (x + y).is_int()
    False

Reimplemented from ArithRef.

Definition at line 3007 of file z3py.py.

3007 def is_int(self):
3008 return False
3009
z3py.is_int
def is_int(a)
Definition: z3py.py:2648

Referenced by IntNumRef.as_long(), RatNumRef.is_int_value(), and ArithSortRef.subsort().

## ◆ is_int_value()

def is_int_value | ( |  | self | ) |

Definition at line 3013 of file z3py.py.

3013 def is_int_value(self):
3014 return self.denominator().is_int() and self.denominator_as_long() == 1
3015
z3py.is_int_value
def is_int_value(a)
Definition: z3py.py:2694

Referenced by RatNumRef.as_long().

## ◆ is_real()

def is_real | ( |  | self | ) |

    Return `True` if `self` is an real expression.

    >>> x = Real('x')
    >>> x.is_real()
    True
    >>> (x + 1).is_real()
    True

Reimplemented from ArithRef.

Definition at line 3010 of file z3py.py.

3010 def is_real(self):
3011 return True
3012
z3py.is_real
def is_real(a)
Definition: z3py.py:2667

## ◆ numerator()

def numerator | ( |  | self | ) |

     Return the numerator of a Z3 rational numeral.

    >>> is_rational_value(RealVal("3/5"))
    True
    >>> n = RealVal("3/5")
    >>> n.numerator()
    3
    >>> is_rational_value(Q(3,5))
    True
    >>> Q(3,5).numerator()
    3

Definition at line 2957 of file z3py.py.

2957 def numerator(self):
2958 """ Return the numerator of a Z3 rational numeral.
2959
2960 >>> is_rational_value(RealVal("3/5"))
2961 True
2962 >>> n = RealVal("3/5")
2963 >>> n.numerator()
2964 3
2965 >>> is_rational_value(Q(3,5))
2966 True
2967 >>> Q(3,5).numerator()
2968 3
2969 """
2970 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
2971
Z3_get_numerator
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.

Referenced by RatNumRef.numerator(), and RatNumRef.numerator_as_long().

## ◆ numerator_as_long()

def numerator_as_long | ( |  | self | ) |

     Return the numerator as a Python long.

    >>> v = RealVal(10000000000)
    >>> v
    10000000000
    >>> v + 1
    10000000000 + 1
    >>> v.numerator_as_long() + 1 == 10000000001
    True

Definition at line 2983 of file z3py.py.

2983 def numerator_as_long(self):
2984 """ Return the numerator as a Python long.
2985
2986 >>> v = RealVal(10000000000)
2987 >>> v
2988 10000000000
2989 >>> v + 1
2990 10000000000 + 1
2991 >>> v.numerator_as_long() + 1 == 10000000001
2992 True
2993 """
2994 return self.numerator().as_long()
2995

Referenced by RatNumRef.as_fraction(), and RatNumRef.as_long().