Solver

typedef bool (*stp_terminate_callback)(void *user)

true: stop. Runs inside the check: it must not call the library except stp_solver_interrupt

typedef void (*stp_text_sink)(const char *text, size_t len, void *user)

typedef size_t (*stp_text_source)(char *buf, size_t max, void *user)

the input read as far as the parser needs it: the source fills up to max bytes and returns how many, 0 at the end and (size_t)-1 if reading failed (the parse then fails with IO); AUTO reads SMT-LIB 2. The source must not call the library (STATE), and runs under the process-wide parser lock

typedef void (*stp_fatal_error_handler)(const char *message, void *user)

typedef void (*stp_cnf_sink)(const char *dimacs, size_t len, stp_cnf_scope scope, void *user)

stp_solver stp_solver_new(stp_tm, stp_options)

any number of solvers per manager, each with its own stack, options and models

void stp_solver_delete(stp_solver)

terms, sorts and models stay valid

const stp_error *stp_solver_failed(stp_solver)

the failure that put the solver in its failed state; NULL if none; infallible

size_t stp_solver_failed_num_terms(stp_solver)

the terms and sorts of that failure, as stp_tm_error_term/_sort

stp_term stp_solver_failed_term(stp_solver, size_t i)

+1

size_t stp_solver_failed_num_sorts(stp_solver)

stp_sort stp_solver_failed_sort(stp_solver, size_t i)

void stp_solver_clear_error(stp_solver)

leave the failed state

stp_tm stp_solver_manager(stp_solver)

+1 handle

stp_status stp_solver_set_str(stp_solver, const char *name, const char *value)

the LIVE options: same names as the stp_options_* setters and getters, on the solver, reporting through the manager’s record; a write outside the entry’s Settable window is OPTION_TIMING. No stp_options handle to the live view exists (nothing to delete by mistake); stp_solver_options_copy gives a detached value.

stp_status stp_solver_set_bool(stp_solver, const char *name, bool)

stp_status stp_solver_set_int64(stp_solver, const char *name, int64_t)

stp_status stp_solver_set_uint64(stp_solver, const char *name, uint64_t)

stp_status stp_solver_set_duration_ms(stp_solver, const char *name, uint64_t ms)

stp_status stp_solver_set_names(stp_solver, const char *name, size_t n, const char *const *members)

stp_status stp_solver_set_bool_e(stp_solver, stp_option, bool)

stp_status stp_solver_set_int64_e(stp_solver, stp_option, int64_t)

stp_status stp_solver_set_uint64_e(stp_solver, stp_option, uint64_t)

stp_status stp_solver_set_str_e(stp_solver, stp_option, const char*)

stp_status stp_solver_set_duration_ms_e(stp_solver, stp_option, uint64_t ms)

stp_status stp_solver_set_args(stp_solver, int argc, const char *const *argv)

char *stp_solver_get_str(stp_solver, const char *name)

stp_status stp_solver_get_bool(stp_solver, const char *name, bool *out)

stp_status stp_solver_get_int64(stp_solver, const char *name, int64_t *out)

stp_status stp_solver_get_uint64(stp_solver, const char *name, uint64_t *out)

stp_status stp_solver_get_duration_ms(stp_solver, const char *name, uint64_t *out)

char *stp_solver_resolved_str(stp_solver, const char *name)

bool stp_solver_option_is_set(stp_solver, const char *name)

stp_status stp_solver_reset_option(stp_solver, const char *name)

stp_status stp_solver_reset_all_options(stp_solver)

every entry back to its default, or none: OPTION_TIMING when an entry whose window has closed holds anything else

stp_status stp_solver_resolve_options(stp_solver)

OPTION_CONFLICT / OPTION_UNAVAILABLE, as a check would find them

stp_options stp_solver_options_copy(stp_solver)

a detached copy; delete it

stp_status stp_solver_assert(stp_solver, stp_term)

SORT_MISMATCH unless Bool; FOREIGN_MANAGER; a NULL term is NULL_HANDLE and fails the solver

stp_status stp_solver_push(stp_solver, uint32_t n)

stp_status stp_solver_pop(stp_solver, uint32_t n)

INVALID_ARGUMENT if n > level; nothing removed

uint32_t stp_solver_level(stp_solver)

char *stp_solver_declared_logic(stp_solver)

the logic the last successful parse named in set-logic, “” for none (not the “logic” option); caller-owned (stp_free)

size_t stp_solver_num_assertions(stp_solver)

outermost first

