Solver¶

class Solver¶

Public Functions

explicit Solver(TermManager tm, Options options = Options())¶: Copies options; resolve() runs here. Any number of solvers may be live over one manager; each has its own assertion stack, options and models.

Solver(Solver&&) noexcept¶

Solver &operator=(Solver&&) noexcept¶

Solver(const Solver&) = delete¶

Solver &operator=(const Solver&) = delete¶

~Solver()¶

TermManager manager() const¶

SolverOptions &options()¶: live

const SolverOptions &options() const¶

void assert_formula(const Term &bool_term)¶: SORT_MISMATCH unless Bool; FOREIGN_MANAGER.

inline void add(const Term &bool_term)¶

void push(std::uint32_t n = 1)¶

void pop(std::uint32_t n = 1)¶: INVALID_ARGUMENT if n > level(); nothing removed.

std::uint32_t level() const noexcept¶

std::string declared_logic() const¶: The logic the last parse that succeeded named in its set-logic, or “” when it named none or a reset came after it (the script’s own (reset), reset() or reset_assertions()); a failed parse leaves it as it was. A script’s set-logic does not set the logic option, which is the caller’s.

std::vector<Term> assertions() const¶: outermost first

void reset_assertions()¶: keeps options; clears a before-search hook not yet used

void reset()¶: assertions gone, options back to defaults, engine rebuilt, no before-search hook

Result check_sat()¶

Result check_sat(const std::vector<Term> &assumptions, std::optional<CheckBudget> budget = std::nullopt)¶

void set_before_search(BeforeSearch hook, std::string reason, NoSearchPoint otherwise = NoSearchPoint::abandon)¶: A hook for the next check_sat or entails that starts, which consumes it whatever becomes of it (answered, abandoned, interrupted or failed). A call refused before its check starts (an argument, sort, option or unsupported-content error) leaves it set, and reset() and reset_assertions() clear it; write_cnf and a parse in EXECUTE mode refuse to run while one is set (STATE). The check takes the batch pipeline, and hook runs at most once, at the moment the check’s SAT backend, with its CNF loaded, would start to search. A check decided before that (by preprocessing) answers, and the hook is never called. Arithmetic-only refinement is supported: copies retain the common atom meanings and certify their models and conflicts exactly. Other refinement refuses the point: lazy array axioms, uninterpreted functions, and the bit-vector and floating-point abstractions (their options alone refuse, whatever the query holds). An array equality the pipeline expands eagerly instead — most equalities between stores over bit-vector arrays — is offered; one left to lazy extensionality (a large one, or one over a constant array or floating-point elements) refuses. Such a check does what otherwise says, at that same moment and without calling the hook: abandoned, unknown (INCOMPLETE) with a reason saying why followed by reason, or searched in place, on the batch pipeline. The statistics before-search.outcome and before-search.refusal say which happened. (A model on eager array axioms that fails its replay still refines a check after the hook; that is sound for copies sharing clauses, since the axioms are valid for the query and their new variables lie above every cutoff.) true lets the check search; false abandons it, unknown (INCOMPLETE) with reason, as does a throw. reason must not be empty (INVALID_ARGUMENT); nullptr clears a hook not yet used. The hook reaches the solver only through its SearchPoint. It may fork(): every copy then holds the loaded backend and continues the same check, provided the caller is single-threaded at that point (libstp starts no threads and holds no lock across the hook) and handles the descriptors the copies inherit.

Entailment entails(const Term &formula, std::optional<CheckBudget> budget = std::nullopt)¶

std::vector<Term> unsat_assumptions() const¶: after unsat: the failed subset; after sat/unknown: STATE

Model model() const¶: The model of the last check that answered sat, until the next check (assert, push and pop do not invalidate it). NO_MODEL otherwise.

std::optional<Model> candidate_model() const¶: after unknown: the last candidate

inline Term value(const Term &t) const¶

