C++ Reference: class IntegerTrail

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.

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.

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().

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.

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.

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

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.

LevelZeroUpperBound

Return type: IntegerValue

Arguments: IntegerVariable var

LowerBound

Return type: IntegerValue

Arguments: IntegerVariable i

Returns the current lower/upper bound of the given integer variable.

LowerBoundAsLiteral

Return type: IntegerLiteral

Arguments: IntegerVariable i

Returns the integer literal that represent the current lower/upper bound of the given integer variable.

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.

num_enqueues

Return type: int64

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.

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

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

UpperBoundAsLiteral

Return type: IntegerLiteral

Arguments: IntegerVariable i

VariableLowerBoundIsFromLevelZero

Return type: bool

Arguments: IntegerVariable var

Returns true if the variable lower bound is still the one from level zero.

Send feedback about...