Terms

stp_term stp_term_copy(stp_term)

always unscoped: “copy” means “keep” (rule 2)

stp_status stp_term_release(stp_term)

STATE for a scoped handle (rule 3)

uint64_t stp_term_id(stp_term)

infallible; 0 for NULL

uint64_t stp_term_hash(stp_term)

infallible; 0 for NULL

stp_tm stp_term_manager(stp_term)

+1 handle

stp_status stp_term_get_kind(stp_term, stp_kind *out)

the public view; guaranteed under simplify = false only

stp_sort stp_term_sort(stp_term)

stp_status stp_term_num_children(stp_term, size_t *out)

stp_term stp_term_child(stp_term, size_t i)

INDEX_OUT_OF_RANGE

stp_status stp_term_num_indices(stp_term, size_t *out)

stp_status stp_term_index(stp_term, size_t i, uint32_t *out)

bool stp_term_is_value(stp_term)

infallible; false for NULL

bool stp_term_is_defined_function(stp_term)

a parameterized define-fun; false for NULL

bool stp_term_is_const(stp_term)

a declared symbol; infallible; false for NULL

char *stp_term_symbol(stp_term)

NULL, no error, if anonymous or not a symbol

char *stp_term_str(stp_term)

SMT-LIB 2, untruncated; works while an error is pending

char *stp_term_to_string(stp_term, stp_format, bool share_subterms)

stp_term stp_term_substitute(stp_term, size_t n, const stp_term *from, const stp_term *to)

stp_term stp_tm_simplify(stp_tm, stp_term)

local rewrites only; touches no solver; an unspecified floating-point case (fp.min of +0 and -0, fp.to_ubv of NaN, …) stays as it is

bool stp_term_same(stp_term, stp_term)

structural: the same node (== on the handles)

stp_status stp_term_to_bool(stp_term, bool *out)

readers: NOT_A_VALUE unless the term is a value; SORT_MISMATCH on the wrong sort; DOES_NOT_FIT where stated

bool stp_term_fits_uint64(stp_term)

false (no record) unless a BV value that fits

bool stp_term_fits_int64(stp_term)

stp_status stp_term_to_uint64(stp_term, uint64_t *out)

stp_status stp_term_to_int64(stp_term, int64_t *out)

two’s complement of the width

char *stp_term_to_bv_string(stp_term, int base, bool pad)

base 2, 10 or 16

stp_status stp_term_bv_num_limbs(stp_term, size_t *out)

ceil(width/64)

stp_status stp_term_to_bv_limbs(stp_term, size_t n, uint64_t *out_lsb_first)

caller buffer of n >= num_limbs

stp_status stp_term_to_bv_bytes(stp_term, size_t n, uint8_t *out, bool little_endian)

n >= ceil(width/8)

stp_status stp_term_to_fp(stp_term, stp_float_value *out)

stp_status stp_term_fp_significand_limbs(stp_term, size_t n, uint64_t *out_lsb_first)

the sig_size-1 trailing bits

char *stp_term_fp_bits(stp_term)

IEEE interchange bits, MSB first

stp_status stp_term_fp_to_double(stp_term, double *out)

DOES_NOT_FIT for formats wider than binary64

stp_status stp_term_fp_to_rational(stp_term, char **numerator, char **denominator)

finite values only (INVALID_ARGUMENT otherwise); two caller-owned strings

stp_status stp_term_to_rm(stp_term, stp_rm *out)

char *stp_term_real_numerator(stp_term)

decimal; may carry a leading ‘-’

char *stp_term_real_denominator(stp_term)

decimal; > 0; lowest terms

bool stp_term_real_fits_int64(stp_term)

stp_status stp_term_real_to_int64(stp_term, int64_t *num, int64_t *den)

DOES_NOT_FIT

stp_status stp_term_real_to_double(stp_term, double *out)

nearest double

stp_status stp_term_to_uninterpreted_index(stp_term, uint64_t *out)