RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3py_1_1_rat_num_ref.html below:

Z3: RatNumRef Class Reference

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) def sort (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) def as_ast (self) def get_id (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) def __init__ (self, ast, ctx=None) def __del__ (self) def __deepcopy__ (self, memo={}) def __str__ (self) def __repr__ (self) def __nonzero__ (self) def __bool__ (self) def sexpr (self) def ctx_ref (self) def eq (self, other) def translate (self, target) def __copy__ (self) def hash (self) def use_pp (self)

Rational values.

Definition at line 3042 of file z3py.py.

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

3108 def

as_decimal(self, prec):

3109 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places. 3111 >>> v = RealVal("1/5") 3114 >>> v = RealVal("1/3")

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()

Return a Z3 rational as a Python Fraction object.

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

Definition at line 3129 of file z3py.py.

3129 def

as_fraction(self):

3130 """Return a Z3 rational as a Python Fraction object. 3132 >>> v = RealVal("1/5") 3136 return

Fraction(self.numerator_as_long(), self.denominator_as_long())

◆ as_long() ◆ as_string()

Return a Z3 rational numeral as a Python string.

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

Definition at line 3120 of file z3py.py.

3120 def

as_string(self):

3121 """Return a Z3 rational numeral as a Python 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()

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

3060 def

denominator(self):

3061 """ Return the denominator of a Z3 rational numeral. 3063 >>> is_rational_value(Q(3,5))

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

3084 def

denominator_as_long(self):

3085 """ Return the denominator as a Python long. 3087 >>> v = RealVal("1/3") 3090 >>> v.denominator_as_long() 3093 return

self.denominator().as_long()

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

◆ is_int() ◆ is_int_value() def is_int_value ( self ) ◆ is_real()

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

◆ numerator()

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

3045 def

numerator(self):

3046 """ Return the numerator of a Z3 rational numeral. 3048 >>> is_rational_value(RealVal("3/5")) 3050 >>> n = RealVal("3/5") 3053 >>> is_rational_value(Q(3,5)) 3055 >>> Q(3,5).numerator() 3058 return

IntNumRef(

Z3_get_numerator

(self.ctx_ref(), self.as_ast()), self.ctx)

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

3071 def

numerator_as_long(self):

3072 """ Return the numerator as a Python long. 3074 >>> v = RealVal(10000000000) 3079 >>> v.numerator_as_long() + 1 == 10000000001 3082 return

self.numerator().as_long()

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

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4