C++ Reference: class IntegerEncoder

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

FullyEncodeVariable

Return type: void

Arguments: IntegerVariable var

Fully encode a variable using its current initial domain. This can be called only once. 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).

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.

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: std::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.

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 iff FullyEncodeVariable(var) has been called. Note that PartialDomainEncoding() may actually return a full domain encoding, but if FullyEncodeVariable() was not called, this will still return false. TODO(user): Detect this case and mark such variable as fully encoded?

Send feedback about...