C API¶
Include <stp/stp.h> and link against libstp. See The 3.x API (C++, C and Python) for examples and error handling.
the STP 3.x C API.
A flat C99 view of <stp/stp.hpp>: every C++ method has a C function here, plus the hand-written runtime (reference counting, scopes, the error record, the failed state of a solver). The enumerations that the data tables define (kinds, error codes, the stable option tier) are included from the generated headers so that the three languages can never disagree on a value.
Conventions
Every identifier is prefixed stp_ / STP_. Nothing is exported unprefixed.
Handles are typed opaque pointers. A term handle IS the interned engine node: two handles compare equal with == exactly when they are the same term. stp_term_id() is unique within a manager and never reused; stp_term_hash() mixes it with the manager id, so handles from different managers share a hash only by coincidence.
Every term handle a function returns carries one reference owned by the caller (release optional for safety, required for memory). Scopes (stp_tm_scope_push/pop) release everything exported inside them; the exact rules are at “reclamation”.
Every fallible function either returns a handle (NULL on error) or returns stp_status (STP_OK / STP_ERROR) with results in out-parameters, except the counts and yes/no queries (stp_tm_num_symbols, stp_model_in_core, stp_options_is_set, …), whose 0 or false on an error is also an answer: they record the error, which says which it was. Details are in the manager’s error record (stp_tm_error): the FIRST error since stp_tm_clear_error is kept, for diagnosis; it blocks nothing. An installed callback (stp_tm_set_error_callback) sees EVERY error.
NULL propagation: a NULL term or sort argument makes a constructor or reader return NULL / STP_ERROR / false without recording anything, so a chain of constructions can be checked once, where it is asserted. A NULL manager, solver, options, model, value or statistics handle, a NULL string and a NULL out-pointer are STP_ERR_NULL_HANDLE, recorded in the object’s record (in the thread-local record when the missing handle is the object itself).
The failed state of a solver (the failbit of iostreams): a mutating call on a solver that fails (assert, push, pop, parse*, reset*, an option write, or an assert of a NULL term) puts THAT solver into a failed state, in which check_sat*, entails, write_cnf, model, candidate_model and value refuse with STP_ERR_STATE naming the original failure, until stp_solver_clear_error(s). A failed construction can therefore never silently drop an assertion, and a typo never affects the manager, other solvers, readers or printers. stp_solver_failed(s) reports the state.
Optional results: stp_solver_candidate_model, stp_solver_symbol, stp_tm_symbol, stp_term_symbol and stp_model_try_value return NULL with NO error record when there is nothing to return; they are the only NULL-returning functions for which NULL is not an error (and the NULL-propagation rule above).
Strings and buffers returned as char* are caller-owned and freed with stp_free(). Nothing is “valid until the next call” except where a function says “static” (a string that lives as long as the process) or names the handle that owns it. Collections are read through indexed accessors.
Nothing in this library calls exit() or abort(). RESOURCE and INTERNAL errors poison the object (every later call fails with STP_ERR_STATE); stp_set_internal_error_policy(STP_ABORT) or STP_ABORT_ON_INTERNAL_ERROR=1 in the environment restores an abort, for debugging.
Thread contract: a manager and the solvers/models over it are used by one thread at a time, whichever thread that is; independent managers are concurrent, except that parses take one process-wide lock for their whole length (an EXECUTE input’s checks and a text source’s waits included); stp_solver_interrupt is the one call safe from any thread and from a signal handler.
Callbacks (the sinks, the terminator, the fatal-error handler, a text source, the error callback) must not call the library: every call from one fails with STP_ERR_STATE but stp_solver_interrupt, stp_solver_clear_interrupt and stp_solver_interrupt_pending.
Public struct layouts, versioned by STP_API_VERSION: stp_result, stp_entailment, stp_budget, stp_error, stp_float_value, stp_version. Every other type is opaque.
