C++ Reference: class Trail

Note: This documentation is automatically generated.

The solver trail stores the assignment made by the solver in order. This class is responsible for maintaining the assignment of each variable and the information of each assignment.

Method
`Assignment`	Return type: `const VariablesAssignment&`
`AssignmentType`	Return type: `int` Arguments: `BooleanVariable var` Returns the "type" of an assignment (see AssignmentType). Note that this function never returns kSameReasonAs or kCachedReason, it instead returns the initial type that caused this assignment. As such, it is different from Info(var).type and the latter should not be used outside this class.
`ChangeReason`	Return type: `void` Arguments: `int trail_index, int propagator_id` Explicitly overwrite the reason so that the given propagator will be asked for it. This is currently only used by the BinaryImplicationGraph.
`CurrentDecisionLevel`	Return type: `int`
`DebugString`	Return type: `std::string` Print the current literals on the trail.
`Dequeue`	Return type: `void`
`Enqueue`	Return type: `void` Arguments: `Literal true_literal, int propagator_id` Enqueues the assignment that make the given literal true on the trail. This should only be called on unassigned variables.
`EnqueueSearchDecision`	Return type: `void` Arguments: `Literal true_literal` Specific Enqueue() version for the search decision.
`EnqueueWithSameReasonAs`	Return type: `void` Arguments: `Literal true_literal, BooleanVariable reference_var` Some constraints propagate a lot of literals at once. In these cases, it is more efficient to have all the propagated literals except the first one referring to the reason of the first of them.
`EnqueueWithStoredReason`	Return type: `ABSL_MUST_USE_RESULT bool` Arguments: `Literal true_literal` Enqueues the given literal using the current content of GetEmptyVectorToStoreReason() as the reason. This API is a bit more leanient and does not require the literal to be unassigned. If it is already assigned to false, then MutableConflict() will be set appropriately and this will return false otherwise this will enqueue the literal and returns true.
`EnqueueWithUnitReason`	Return type: `void` Arguments: `Literal true_literal` Specific Enqueue() version for a fixed variable.
`FailingClause`	Return type: `absl::Span<const Literal>` Returns the last conflict.
`FailingSatClause`	Return type: `SatClause*`
`GetEmptyVectorToStoreReason`	Return type: `std::vector<Literal>*` Arguments: `int trail_index` This can be used to get a location at which the reason for the literal at trail_index on the trail can be stored. This clears the vector before returning it.
`GetEmptyVectorToStoreReason`	Return type: `std::vector<Literal>*` Shortcut for GetEmptyVectorToStoreReason(Index()).
`Index`	Return type: `int`
`Info`	Return type: `const AssignmentInfo&` Arguments: `BooleanVariable var`
`IteratorAt`	Return type: `const std::vector<Literal>::const_iterator` Arguments: `int index` This accessor can return trail_.end(). operator[] cannot. This allows normal std:vector operations, such as assign(begin, end).
`MutableConflict`	Return type: `std::vector<Literal>*` Generic interface to set the current failing clause. Returns the address of a vector where a client can store the current conflict. This vector will be returned by the FailingClause() call.
`NumberOfEnqueues`	Return type: `int64_t`
`NumVariables`	Return type: `int` Getters.
`Reason`	Return type: `absl::Span<const Literal>` Arguments: `BooleanVariable var` Returns the reason why this variable was assigned. Note that this shouldn't be called on a variable at level zero, because we don't cleanup the reason data for these variables but the underlying clauses may have been deleted.
`ReferenceVarWithSameReason`	Return type: `BooleanVariable` Arguments: `BooleanVariable var` If a variable was propagated with EnqueueWithSameReasonAs(), returns its reference variable. Otherwise return the given variable.
`RegisterPropagator`	Return type: `void` Arguments: `SatPropagator* propagator` Registers a propagator. This assigns a unique id to this propagator and calls SetPropagatorId() on it.
`Resize`	Return type: `void` Arguments: `int num_variables`
`SetDecisionLevel`	Return type: `void` Arguments: `int level` Changes the decision level used by the next Enqueue().
`SetFailingSatClause`	Return type: `void` Arguments: `SatClause* clause` Specific SatClause interface so we can update the conflict clause activity. Note that MutableConflict() automatically sets this to nullptr, so we can know whether or not the last conflict was caused by a clause.
`Trail`
`Untrail`	Return type: `void` Arguments: `int target_trail_index` Reverts the trail and underlying assignment to the given target trail index. Note that we do not touch the assignment info.