C++ Reference: class EncodingNode

Note: This documentation is automatically generated.

This class represents a number in [0, ub]. The encoding uses ub binary variables x_i with i in [0, ub) where x_i means that the number is > i. It is called an EncodingNode, because it represents one node of the tree used to encode a cardinality constraint.

In practice, not all literals are explicitly created:
   - Only the literals in [lb, current_ub) are "active" at a given time.
   - The represented number is known to be >= lb.
   - It may be greater than current_ub, but the extra literals will be only created lazily. In all our solves, the literal current_ub - 1, will always be assumed to false (i.e. the number will be <= current_ub - 1).
   - Note that lb may increase and ub decrease as more information is learned about this node by the sat solver.

This is roughly based on the cardinality constraint encoding described in: Bailleux and Yacine Boufkhad, "Efficient CNF Encoding of Boolean Cardinality Constraints", In Proc. of CP 2003, pages 108-122, 2003.

Method
`ApplyWeightUpperBound`	Return type: `void` Arguments: `Coefficient gap, SatSolver* solver` Fix any literal that would cause the weight of this node to go over the gap.
`AssumptionIs`	Return type: `bool` Arguments: `Literal other` GetAssumption() might need to create new literals.
`child_a`	Return type: `EncodingNode*`
`child_b`	Return type: `EncodingNode*`
`current_ub`	Return type: `int`
`DebugString`	Return type: `std::string` Arguments: `const VariablesAssignment& assignment` We use the solver to display the current values of the literals.
`depth`	Return type: `int`
`EncodingNode`
`EncodingNode`	Return type: `explicit` Arguments: `Literal l` Constructs a EncodingNode of size one, just formed by the given literal.
`EncodingNode`	Arguments: `int lb, int ub, std::function<Literal(int x)> create_lit` Constructs a node with value in [lb, ub]. New literal "<=x" will be constructed using create_lit(x).
`GetAssumption`	Return type: `Literal` Arguments: `SatSolver* solver`
`GreaterThan`	Return type: `Literal` Arguments: `int i` Returns a literal with the meaning 'this node number is > i'. The given i must be in [lb_, current_ub).
`HasNoWeight`	Return type: `bool`
`IncreaseCurrentUB`	Return type: `bool` Arguments: `SatSolver* solver` Creates a new literals and increases current_ub. Returns false if we were already at the upper bound for this node.
`IncreaseWeightLb`	Return type: `void`
`InitializeFullNode`	Return type: `void` Arguments: `int n, EncodingNode* a, EncodingNode* b, SatSolver* solver` Creates a "full" encoding node on n new variables, the represented number beeing in [lb, ub = lb + n). The variables are added to the given solver with the basic implications linking them: literal(0) >= ... >= literal(n-1)
`InitializeLazyCoreNode`	Return type: `void` Arguments: `Coefficient weight, EncodingNode* a, EncodingNode* b`
`InitializeLazyNode`	Return type: `void` Arguments: `EncodingNode* a, EncodingNode* b, SatSolver* solver` Creates a "lazy" encoding node representing the sum of a and b. Only one literals will be created by this operation. Note that no clauses linking it with a or b are added by this function.
`lb`	Return type: `int`
`literal`	Return type: `Literal` Arguments: `int i`
`Reduce`	Return type: `Coefficient` Arguments: `const SatSolver& solver` Removes the left-side literals fixed to 1. Note that this increases lb_ and reduces the number of active literals. It also removes any right-side literals fixed to 0. If such a literal exists, ub is updated accordingly. Return the overall weight increase.
`set_depth`	Return type: `void` Arguments: `int depth` The depth is mainly used as an heuristic to decide which nodes to merge first. See the < operator.
`set_weight`	Return type: `void` Arguments: `Coefficient w`
`size`	Return type: `int` Accessors to size() and literals in [lb, current_ub).
`ub`	Return type: `int`
`weight`	Return type: `Coefficient`