|
| bool | clone |
| | Whether engines create a clone when being initialized.
|
| double | threads |
| | Number of threads to use.
|
| unsigned int | c_d |
| | Create a clone after every c_d commits (commit distance).
|
| unsigned int | a_d |
| | Create a clone during recomputation if distance is greater than a_d (adaptive distance).
|
| unsigned int | d_l |
| | Discrepancy limit (for LDS).
|
| unsigned int | assets |
| | Number of assets (engines) in a portfolio.
|
| unsigned int | slice |
| | Size of a slice in a portfolio (in number of failures).
|
| unsigned int | nogoods_limit |
| | Depth limit for extraction of no-goods.
|
| Stop * | stop |
| | Stop object for stopping search.
|
| Cutoff * | cutoff |
| | Cutoff for restart-based search.
|
| SearchTracer * | tracer |
| | Tracer object for tracing search.
|
Search engine options
Defines options for search engines. Not all search engines might honor all option values.
- c_d as minimal recomputation distance: this guarantees that a path between two nodes in the search tree for which copies are stored has at least length c_d. That is, in order to recompute a node in the search tree, c_d recomputation steps are needed. The minimal recomputation distance yields a guarantee on saving memory compared to full copying: it stores c_d times less nodes than full copying.
- a_d as adaptive recomputation distance: when a node needs to be recomputed and the path is longer than a_d, an intermediate copy is created (approximately in the middle of the path) to speed up future recomputation. Note that small values of a_d can increase the memory consumption considerably.
Full copying corresponds to a maximal recomputation distance c_d of 1.
All recomputation performed is based on batch recomputation: batch recomputation performs propagation only once for an entire path used in recomputation.
The number of threads to be used is controlled by a double \(n\) (assume that \(m\) is the number of processing units available). If \(1 \leq n\), \(n\) threads are chosen (of course with rounding). If \(n \leq -1\), then \(m + n\) threads are chosen (all but \(-n\) processing units get a thread). If \(n\) is zero, \(m\) threads are chosen. If \(0<n<1\), \(n \times m\) threads are chosen. If \(-1 <n<0\), \((1+n)\times m\) threads are chosen.
Definition at line 751 of file search.hh.
