ClauseExchange

class ClauseExchange

Learned-clause exchange between copies of one check’s SAT backend, forked at its before-search point (Solver::set_before_search) and connected there (SearchPoint::connect_clause_exchange). Literals are the backend’s own numbering, which every copy forked at that point shares and which means nothing outside that group. Every clause next() hands over must have been learned() by such a copy: it then holds in every model of the query. It is implied by the clauses every copy shares plus, in a copy that refined after the point (eager array axioms whose model failed replay), lemmas valid for the query — provided every copy runs the same backend options (diversify() changes only the search), no technique that removes models runs between the fork and the connection, and variables created after the connection (the backend’s extension variables, a refinement’s encoding) lie above the cutoff, so no exported clause names one. Both run inside the search: they must not call back into the solver and must not throw.

Public Functions

virtual ~ClauseExchange()

virtual void learned(const int *literals, std::size_t size) noexcept = 0

A clause the backend learned: at most max_size literals, all over the variables that existed when the exchange was connected.

virtual bool next(std::vector<int> &literals) noexcept = 0

One clause to import, replacing the contents of literals, or false when none is pending.

inline virtual void begin_import(std::size_t) noexcept

The start of an import poll, before its first next(): the poll takes every unit and at most budget clauses of two or more literals (the settings’ import_budget, or the backend’s own cap when that is 0). An exchange may select the poll’s clauses here; the poll ends at the first next() returning false.