stp.ExprRef

class stp.ExprRef

A term. == builds EQUAL (SMT ‘=’) for every sort and != builds DISTINCT. Operands: another term of this manager, or a Python literal coercible to this term’s sort. x == None and objects that are neither terms nor numbers -> NotImplemented (Python answers False by identity); a number that cannot coerce to the sort -> TypeError naming the sort; a term of another manager -> SortMismatch.

kind()

num_args()

arg(i)

manager()

is_symbol()

decl_name()

eq(other)

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

__eq__(other)

Return self==value.

__ne__(other)

Return self!=value.

__bool__()

to_string(format='smtlib2')

substitute(*pairs)

translate(tm)

__iter__()

__contains__(item)

get_id()

sexpr()

SMT-LIB 2, untruncated.

ctx_ref()

child(i)

children()

fits_int64()

fits_uint64()

fp_bits()

fp_to_double()

fp_to_rational()

id

indices()

is_const()

is_defined_function()

is_value()

node_hash()

num_children()

real_denominator()

real_numerator()

real_to_double()

same(other)

sort()

sort_kind()

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

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

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

to_uint64()

to_uninterpreted_index()