stp.TermManager

class stp.TermManager(simplify=None, default_rounding_mode=None, options=None, uf_sort_width=None)

A term manager: the node factory, the sort pool and the one name table.

TermManager(simplify=True, default_rounding_mode=RoundingMode.RNE, options=None, uf_sort_width=16). options supplies the manager-scoped entries (simplify, default-rounding-mode, uf-sort-width) by name, in any form Solver takes (an Options object, a solver’s live options, a dict); the keyword arguments override it.

property default_rounding_mode

The mode FP operators use when none is given (read/write).

mk_term(kind, args, indices=(), sort=None)

The generic constructor: kind, the argument terms, the integer indices in SMT-LIB order and, for CONST_ARRAY, the result sort.

mk_fresh(sort, prefix='')

array_from_bytes(data, index_width=32)

array_sort(index, element)

bind_symbol(name, t)

bool_sort()

busy

True while a check or a parse runs on this manager (the GIL is released then).

bv_sort(width)

clear_error()

declare(name, sort)

declare_sort(name)

declared_sorts()

fp_sort(ebits, sbits)

fun_sort(domain, codomain)

id

mk_bool(v)

mk_bv(width, value)

A bit-vector value of width bits: strict (the two’s complement range of the width, checked by the C layer); any Python int.

mk_bv_bytes(width, data, little_endian=True)

mk_bv_str(width, digits, base=10)

mk_const_array(array_sort, element)

mk_fp_decimal(fp, rm, literal)

mk_fp_double(fp, rm, value)

mk_fp_from_bits(fp, bv)

mk_fp_from_bits_str(fp, bits)

mk_fp_special(fp, which)

which: ‘nan’, ‘+zero’, ‘-zero’, ‘+inf’, ‘-inf’.

mk_fresh_sort(prefix='')

mk_real_str(literal)

mk_rm(rm)

owner_thread

The ident of the thread that created the manager (informational: a manager may be used from any thread, one call at a time).

pending_error()

The manager’s recorded error as an exception object, or None (never raised, never cleared).

real_sort()

rewrap(t, cls)

A NEW wrapper of t’s node of class cls (a Term subclass), holding its own reference and not entered in the identity map: for value views that decorate a term (an array value is the store chain it denotes plus its entries).

rm_sort()

simplify

simplify_term(t)

substitute(t, from_, to)

symbol(name)

symbols()

term_from_id(id)

uf_sort_width