C++ Reference: class IntegerEncoder

Note: This documentation is automatically generated.

Each integer variable x will be associated with a set of literals encoding (x >= v) for some values of v. This class maintains the relationship between the integer variables and such literals which can be created by a call to CreateAssociatedLiteral().

The advantage of creating such Boolean variables is that the SatSolver which is driving the search can then take this variable as a decision and maintain these variables activity and so on. These variables can also be propagated directly by the learned clauses.

This class also support a non-lazy full domain encoding which will create one literal per possible value in the domain. See FullyEncodeVariable(). This is meant to be called by constraints that directly work on the variable values like a table constraint or an all-diff constraint.

TODO(user): We could also lazily create precedences Booleans between two arbitrary IntegerVariable. This is better done in the PrecedencesPropagator though.

Method
AddAllImplicationsBetweenAssociatedLiterals	Return type: void
AssociateToIntegerEqualValue	Return type: void Arguments: Literal literal, IntegerVariable var, IntegerValue value
AssociateToIntegerLiteral	Return type: void Arguments: Literal literal, IntegerLiteral i_lit Associates the Boolean literal to (X >= bound) or (X == value). If a literal was already associated to this fact, this will add an equality constraints between both literals. If the fact is trivially true or false, this will fix the given literal.
Canonicalize	Return type: std::pair<IntegerLiteral, IntegerLiteral> Arguments: IntegerLiteral i_lit Returns the "canonical" (i_lit, negation of i_lit) pair. This mainly deal with domain with initial hole like [1,2][5,6] so that if one ask for x <= 3, this get canonicalized in the pair (x <= 2, x >= 5). Note that it is an error to call this with a literal that is trivially true or trivially false according to the initial variable domain. This is CHECKed to make sure we don't create wasteful literal. TODO(user): This is linear in the domain "complexity", we can do better if needed.
ClearNewlyFixedIntegerLiterals	Return type: void
DisableImplicationBetweenLiteral	Return type: void Advanced usage. It is more efficient to create the associated literals in order, but it might be anoying to do so. Instead, you can first call DisableImplicationBetweenLiteral() and when you are done creating all the associated literals, you can call (only at level zero) AddAllImplicationsBetweenAssociatedLiterals() which will also turn back on the implications between literals for the one that will be added afterwards.
FullDomainEncoding	Return type: std::vector<ValueLiteralPair> Arguments: IntegerVariable var Computes the full encoding of a variable on which FullyEncodeVariable() has been called. The returned elements are always sorted by increasing IntegerValue and we filter values associated to false literals. Performance note: This function is not particularly fast, however it should only be required during domain creation.
FullyEncodeVariable	Return type: void Arguments: IntegerVariable var Fully encode a variable using its current initial domain. If the variable is already fully encoded, this does nothing. This creates new Booleans variables as needed: 1) num_values for the literals X == value. Except when there is just two value in which case only one variable is created. 2) num_values - 3 for the literals X >= value or X <= value (using their negation). The -3 comes from the fact that we can reuse the equality literals for the two extreme points. The encoding for NegationOf(var) is automatically created too. It reuses the same Boolean variable as the encoding of var. TODO(user): It is currently only possible to call that at the decision level zero because we cannot add ternary clause in the middle of the search (for now). This is Checked.
GetAllIntegerLiterals	Return type: const InlinedIntegerLiteralVector& Arguments: Literal lit Same as GetIntegerLiterals(), but in addition, if the literal was associated to an integer == value, then the returned list will contain both (integer >= value) and (integer <= value).
GetAssociatedEqualityLiteral	Return type: LiteralIndex Arguments: IntegerVariable var, IntegerValue value
GetAssociatedLiteral	Return type: LiteralIndex Arguments: IntegerLiteral i_lit
GetFalseLiteral	Return type: Literal
GetIntegerLiterals	Return type: const InlinedIntegerLiteralVector& Arguments: Literal lit Returns the IntegerLiterals that were associated with the given Literal.
GetLiteralView	Return type: const IntegerVariable Arguments: Literal lit If it exists, returns a [0,1] integer variable which is equal to 1 iff the given literal is true. Returns kNoIntegerVariable if such variable does not exist. Note that one can create one by creating a new IntegerVariable and calling AssociateToIntegerEqualValue().
GetOrCreateAssociatedLiteral	Return type: Literal Arguments: IntegerLiteral i_lit Returns, after creating it if needed, a Boolean literal such that: - if true, then the IntegerLiteral is true. - if false, then the negated IntegerLiteral is true. Note that this "canonicalize" the given literal first. This add the proper implications with the two "neighbor" literals of this one if they exist. This is the "list encoding" in: Thibaut Feydy, Peter J. Stuckey, "Lazy Clause Generation Reengineered", CP 2009.
GetOrCreateLiteralAssociatedToEquality	Return type: Literal Arguments: IntegerVariable var, IntegerValue value
GetTrueLiteral	Return type: Literal Gets the literal always set to true, make it if it does not exist.
IntegerEncoder	Return type: explicit Arguments: Model* model
~IntegerEncoder
LiteralIsAssociated	Return type: bool Arguments: IntegerLiteral i_lit Returns true iff the given integer literal is associated. The second version returns the associated literal or kNoLiteralIndex. Note that none of these function call Canonicalize() first for speed, so it is possible that this returns false even though GetOrCreateAssociatedLiteral() would not create a new literal.
LiteralOrNegationHasView	Return type: ABSL_MUST_USE_RESULT bool Arguments: Literal lit, IntegerVariable* view = nullptr, bool* view_is_direct = nullptr If this is true, then a literal can be linearized with an affine expression involving an integer variable.
NewlyFixedIntegerLiterals	Return type: const std::vector<IntegerLiteral> This is part of a "hack" to deal with new association involving a fixed literal. Note that these are only allowed at the decision level zero.
PartialDomainEncoding	Return type: std::vector<ValueLiteralPair> Arguments: IntegerVariable var Same as FullDomainEncoding() but only returns the list of value that are currently associated to a literal. In particular this has no guarantee to span the full domain of the given variable (but it might).
PartialGreaterThanEncoding	Return type: absl::btree_map<IntegerValue, Literal> Arguments: IntegerVariable var Returns the set of Literal associated to IntegerLiteral of the form var >= value. We make a copy, because this can be easily invalidated when calling any function of this class. So it is less efficient but safer.
RawDomainEncoding	Return type: std::vector<ValueLiteralPair> Arguments: IntegerVariable var Raw encoding. May be incomplete and is not sorted. Contains all literals, true or false.
SearchForLiteralAtOrBefore	Return type: LiteralIndex Arguments: IntegerLiteral i, IntegerValue* bound Returns a Boolean literal associated with a bound lower than or equal to the one of the given IntegerLiteral. If the given IntegerLiteral is true, then the returned literal should be true too. Returns kNoLiteralIndex if no such literal was created. Ex: if 'i' is (x >= 4) and we already created a literal associated to (x >= 2) but not to (x >= 3), we will return the literal associated with (x >= 2).
VariableIsFullyEncoded	Return type: bool Arguments: IntegerVariable var Returns true if we know that PartialDomainEncoding(var) span the full domain of var. This is always true if FullyEncodeVariable(var) has been called.