Term manager

typedef void (*stp_error_callback)(const stp_error*, void *user)

sees every error; may return; the call still fails; must not call the library; the pointer is valid during the call only

stp_tm stp_tm_new(stp_options manager_options)

NULL: defaults; a SET solver-scoped entry is OPTION_VALUE

stp_tm stp_tm_new_with(bool simplify, stp_rm default_rounding_mode, uint32_t uf_sort_width)

the three manager entries as arguments

stp_tm stp_tm_copy(stp_tm)

another handle to the same manager

void stp_tm_release(stp_tm)

the manager dies when nothing refers to it

uint64_t stp_tm_id(stp_tm)

process-unique; 0 for NULL

bool stp_tm_simplify_enabled(stp_tm)

construction-time folding on?

stp_rm stp_tm_default_rounding_mode(stp_tm)
stp_status stp_tm_set_default_rounding_mode(stp_tm, stp_rm)
uint32_t stp_tm_uf_sort_width(stp_tm)
void stp_tm_scope_push(stp_tm)

reclamation (the C runtime). Each node carries two external counts: unscoped references (owned by the caller) and scoped references (owned by the innermost open scope, which keeps a journal of them). Four rules:

  1. A handle a function RETURNS while a scope is open is scoped; with no scope open it is unscoped.

  2. stp_term_copy(t) always yields an UNSCOPED reference: “copy” means “keep”. That is how a handle produced inside a scope survives the scope.

  3. stp_term_release(t) gives back one unscoped reference; if t has none it is STP_ERR_STATE (“scoped handle: copy it to keep it, or let the scope pop”) and nothing happens.

  4. stp_tm_scope_pop releases every reference in the popped journal; stp_tm_release_all releases every external reference of the manager, scoped and unscoped, and empties every journal (the scopes stay open). C++ Terms in the same process hold engine references of their own and are unaffected. Every unscoped reference and every open scope keeps the manager alive; a sort handle does not (sorts are owned by the manager and valid while it lives). The scope functions are infallible (a NULL argument does nothing; a pop with no scope open does nothing).

void stp_tm_scope_pop(stp_tm)
size_t stp_tm_scope_depth(stp_tm)

open scopes

void stp_tm_release_all(stp_tm)

term references only; solver, model, options and statistics handles have their own release

const stp_error *stp_tm_error(stp_tm)

NULL when no error is pending; infallible

size_t stp_tm_error_num_terms(stp_tm)

the terms involved in the recorded error (e.g. both operands)

stp_term stp_tm_error_term(stp_tm, size_t i)

+1; a FOREIGN_MANAGER error lists no term (it would be another manager’s)

size_t stp_tm_error_num_sorts(stp_tm)

the sorts involved in the recorded error

stp_sort stp_tm_error_sort(stp_tm, size_t i)
void stp_tm_clear_error(stp_tm)
void stp_tm_set_error_callback(stp_tm, stp_error_callback, void *user)