C++ Reference: class IntegerTrail

Note: This documentation is automatically generated.

This class maintains a set of integer variables with their current bounds. Bounds can be propagated from an external "source" and this class helps to maintain the reason for each propagation.

Method
`AddIntegerVariable`	Return type: `IntegerVariable` Arguments: `IntegerValue lower_bound, IntegerValue upper_bound` Adds a new integer variable. Adding integer variable can only be done when the decision level is zero (checked). The given bounds are INCLUSIVE and must not cross. Note on integer overflow: 'upper_bound - lower_bound' must fit on an int64_t, this is DCHECKed. More generally, depending on the constraints that are added, the bounds magnitude must be small enough to satisfy each constraint overflow precondition.
`AddIntegerVariable`	Return type: `IntegerVariable` Arguments: `const Domain& domain` Same as above but for a more complex domain specified as a sorted list of disjoint intervals. See the Domain class.
`AddIntegerVariable`	Return type: `IntegerVariable` Same as AddIntegerVariable() but uses the maximum possible range. Note that since we take negation of bounds in various places, we make sure that we don't have overflow when we take the negation of the lower bound or of the upper bound.
`AppendNewBounds`	Return type: `void` Arguments: `std::vector<IntegerLiteral>* output` Inspects the trail and output all the non-level zero bounds (one per variables) to the output. The algo is sparse if there is only a few propagations on the trail.
`AppendRelaxedLinearReason`	Return type: `void` Arguments: `IntegerValue slack, absl::Span<const IntegerValue> coeffs, absl::Span<const IntegerVariable> vars, std::vector<IntegerLiteral>* reason` Same as above but take in IntegerVariables instead of IntegerLiterals.
`ConditionalEnqueue`	Return type: `ABSL_MUST_USE_RESULT bool` Arguments: `Literal lit, IntegerLiteral i_lit, std::vector<Literal>* literal_reason, std::vector<IntegerLiteral>* integer_reason` Pushes the given integer literal assuming that the Boolean literal is true. This can do a few things: - If lit it true, add it to the reason and push the integer bound. - If the bound is infeasible, push lit to false. - If the underlying variable is optional and also controlled by lit, push the bound even if lit is not assigned.
`ConditionalLowerBound`	Return type: `IntegerValue` Arguments: `Literal l, IntegerVariable i` Advanced usage. Returns the current lower bound assuming the literal is true.
`ConditionalLowerBound`	Return type: `IntegerValue` Arguments: `Literal l, AffineExpression expr`
`CurrentBranchHadAnIncompletePropagation`	Return type: `bool` If we had an incomplete propagation, it is important to fix all the variables and not relly on the propagation to do so. This is related to the InPropagationLoop() code above.
`Enqueue`	Return type: `ABSL_MUST_USE_RESULT bool` Arguments: `IntegerLiteral i_lit, absl::Span<const Literal> literal_reason, absl::Span<const IntegerLiteral> integer_reason` Enqueue new information about a variable bound. Calling this with a less restrictive bound than the current one will have no effect. The reason for this "assignment" must be provided as: - A set of Literal currently beeing all false. - A set of IntegerLiteral currently beeing all true. IMPORTANT: Notice the inversed sign in the literal reason. This is a bit confusing but internally SAT use this direction for efficiency. Note(user): Duplicates Literal/IntegerLiteral are supported because we call STLSortAndRemoveDuplicates() in MergeReasonInto(), but maybe they shouldn't for efficiency reason. TODO(user): If the given bound is equal to the current bound, maybe the new reason is better? how to decide and what to do in this case? to think about it. Currently we simply don't do anything.
`Enqueue`	Return type: `ABSL_MUST_USE_RESULT bool` Arguments: `IntegerLiteral i_lit, absl::Span<const Literal> literal_reason, absl::Span<const IntegerLiteral> integer_reason, int trail_index_with_same_reason` Same as Enqueue(), but takes an extra argument which if smaller than integer_trail_.size() is interpreted as the trail index of an old Enqueue() that had the same reason as this one. Note that the given Span must still be valid as they are used in case of conflict. TODO(user): This currently cannot refer to a trail_index with a lazy reason. Fix or at least check that this is the case.
`Enqueue`	Return type: `ABSL_MUST_USE_RESULT bool` Arguments: `IntegerLiteral i_lit, LazyReasonFunction lazy_reason`
`EnqueueLiteral`	Return type: `void` Arguments: `Literal literal, absl::Span<const Literal> literal_reason, absl::Span<const IntegerLiteral> integer_reason` Enqueues the given literal on the trail. See the comment of Enqueue() for the reason format.
`FindTrailIndexOfVarBefore`	Return type: `int` Arguments: `IntegerVariable var, int threshold` Returns the trail index < threshold of a TrailEntry about var. Returns -1 if there is no such entry (at a positive decision level). This is basically the trail index of the lower bound of var at the time. Important: We do some optimization internally, so this should only be used from within a LazyReasonFunction().
`FirstUnassignedVariable`	Return type: `IntegerVariable`
`FixedValue`	Return type: `IntegerValue` Arguments: `IntegerVariable i` Checks that the variable is fixed and returns its value.
`FixedValue`	Return type: `IntegerValue` Arguments: `AffineExpression expr`
`GetOrCreateConstantIntegerVariable`	Return type: `IntegerVariable` Arguments: `IntegerValue value` Same as AddIntegerVariable(value, value), but this is a bit more efficient because it reuses another constant with the same value if its exist. Note(user): Creating constant integer variable is a bit wasteful, but not that much, and it allows to simplify a lot of constraints that do not need to handle this case any differently than the general one. Maybe there is a better solution, but this is not really high priority as of December 2016.
`HasPendingRootLevelDeduction`	Return type: `bool` Return true if we can fix new fact at level zero.
`Index`	Return type: `int`
`InitialVariableDomain`	Return type: `const Domain&` Arguments: `IntegerVariable var` Returns the initial domain of the given variable. Note that the min/max are updated with level zero propagation, but not holes.
`InPropagationLoop`	Return type: `bool` Basic heuristic to detect when we are in a propagation loop, and suggest a good variable to branch on (taking the middle value) to get out of it.
`IntegerLiteralIsFalse`	Return type: `bool` Arguments: `IntegerLiteral l`
`IntegerLiteralIsTrue`	Return type: `bool` Arguments: `IntegerLiteral l` Returns the current value (if known) of an IntegerLiteral.
`IntegerTrail`	Return type: `explicit` Arguments: `Model* model`
`~IntegerTrail`
`IsCurrentlyIgnored`	Return type: `bool` Arguments: `IntegerVariable i`
`IsFixed`	Return type: `bool` Arguments: `IntegerVariable i` Checks if the variable is fixed.
`IsFixed`	Return type: `bool` Arguments: `AffineExpression expr`
`IsFixedAtLevelZero`	Return type: `bool` Arguments: `IntegerVariable var` Returns true if the variable is fixed at level 0.
`IsFixedAtLevelZero`	Return type: `bool` Arguments: `AffineExpression expr` Returns true if the affine expression is fixed at level 0.
`IsIgnoredLiteral`	Return type: `Literal` Arguments: `IntegerVariable i`
`IsOptional`	Return type: `bool` Arguments: `IntegerVariable i` For an optional variable, both its lb and ub must be valid bound assuming the fact that the variable is "present". However, the domain [lb, ub] is allowed to be empty (i.e. ub < lb) if the given is_ignored literal is true. Moreover, if is_ignored is true, then the bound of such variable should NOT impact any non-ignored variable in any way (but the reverse is not true).
`LevelZeroLowerBound`	Return type: `IntegerValue` Arguments: `IntegerVariable var` Returns globally valid lower/upper bound on the given integer variable.
`LevelZeroLowerBound`	Return type: `IntegerValue` Arguments: `AffineExpression exp` Returns globally valid lower/upper bound on the given affine expression.
`LevelZeroUpperBound`	Return type: `IntegerValue` Arguments: `IntegerVariable var`
`LevelZeroUpperBound`	Return type: `IntegerValue` Arguments: `AffineExpression exp`
`LowerBound`	Return type: `IntegerValue` Arguments: `IntegerVariable i` Returns the current lower/upper bound of the given integer variable.
`LowerBound`	Return type: `IntegerValue` Arguments: `AffineExpression expr` Same as above for an affine expression.
`LowerBoundAsLiteral`	Return type: `IntegerLiteral` Arguments: `IntegerVariable i` Returns the integer literal that represent the current lower/upper bound of the given integer variable.
`LowerBoundAsLiteral`	Return type: `IntegerLiteral` Arguments: `AffineExpression expr` Returns the integer literal that represent the current lower/upper bound of the given affine expression. In case the expression is constant, it returns IntegerLiteral::TrueLiteral().
`MarkIntegerVariableAsOptional`	Return type: `void` Arguments: `IntegerVariable i, Literal is_considered`
`MergeReasonInto`	Return type: `void` Arguments: `absl::Span<const IntegerLiteral> literals, std::vector<Literal>* output` Appends the reason for the given integer literals to the output and call STLSortAndRemoveDuplicates() on it.
`NextVariableToBranchOnInPropagationLoop`	Return type: `IntegerVariable`
`NotifyThatPropagationWasAborted`	Return type: `void`
`num_enqueues`	Return type: `int64_t` Returns the number of enqueues that changed a variable bounds. We don't count enqueues called with a less restrictive bound than the current one. Note(user): this can be used to see if any of the bounds changed. Just looking at the integer trail index is not enough because at level zero it doesn't change since we directly update the "fixed" bounds.
`num_level_zero_enqueues`	Return type: `int64_t` Same as num_enqueues but only count the level zero changes.
`NumConstantVariables`	Return type: `int`
`NumIntegerVariables`	Return type: `IntegerVariable` Returns the number of created integer variables. Note that this is twice the number of call to AddIntegerVariable() since we automatically create the NegationOf() variable too.
`OptionalLiteralIndex`	Return type: `LiteralIndex` Arguments: `IntegerVariable i`
`Propagate`	Return type: `bool` Arguments: `Trail* trail` SatPropagator interface. These functions make sure the current bounds information is in sync with the current solver literal trail. Any class/propagator using this class must make sure it is synced to the correct state before calling any of its functions.
`Reason`	Return type: `absl::Span<const Literal>` Arguments: `const Trail& trail, int trail_index`
`ReasonFor`	Return type: `std::vector<Literal>` Arguments: `IntegerLiteral literal` Returns the reason (as set of Literal currently false) for a given integer literal. Note that the bound must be less restrictive than the current bound (checked).
`RegisterReversibleClass`	Return type: `void` Arguments: `ReversibleInterface* rev` Registers a reversible class. This class will always be synced with the correct decision level.
`RegisterWatcher`	Return type: `void` Arguments: `SparseBitset<IntegerVariable>* p` All the registered bitsets will be set to one each time a LbVar is modified. It is up to the client to clear it if it wants to be notified with the newly modified variables.
`RelaxLinearReason`	Return type: `void` Arguments: `IntegerValue slack, absl::Span<const IntegerValue> coeffs, std::vector<IntegerLiteral>* reason` Advanced usage. Given the reason for (Sum_i coeffs[i] * reason[i].var >= current_lb) initially in reason, this function relaxes the reason given that we only need the explanation of (Sum_i coeffs[i] * reason[i].var >= current_lb - slack). Preconditions: - coeffs must be of same size as reason, and all entry must be positive. - *reason must initially contains the trivial initial reason, that is the current lower-bound of each variables. TODO(user): Requiring all initial literal to be at their current bound is not really clean. Maybe we can change the API to only take IntegerVariable and produce the reason directly. TODO(user): change API so that this work is performed during the conflict analysis where we can be smarter in how we relax the reason. Note however that this function is mainly used when we have a conflict, so this is not really high priority. TODO(user): Test that the code work in the presence of integer overflow.
`RelaxLinearReason`	Return type: `void` Arguments: `IntegerValue slack, absl::Span<const IntegerValue> coeffs, std::vector<int>* trail_indices` Same as above but relax the given trail indices.
`RemoveLevelZeroBounds`	Return type: `void` Arguments: `std::vector<IntegerLiteral>* reason` Removes from the reasons the literal that are always true. This is mainly useful for experiments/testing.
`ReportConflict`	Return type: `bool` Arguments: `absl::Span<const Literal> literal_reason, absl::Span<const IntegerLiteral> integer_reason` Helper functions to report a conflict. Always return false so a client can simply do: return integer_trail_->ReportConflict(...);
`ReportConflict`	Return type: `bool` Arguments: `absl::Span<const IntegerLiteral> integer_reason`
`ReserveSpaceForNumVariables`	Return type: `void` Arguments: `int num_vars` Optimization: you can call this before calling AddIntegerVariable() num_vars time.
`SafeEnqueue`	Return type: `ABSL_MUST_USE_RESULT bool` Arguments: `IntegerLiteral i_lit, absl::Span<const IntegerLiteral> integer_reason` Enqueue new information about a variable bound. It has the same behavior as the Enqueue() method, except that it accepts true and false integer literals, both for i_lit, and for the integer reason. This method will do nothing if i_lit is a true literal. It will report a conflict if i_lit is a false literal, and enqueue i_lit normally otherwise. Furthemore, it will check that the integer reason does not contain any false literals, and will remove true literals before calling ReportConflict() or Enqueue().
`timestamp`	Return type: `int64_t`
`Untrail`	Return type: `void` Arguments: `const Trail& trail, int literal_trail_index`
`UpdateInitialDomain`	Return type: `bool` Arguments: `IntegerVariable var, Domain domain` Takes the intersection with the current initial variable domain. TODO(user): There is some memory inefficiency if this is called many time because of the underlying data structure we use. In practice, when used with a presolve, this is not often used, so that is fine though.
`UpperBound`	Return type: `IntegerValue` Arguments: `IntegerVariable i`
`UpperBound`	Return type: `IntegerValue` Arguments: `AffineExpression expr`
`UpperBoundAsLiteral`	Return type: `IntegerLiteral` Arguments: `IntegerVariable i`
`UpperBoundAsLiteral`	Return type: `IntegerLiteral` Arguments: `AffineExpression expr`
`VariableLowerBoundIsFromLevelZero`	Return type: `bool` Arguments: `IntegerVariable var` Returns true if the variable lower bound is still the one from level zero.