# 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: |

`AssociateToIntegerEqualValue` | Return type: Arguments: |

`AssociateToIntegerLiteral` | Return type: Arguments: 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: Arguments: 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: |

`DisableImplicationBetweenLiteral` | Return type: 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: Arguments: 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: Arguments: 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: Arguments: 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: Arguments: |

`GetAssociatedLiteral` | Return type: Arguments: |

`GetFalseLiteral` | Return type: |

`GetIntegerLiterals` | Return type: Arguments: Returns the IntegerLiterals that were associated with the given Literal. |

`GetLiteralView` | Return type: Arguments: 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: Arguments: 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: Arguments: |

`GetTrueLiteral` | Return type: Gets the literal always set to true, make it if it does not exist. |

`IntegerEncoder` | Return type: Arguments: |

`~IntegerEncoder` | |

`LiteralIsAssociated` | Return type: Arguments: 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: Arguments: If this is true, then a literal can be linearized with an affine expression involving an integer variable. |

`NewlyFixedIntegerLiterals` | Return type: 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: Arguments: 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: Arguments: 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: Arguments: Raw encoding. May be incomplete and is not sorted. Contains all literals, true or false. |

`SearchForLiteralAtOrBefore` | Return type: Arguments: 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: Arguments: Returns true if we know that PartialDomainEncoding(var) span the full domain of var. This is always true if FullyEncodeVariable(var) has been called. |