Model

stp_model stp_model_copy(stp_model)

void stp_model_release(stp_model)

stp_tm stp_model_manager(stp_model)

+1 handle

stp_term stp_model_value(stp_model, stp_term)

a VALUE of the term’s sort; symbols outside the core are completed. An array’s value is the constant array of its default under a store per cell (stp_array_value_as_term); a function has none (SORT_MISMATCH: read it with stp_model_fun_value)

stp_term stp_model_try_value(stp_model, stp_term)

NULL, no error, if completion would be needed; an array whose base is in the core, default included, needs none

stp_status stp_model_values(stp_model, size_t n, const stp_term *in, stp_term *out)

batch, all or nothing; on STP_OK every out[i] is +1

stp_status stp_model_bool(stp_model, stp_term, bool *out)

stp_status stp_model_uint64(stp_model, stp_term, uint64_t *out)

DOES_NOT_FIT

stp_status stp_model_int64(stp_model, stp_term, int64_t *out)

char *stp_model_bv_string(stp_model, stp_term, int base, bool pad)

stp_status stp_model_bv_num_limbs(stp_model, stp_term, size_t *out)

stp_status stp_model_bv_limbs(stp_model, stp_term, size_t n, uint64_t *out_lsb_first)

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

stp_status stp_model_fp(stp_model, stp_term, stp_float_value *out)

stp_status stp_model_fp_significand_limbs(stp_model, stp_term, size_t n, uint64_t *out_lsb_first)

stp_status stp_model_fp_to_double(stp_model, stp_term, double *out)

stp_status stp_model_rm(stp_model, stp_term, stp_rm *out)

char *stp_model_real_numerator(stp_model, stp_term)

char *stp_model_real_denominator(stp_model, stp_term)

stp_status stp_model_uninterpreted_index(stp_model, stp_term, uint64_t *out)

stp_array_value stp_model_array_value(stp_model, stp_term array)

any array-sorted term

stp_fun_value stp_model_fun_value(stp_model, stp_term fun)

any function symbol

stp_status stp_model_array_bytes(stp_model, stp_term array, uint64_t first_index, size_t count, uint8_t *out)

dense read of a BV-indexed BV-element array whose element width is a multiple of 8 (INVALID_ARGUMENT otherwise): count elements from first_index, little-endian bytes per element, completed by the model’s array fill rule; INVALID_ARGUMENT when the elements leave the index sort

size_t stp_model_num_symbols(stp_model)

the model core: symbols the solver assigned

stp_term stp_model_symbol(stp_model, size_t i)

bool stp_model_in_core(stp_model, stp_term symbol)

false: value() would complete it

char *stp_model_to_smt2(stp_model)

the whole model

void stp_array_value_release(stp_array_value)

stp_sort stp_array_value_sort(stp_array_value)

stp_term stp_array_value_default(stp_array_value)

a VALUE of the element sort

size_t stp_array_value_size(stp_array_value)

explicit entries

stp_status stp_array_value_entry(stp_array_value, size_t i, stp_term *index, stp_term *element)

+1 each; ascending by unsigned index value; a cell the model records, every other one holds the default

stp_term stp_array_value_at(stp_array_value, stp_term index_value)

the element, default if absent

stp_term stp_array_value_as_term(stp_array_value)

store chain over (as const …); re-assertable

void stp_fun_value_release(stp_fun_value)

stp_sort stp_fun_value_sort(stp_fun_value)

uint32_t stp_fun_value_arity(stp_fun_value)

bool stp_fun_value_is_tabular(stp_fun_value)

A define-fun has a symbolic body instead of a table: size, entry and else report UNSUPPORTED. apply evaluates it in the saved model; as_ite returns its body over the supplied formals, with free symbols fixed to the model (UNSUPPORTED for parameter-dependent partial floating-point operations).

stp_term stp_fun_value_else(stp_fun_value)

always ground: a VALUE of the codomain

size_t stp_fun_value_size(stp_fun_value)

stp_status stp_fun_value_entry(stp_fun_value, size_t i, size_t n, stp_term *args_out, stp_term *value)

an application the model records; INVALID_ARGUMENT if n is below the arity

stp_term stp_fun_value_apply(stp_fun_value, size_t n, const stp_term *arg_values)

stp_term stp_fun_value_as_ite(stp_fun_value, size_t n, const stp_term *formals)