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.

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

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

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

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

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

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 set_terminator(Terminator*)¶: Not owned; nullptr clears. A terminator runs inside the check and must not call the library (STATE), except Solver::interrupt().

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_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).

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).