Symbols and values

stp_term stp_declare(stp_tm, const char *name, stp_sort)

the manager’s name table: the same (name, sort) gives the same term; SORT_MISMATCH on a clash; INVALID_ARGUMENT for a name SMT-LIB predefines (true, select, bvadd, RNE, …)

stp_term stp_mk_fresh(stp_tm, stp_sort, const char *prefix)

anonymous, never in the name table; printed as prefix!k; NULL prefix means “”

stp_term stp_tm_symbol(stp_tm, const char *name)

NULL, no error, if absent; define-fun: the body if nullary, otherwise a callable function term

stp_status stp_tm_bind_symbol(stp_tm, const char *name, stp_term)

enter an existing symbol into the table under this name; SORT_MISMATCH if taken, INVALID_ARGUMENT for a compound term or a predefined name

size_t stp_tm_num_symbols(stp_tm)

declared symbols and parameterized definitions, distinct identities

stp_term stp_tm_symbol_at(stp_tm, size_t i)

size_t stp_tm_num_declared_sorts(stp_tm)

stp_sort stp_tm_declared_sort_at(stp_tm, size_t i)

stp_term stp_tm_term_from_id(stp_tm, uint64_t id)

INVALID_ARGUMENT if no live term has that id

stp_term stp_mk_true(stp_tm)

stp_term stp_mk_false(stp_tm)

stp_term stp_mk_bool(stp_tm, bool)

stp_term stp_mk_bv_uint64(stp_tm, uint32_t width, uint64_t value)

VALUE_OUT_OF_RANGE unless it fits

stp_term stp_mk_bv_int64(stp_tm, uint32_t width, int64_t value)

two’s complement range of width

stp_term stp_mk_bv_str(stp_tm, uint32_t width, const char *digits, int base)

base 2, 10, 16; #b/#x/0x; ‘-’ in base 10; ‘_’ between two digits

stp_term stp_mk_bv_limbs(stp_tm, uint32_t width, size_t n, const uint64_t *lsb_first)

stp_term stp_mk_bv_bytes(stp_tm, uint32_t width, size_t n, const uint8_t *bytes, bool little_endian)

stp_term stp_mk_bv_wrapped(stp_tm, uint32_t width, uint64_t value)

value mod 2^width, by name

stp_term stp_mk_bv_zero(stp_tm, uint32_t width)

stp_term stp_mk_bv_ones(stp_tm, uint32_t width)

stp_term stp_mk_bv_min_signed(stp_tm, uint32_t width)

stp_term stp_mk_bv_max_signed(stp_tm, uint32_t width)

stp_term stp_mk_fp_from_bits(stp_tm, stp_sort fp, stp_term bv_value)

NaN canonicalised

stp_term stp_mk_fp_from_bits_str(stp_tm, stp_sort fp, const char *bits)

“0b..”, “0x..” or bare binary

stp_term stp_mk_fp(stp_tm, stp_term sign, stp_term exponent, stp_term significand)

(fp …); symbolic allowed

stp_term stp_mk_fp_pos_zero(stp_tm, stp_sort fp)

stp_term stp_mk_fp_neg_zero(stp_tm, stp_sort fp)

stp_term stp_mk_fp_pos_inf(stp_tm, stp_sort fp)

stp_term stp_mk_fp_neg_inf(stp_tm, stp_sort fp)

stp_term stp_mk_fp_nan(stp_tm, stp_sort fp)

the canonical quiet NaN of the format

stp_term stp_mk_fp_double(stp_tm, stp_sort fp, stp_rm rm, double value)

exact, then rounded once under rm

stp_term stp_mk_fp_decimal(stp_tm, stp_sort fp, stp_rm rm, const char *literal)

“0.1”, “1/3”, “-2.5e-3”

stp_term stp_mk_rm(stp_tm, stp_rm)

stp_term stp_mk_real_int64(stp_tm, int64_t)

stp_term stp_mk_real_fraction(stp_tm, int64_t numerator, int64_t denominator)

INVALID_ARGUMENT if 0

stp_term stp_mk_real_str(stp_tm, const char *literal)

“-3/7”, “0.25”, “12”

stp_term stp_mk_const_array(stp_tm, stp_sort array_sort, stp_term element)

every cell equals element, which may be symbolic

stp_term stp_array_from_bytes(stp_tm, size_t n, const uint8_t *bytes, uint32_t index_width)

sugar: store chain over (as const … 0)