void interrupt() noexcept¶: Thread-safe and async-signal-safe. The flag is CONSUMED by the check that reports it — a check an input read with ParseMode::EXECUTE runs as much as check_sat’s; if no check is running, the next check returns unknown(INTERRUPTED) immediately. clear_interrupt() discards a pending interrupt. INTERRUPTED > TIMEOUT > CONFLICT_LIMIT when several fire. The terminator reaches a script’s checks the same way.

void clear_interrupt() noexcept¶

bool interrupt_pending() const noexcept¶

void set_terminator(Terminator*)¶: Not owned; nullptr clears. A terminator runs inside the check and must not call the library (STATE), except Solver::interrupt().

Statistics statistics() const¶

std::optional<Term> symbol(std::string_view name) const¶

void parse_smt2(std::string_view script, ParseMode = ParseMode::DECLARE_AND_ASSERT)¶: Definitions surviving a successful parse belong to the manager too; later parses and parse_term can use them. Their names cannot be redefined or declared. A script’s reset does not discard the manager’s retained declarations, definitions or handles. Redeclaring a retained name with a different identity is PARSE, with the assertion stack restored. In particular, declare-sort creates a new identity even at the same spelling; use a fresh manager for a new namespace. Ordinary symbols redeclared at the same sort keep their identity. A NUL in script is INVALID_ARGUMENT: the lexer would end the script there, silently. So is one in a stream (parse), when it is reached.

void parse(std::string_view text, Format)¶: SMT-LIB 2: SMTLIB2 or AUTO.

void parse_file(std::string_view path, Format = Format::AUTO)¶: SMT-LIB 2: SMTLIB2 or AUTO

void parse(std::istream &in, Format, ParseMode = ParseMode::DECLARE_AND_ASSERT)¶: Reads the input from a stream as far as the parser needs it, taking what the stream holds after at most one refill: a script driven over a pipe is answered command by command. AUTO reads SMT-LIB 2. IO if the stream fails, which ends the parse there. The stream’s reads run as a callback (no library calls) and under the process-wide parser lock.

Term parse_term(std::string_view smt2_term) const¶: over the manager’s name table

std::string to_smt2(bool with_check_sat = false) const¶: The assertions as a script a fresh manager reads back: the logic their content and the manager’s declarations need, the declarations, the assertion levels as pushes. produce-models prints as a set-option, the solver’s other options as “; name = value” comments. Through the engine’s printers, which recurse once per level of a term (see Term::to_string).

std::string to_string(Format) const¶: SMTLIB2 (to_smt2(false)), DOT or GDL.

CnfScope write_cnf(std::ostream&) const¶: DIMACS of the current assertions: the batch pipeline encodes them up to its first CNF without solving, whatever incremental says, and the scope says how that CNF relates to them. Not a check: the last check’s result, model and failed assumptions stay, a pending interrupt stays pending, and 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 set_diagnostic_sink(std::function<void(std::string_view)>)¶: Where diagnostic-tier options write: statistics, warnings and the other text the engine prints for people rather than programs, “Fatal Error:” reports included. Default: nowhere. A sink must not call the library (STATE); nor must any other callback.

void set_output_sink(std::function<void(std::string_view)>)¶: Where the solver’s printed output goes: the responses of an input read with ParseMode::EXECUTE or PARSE_ONLY, and what the printing options print. Default: nowhere. An empty chunk asks the sink to flush: the text so far is complete. A SAT backend’s own report, which print-functionstat switches on, reaches this sink from CryptoMiniSat only: CaDiCaL and MiniSat write theirs to standard output themselves. It must not call the library (STATE).

void set_fatal_error_handler(std::function<void(std::string_view)>)¶: Called with the engine’s report of a fatal error in this solver’s work (an internal failure, or a refusal that ends a parse) where it happens, before anything unwinds; the report also reaches the diagnostic sink as “Fatal Error: …”. The handler may end the process; if it returns, the call fails as it otherwise would. It must not call the library. Default: none.

void set_cnf_sink(std::function<void(std::string_view dimacs, CnfScope)>)¶: Every CNF a check hands to the SAT solver, as DIMACS, and how it relates to the query; a check can hand over several (refinement). Default: none. It must not call the library (STATE).