stp.UninterpretedNumRef

class stp.UninterpretedNumRef

property index

__bool__()

__contains__(item)

__eq__(other)

Return self==value.

__iter__()

__ne__(other)

Return self!=value.

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)