stp.ArrayNumRef

class stp.ArrayNumRef

An array value: a term (a Store chain over K) that is also a read-only mapping view. v[i] for a value index is an explicit lookup (never via folding): the element if present, else the default; for a symbolic index it is Select(v, i). i in v means “has an explicit entry”.

property default

items()

keys()

values()

__len__()

__getitem__(i)

__contains__(i)

__iter__()

as_bytes(first_index, count)

A dense read of count elements from first_index, little-endian bytes per element; the element width must be a multiple of 8.

as_term()

as_list()

__bool__()

__eq__(other)

Return self==value.

__ne__(other)

Return self!=value.

arg(i)

child(i)

children()

ctx_ref()

decl_name()

domain()

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

range()

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)