C++ Reference: class Trail

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.

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

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

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.

SetLastPolarity

Return type: void

Arguments: BooleanVariable var, bool polarity

Trail

Return type: explicit

Arguments: Model* model

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.