Z3
 
Loading...
Searching...
No Matches
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)
 
def from_string (self, s)
 
def serialize (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
 
- Protected Member Functions inherited from Z3PPObject
def _repr_html_ (self)
 

Detailed Description

Rational values.

Definition at line 2992 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 3058 of file z3py.py.

3058 def as_decimal(self, prec):
3059 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
3060
3061 >>> v = RealVal("1/5")
3062 >>> v.as_decimal(3)
3063 '0.2'
3064 >>> v = RealVal("1/3")
3065 >>> v.as_decimal(3)
3066 '0.333?'
3067 """
3068 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
3069
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 3079 of file z3py.py.

3079 def as_fraction(self):
3080 """Return a Z3 rational as a Python Fraction object.
3081
3082 >>> v = RealVal("1/5")
3083 >>> v.as_fraction()
3084 Fraction(1, 5)
3085 """
3086 return Fraction(self.numerator_as_long(), self.denominator_as_long())
3087
3088

◆ as_long()

def as_long (   self)

Definition at line 3054 of file z3py.py.

3054 def as_long(self):
3055 _z3_assert(self.is_int_value(), "Expected integer fraction")
3056 return self.numerator_as_long()
3057

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

3070 def as_string(self):
3071 """Return a Z3 rational numeral as a Python string.
3072
3073 >>> v = Q(3,6)
3074 >>> v.as_string()
3075 '1/2'
3076 """
3077 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
3078
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 3010 of file z3py.py.

3010 def denominator(self):
3011 """ Return the denominator of a Z3 rational numeral.
3012
3013 >>> is_rational_value(Q(3,5))
3014 True
3015 >>> n = Q(3,5)
3016 >>> n.denominator()
3017 5
3018 """
3019 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
3020
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 3034 of file z3py.py.

3034 def denominator_as_long(self):
3035 """ Return the denominator as a Python long.
3036
3037 >>> v = RealVal("1/3")
3038 >>> v
3039 1/3
3040 >>> v.denominator_as_long()
3041 3
3042 """
3043 return self.denominator().as_long()
3044

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

3045 def is_int(self):
3046 return False
3047

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

◆ is_int_value()

def is_int_value (   self)

Definition at line 3051 of file z3py.py.

3051 def is_int_value(self):
3052 return self.denominator().is_int() and self.denominator_as_long() == 1
3053

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

3048 def is_real(self):
3049 return True
3050

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

2995 def numerator(self):
2996 """ Return the numerator of a Z3 rational numeral.
2997
2998 >>> is_rational_value(RealVal("3/5"))
2999 True
3000 >>> n = RealVal("3/5")
3001 >>> n.numerator()
3002 3
3003 >>> is_rational_value(Q(3,5))
3004 True
3005 >>> Q(3,5).numerator()
3006 3
3007 """
3008 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
3009
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 3021 of file z3py.py.

3021 def numerator_as_long(self):
3022 """ Return the numerator as a Python long.
3023
3024 >>> v = RealVal(10000000000)
3025 >>> v
3026 10000000000
3027 >>> v + 1
3028 10000000000 + 1
3029 >>> v.numerator_as_long() + 1 == 10000000001
3030 True
3031 """
3032 return self.numerator().as_long()
3033

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