![]() |
Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
|
#include <synchronization.h>
Public Member Functions | |
SharedClausesManager (bool always_synchronize) | |
void | AddBinaryClause (int id, int lit1, int lit2) |
const CompactVectorVector< int > & | GetUnseenClauses (int id) |
void | AddBatch (int id, CompactVectorVector< int > batch) |
void | GetUnseenBinaryClauses (int id, std::vector< std::pair< int, int > > *new_clauses) |
int | RegisterNewId (bool may_terminate_early) |
Ids are used to identify which worker is exporting/importing clauses. | |
void | SetWorkerNameForId (int id, absl::string_view worker_name) |
void | LogStatistics (SolverLogger *logger) |
Search statistics. | |
void | Synchronize () |
This class holds clauses found and shared by workers. It is exact for binary clauses, but approximate for longer ones.
It is thread-safe.
Definition at line 715 of file synchronization.h.
|
explicit |
Definition at line 1240 of file synchronization.cc.
void operations_research::sat::SharedClausesManager::AddBatch | ( | int | id, |
CompactVectorVector< int > | batch ) |
Definition at line 1284 of file synchronization.cc.
void operations_research::sat::SharedClausesManager::AddBinaryClause | ( | int | id, |
int | lit1, | ||
int | lit2 ) |
Small optim. If the worker is already up to date with clauses to import, we can mark this new clause as already seen.
Definition at line 1264 of file synchronization.cc.
void operations_research::sat::SharedClausesManager::GetUnseenBinaryClauses | ( | int | id, |
std::vector< std::pair< int, int > > * | new_clauses ) |
Fills new_clauses with {{lit1 of clause1, lit2 of clause1}, {lit1 of clause2, lit2 of clause2}, ...}
Definition at line 1305 of file synchronization.cc.
const CompactVectorVector< int > & operations_research::sat::SharedClausesManager::GetUnseenClauses | ( | int | id | ) |
Returns new glue clauses. The spans are guaranteed to remain valid until the next call to SyncClauses().
Definition at line 1290 of file synchronization.cc.
void operations_research::sat::SharedClausesManager::LogStatistics | ( | SolverLogger * | logger | ) |
Search statistics.
Definition at line 1318 of file synchronization.cc.
int operations_research::sat::SharedClausesManager::RegisterNewId | ( | bool | may_terminate_early | ) |
Ids are used to identify which worker is exporting/importing clauses.
Definition at line 1243 of file synchronization.cc.
void operations_research::sat::SharedClausesManager::SetWorkerNameForId | ( | int | id, |
absl::string_view | worker_name ) |
Definition at line 1258 of file synchronization.cc.
void operations_research::sat::SharedClausesManager::Synchronize | ( | ) |
Unlocks waiting binary clauses for workers if always_synchronize is false. Periodically starts a new sharing round, making glue clauses visible.
Delete batches that have been consumed by all workers. Keep a few batches around for startup (min finished batch doesn't count workers that haven't registered yet).
Definition at line 1335 of file synchronization.cc.