Sorts¶

stp_sort stp_mk_bool_sort(stp_tm)¶: Names supplied to stp_tm_declare_sort, stp_declare and stp_tm_bind_symbol, and prefixes supplied to stp_mk_fresh_sort and stp_mk_fresh, must be representable as SMT-LIB quoted symbols: no ‘|’, backslash, DEL, or ASCII control characters other than tab, newline and carriage return. Spaces and non-ASCII bytes (including UTF-8) are allowed; printing quotes where needed. Leading ‘@’ and ‘.’ are reserved for solver use. Violations are INVALID_ARGUMENT before any name is recorded. Names must be nonempty; fresh-name prefixes may be empty. As with all C strings, the first NUL terminates the name or prefix.

stp_sort stp_mk_bv_sort(stp_tm, uint32_t width)¶: INVALID_ARGUMENT if width == 0

stp_sort stp_mk_fp_sort(stp_tm, uint32_t exp_size, uint32_t sig_size)¶: each >= 2

stp_sort stp_mk_array_sort(stp_tm, stp_sort index, stp_sort element)¶: UNSUPPORTED for combinations the engine lacks

stp_sort stp_mk_fun_sort(stp_tm, size_t arity, const stp_sort *domain, stp_sort codomain)¶

stp_sort stp_tm_declare_sort(stp_tm, const char *name)¶: a named uninterpreted sort, keyed by name; INVALID_ARGUMENT for a sort SMT-LIB predefines (Bool, Real, …)

stp_sort stp_mk_fresh_sort(stp_tm, const char *prefix)¶: anonymous; printed as prefix!k; NULL prefix means “”

stp_status stp_sort_bv_size(stp_sort, uint32_t *out)¶: INVALID_ARGUMENT unless a BV sort

stp_status stp_sort_fp_exp_size(stp_sort, uint32_t *out)¶: INVALID_ARGUMENT unless an FP sort

stp_status stp_sort_fp_sig_size(stp_sort, uint32_t *out)¶: includes the hidden bit