SearchPoint

class SearchPoint

A check’s SAT backend at its before-search point (Solver::set_before_search): the check’s CNF is loaded and nothing has searched. Valid only inside the hook it is handed to.

Public Functions

std::uint64_t variables() const

The variables STP’s encoding numbered. The exchange’s cutoff (sat.exchange.variables) is the backend’s own count at connection, which may be smaller (a numbered variable no clause mentions); the backend’s extension variables (cadical-factor) appear only during the search, above it.

bool connect_clause_exchange(ClauseExchange *exchange, const ClauseExchangeSettings &settings = {})

Connect exchange (not owned; nullptr disconnects) to this check’s backend, exporting only clauses over the variables it holds now. false when the backend cannot exchange clauses (CaDiCaL without STP’s clause-import extension). Arithmetic-only refinement is supported. A backend rebuild stops sharing because its variable numbering is private. The closing counters are the solver’s sat.exchange.* statistics.

bool diversify(const SearchDiversification &diversification)

Diversify this check’s search (SearchDiversification). false when the backend does not support it; nothing then changed. Accepted settings are restored on replacement backends of this check, without calling the hook again or reconnecting its clause exchange.

SearchPoint(const SearchPoint&) = delete

SearchPoint &operator=(const SearchPoint&) = delete

Friends

friend struct detail::SearchPointAccess