stp.RatNumRef

class stp.RatNumRef

A Real value (always a rational).

as_fraction()

numerator()

denominator()

numerator_as_long()

denominator_as_long()

as_decimal(prec)

A decimal string with prec digits after the point, truncated toward zero (z3py appends ‘?’ when the expansion continues).

as_string()

__float__()

is_int()

__add__(other)

__bool__()

__contains__(item)

__eq__(other)

Return self==value.

__ge__(other)

Return self>=value.

__gt__(other)

Return self>value.

__iter__()

__le__(other)

Return self<=value.

__lt__(other)

Return self<value.

__mul__(other)

__ne__(other)

Return self!=value.

__neg__()

__radd__(other)

__rmul__(other)

__rsub__(other)

__rtruediv__(other)

__sub__(other)

__truediv__(other)

arg(i)

child(i)

children()

ctx_ref()

decl_name()

eq(other)

Structural equality: the same term (the explicit test; == builds a term).

fits_int64()

fits_uint64()

fp_bits()

fp_to_double()

fp_to_rational()

get_id()

id

indices()

is_const()

is_defined_function()

is_symbol()

is_value()

kind()

manager()

node_hash()

num_args()

num_children()

real_denominator()

real_numerator()

real_to_double()

same(other)

sexpr()

SMT-LIB 2, untruncated.

sort()

sort_kind()

The sort kind in one call (the class chooser’s view).

substitute(*pairs)

symbol()

to_bool()

to_bv_bytes(little_endian=True)

to_bv_string(base=2, pad=True)

to_fp()

(exp_size, sig_size, sign, biased_exponent, class, significand) of an FP value.

to_int()

The two’s complement value of a BV value as a Python int, any width.

to_int64()

to_rm()

to_string(format='smtlib2')

to_uint()

The unsigned value of a BV value as a Python int, any width.

to_uint64()

to_uninterpreted_index()

translate(tm)