stp_term stp_solver_assertion(stp_solver, size_t i)

stp_status stp_solver_reset_assertions(stp_solver)

keeps options

stp_status stp_solver_reset(stp_solver)

assertions gone, options back to defaults, engine rebuilt

stp_status stp_solver_check_sat(stp_solver, stp_result *out)

out is written on STP_OK only

stp_status stp_solver_check_sat_assuming(stp_solver, size_t n, const stp_term *assumptions, stp_result *out)

stp_status stp_solver_check_sat_budget(stp_solver, size_t n, const stp_term *assumptions, const stp_budget*, stp_result *out)

stp_status stp_solver_entails(stp_solver, stp_term formula, const stp_budget*, stp_entailment *out)

char *stp_solver_last_reason_message(stp_solver)

the sentence behind the LAST result’s reason (”” unless unknown); overwritten by the next check

size_t stp_solver_num_unsat_assumptions(stp_solver)

after unsat: the failed subset (0 if there were no assumptions); after sat/unknown: STATE (and 0)

stp_term stp_solver_unsat_assumption(stp_solver, size_t i)

stp_model stp_solver_model(stp_solver)

models: the model of the last check that answered sat, until the next check (assert/push/pop do not invalidate it) NO_MODEL unless the last check answered sat

stp_model stp_solver_candidate_model(stp_solver)

NULL, no error, if there is none

stp_term stp_solver_value(stp_solver, stp_term)

one lookup in the shared snapshot

void stp_solver_interrupt(stp_solver)

interrupts: safe from any thread and from a signal handler; consumed by the check that reports INTERRUPTED (a check an EXECUTE-mode input runs included); a pending interrupt with no check running makes the next check return INTERRUPTED at once; INTERRUPTED > TIMEOUT > CONFLICT_LIMIT

void stp_solver_clear_interrupt(stp_solver)

discard a pending interrupt

bool stp_solver_interrupt_pending(stp_solver)

stp_status stp_solver_set_terminator(stp_solver, stp_terminate_callback, void *user)

NULL clears

stp_statistics stp_solver_statistics(stp_solver)

a snapshot

stp_term stp_solver_symbol(stp_solver, const char *name)

symbols and scripts (the name table is the manager’s) NULL, no error, if unknown

stp_status stp_solver_parse_smt2(stp_solver, const char *script, stp_parse_mode)

stp_status stp_solver_parse(stp_solver, const char *text, stp_format)

SMT-LIB 2: SMTLIB2 or AUTO

stp_status stp_solver_parse_file(stp_solver, const char *path, stp_format)

SMT-LIB 2: SMTLIB2 or AUTO

stp_term stp_solver_parse_term(stp_solver, const char *smt2_term)

over the manager’s name table

char *stp_solver_to_smt2(stp_solver, bool with_check_sat)

char *stp_solver_to_string(stp_solver, stp_format)

SMTLIB2, DOT, GDL

stp_status stp_solver_write_cnf(stp_solver, stp_text_sink, void *user, stp_cnf_scope *scope)

the batch pipeline encodes the assertions up to its first CNF without solving (whatever incremental says), delivered as DIMACS in one call; *scope (NULL: not wanted) says how the CNF relates to them. Not a check: the last check’s result, model and failed assumptions stay, a pending interrupt stays pending, the CNF sink does not see it. STATE when an interrupt or a budget stops it first; UNSUPPORTED when the pipeline ends before a CNF for another reason

void stp_solver_set_diagnostic_sink(stp_solver, stp_text_sink, void *user)

where diagnostic-tier options write, “Fatal Error:” reports included; NULL: nowhere; must not call the library (STATE)

stp_status stp_solver_parse_source(stp_solver, stp_text_source, void *user, stp_format, stp_parse_mode)

void stp_solver_set_output_sink(stp_solver, stp_text_sink, void *user)

the responses of an EXECUTE or PARSE_ONLY input and what the printing options print; a call with len 0 asks for a flush; NULL: nowhere. A SAT backend’s own report (print-functionstat) comes here from CryptoMiniSat only: CaDiCaL and MiniSat write theirs to stdout themselves. Must not call the library (STATE)

void stp_solver_set_fatal_error_handler(stp_solver, stp_fatal_error_handler, void *user)

told of an engine fatal error in this solver’s work before anything unwinds; may end the process; must not call the library; NULL: none

void stp_solver_set_cnf_sink(stp_solver, stp_cnf_sink, void *user)

every CNF a check hands to the SAT solver, as DIMACS; NULL: none; must not call the library (STATE)