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.