Z3
 
Loading...
Searching...
No Matches
RatNumRef Class Reference
+ Inheritance diagram for RatNumRef:

Public Member Functions

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

Additional Inherited Members

- Data Fields inherited from AstRef
 ast = ast
 
 ctx = _get_ctx(ctx)
 
- Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)
 

Detailed Description

Rational values.

Definition at line 3067 of file z3py.py.

Member Function Documentation

◆ as_decimal()

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 3133 of file z3py.py.

3133 def as_decimal(self, prec):
3134 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
3135
3136 >>> v = RealVal("1/5")
3137 >>> v.as_decimal(3)
3138 '0.2'
3139 >>> v = RealVal("1/3")
3140 >>> v.as_decimal(3)
3141 '0.333?'
3142 """
3143 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
3144
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()

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 3154 of file z3py.py.

3154 def as_fraction(self):
3155 """Return a Z3 rational as a Python Fraction object.
3156
3157 >>> v = RealVal("1/5")
3158 >>> v.as_fraction()
3159 Fraction(1, 5)
3160 """
3161 return Fraction(self.numerator_as_long(), self.denominator_as_long())
3162

◆ as_long()

as_long ( self)

Definition at line 3129 of file z3py.py.

3129 def as_long(self):
3130 _z3_assert(self.is_int_value(), "Expected integer fraction")
3131 return self.numerator_as_long()
3132

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

◆ as_string()

as_string ( self)
Return a Z3 rational numeral as a Python string.

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

Definition at line 3145 of file z3py.py.

3145 def as_string(self):
3146 """Return a Z3 rational numeral as a Python string.
3147
3148 >>> v = Q(3,6)
3149 >>> v.as_string()
3150 '1/2'
3151 """
3152 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
3153
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 BitVecNumRef.as_long().

◆ denominator()

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 3085 of file z3py.py.

3085 def denominator(self):
3086 """ Return the denominator of a Z3 rational numeral.
3087
3088 >>> is_rational_value(Q(3,5))
3089 True
3090 >>> n = Q(3,5)
3091 >>> n.denominator()
3092 5
3093 """
3094 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
3095
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 denominator_as_long(), and is_int_value().

◆ denominator_as_long()

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 3109 of file z3py.py.

3109 def denominator_as_long(self):
3110 """ Return the denominator as a Python long.
3111
3112 >>> v = RealVal("1/3")
3113 >>> v
3114 1/3
3115 >>> v.denominator_as_long()
3116 3
3117 """
3118 return self.denominator().as_long()
3119

Referenced by as_fraction(), and is_int_value().

◆ is_int()

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 3120 of file z3py.py.

3120 def is_int(self):
3121 return False
3122

Referenced by is_int_value().

◆ is_int_value()

is_int_value ( self)

Definition at line 3126 of file z3py.py.

3126 def is_int_value(self):
3127 return self.denominator().is_int() and self.denominator_as_long() == 1
3128

Referenced by as_long().

◆ is_real()

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 3123 of file z3py.py.

3123 def is_real(self):
3124 return True
3125

◆ numerator()

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 3070 of file z3py.py.

3070 def numerator(self):
3071 """ Return the numerator of a Z3 rational numeral.
3072
3073 >>> is_rational_value(RealVal("3/5"))
3074 True
3075 >>> n = RealVal("3/5")
3076 >>> n.numerator()
3077 3
3078 >>> is_rational_value(Q(3,5))
3079 True
3080 >>> Q(3,5).numerator()
3081 3
3082 """
3083 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
3084
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 numerator_as_long().

◆ numerator_as_long()

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 3096 of file z3py.py.

3096 def numerator_as_long(self):
3097 """ Return the numerator as a Python long.
3098
3099 >>> v = RealVal(10000000000)
3100 >>> v
3101 10000000000
3102 >>> v + 1
3103 10000000000 + 1
3104 >>> v.numerator_as_long() + 1 == 10000000001
3105 True
3106 """
3107 return self.numerator().as_long()
3108

Referenced by as_fraction(), and as_long().

◆ py_value()

py_value ( self)
Return a Python value that is equivalent to `self`.

Reimplemented from AstRef.

Definition at line 3163 of file z3py.py.

3163 def py_value(self):
3164 return Z3_get_numeral_double(self.ctx_ref(), self.as_ast())
3165
3166
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.