|
EncodingNode | LazyMerge (EncodingNode *a, EncodingNode *b, SatSolver *solver) |
|
void | IncreaseNodeSize (EncodingNode *node, SatSolver *solver) |
|
EncodingNode | FullMerge (Coefficient upper_bound, EncodingNode *a, EncodingNode *b, SatSolver *solver) |
|
EncodingNode * | MergeAllNodesWithDeque (Coefficient upper_bound, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository) |
|
EncodingNode * | LazyMergeAllNodeWithPQ (const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository) |
|
std::vector< EncodingNode * > | CreateInitialEncodingNodes (const std::vector< Literal > &literals, const std::vector< Coefficient > &coeffs, Coefficient *offset, std::deque< EncodingNode > *repository) |
|
std::vector< EncodingNode * > | CreateInitialEncodingNodes (const LinearObjective &objective_proto, Coefficient *offset, std::deque< EncodingNode > *repository) |
|
std::vector< Literal > | ReduceNodesAndExtractAssumptions (Coefficient upper_bound, Coefficient stratified_lower_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver) |
|
Coefficient | ComputeCoreMinWeight (const std::vector< EncodingNode * > &nodes, const std::vector< Literal > &core) |
|
Coefficient | MaxNodeWeightSmallerThan (const std::vector< EncodingNode * > &nodes, Coefficient upper_bound) |
|
void | ProcessCore (const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver) |
|