#include <sat_base.h>

Public Member Functions
	Trail ()

	Trail (const Trail &)=delete
	This type is neither copyable nor movable.

Trail &	operator= (const Trail &)=delete

void	Resize (int num_variables)

void	RegisterPropagator (SatPropagator *propagator)

void	SetCurrentPropagatorId (int propagator_id)

void	FastEnqueue (Literal true_literal)

void	Enqueue (Literal true_literal, int propagator_id)

void	EnqueueSearchDecision (Literal true_literal)
	Specific Enqueue() version for the search decision.

void	EnqueueWithUnitReason (Literal true_literal)
	Specific Enqueue() version for a fixed variable.

void	EnqueueWithSameReasonAs (Literal true_literal, BooleanVariable reference_var)

ABSL_MUST_USE_RESULT bool	EnqueueWithStoredReason (Literal true_literal)

absl::Span< const Literal >	Reason (BooleanVariable var, int64_t conflict_id=-1) const

int	AssignmentType (BooleanVariable var) const

BooleanVariable	ReferenceVarWithSameReason (BooleanVariable var) const

std::vector< Literal > *	GetEmptyVectorToStoreReason (int trail_index) const

std::vector< Literal > *	GetEmptyVectorToStoreReason () const
	Shortcut for GetEmptyVectorToStoreReason(Index()).

void	ChangeReason (int trail_index, int propagator_id)

void	Untrail (int target_trail_index)

void	SetDecisionLevel (int level)
	Changes the decision level used by the next Enqueue().

int	CurrentDecisionLevel () const

std::vector< Literal > *	MutableConflict ()

absl::Span< const Literal >	FailingClause () const
	Returns the last conflict.

void	SetFailingSatClause (SatClause *clause)

SatClause *	FailingSatClause () const

int	NumVariables () const
	Getters.

int64_t	NumberOfEnqueues () const

int	Index () const

std::vector< Literal >::const_iterator	IteratorAt (int index) const

const Literal &	operator[] (int index) const

const VariablesAssignment &	Assignment () const

const AssignmentInfo &	Info (BooleanVariable var) const

std::string	DebugString () const
	Print the current literals on the trail.

void	RegisterDebugChecker (std::function< bool(absl::Span< const Literal > clause)> checker)

Detailed Description

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.

Definition at line 288 of file sat_base.h.

Constructor & Destructor Documentation

◆ Trail() [1/2]

operations_research::sat::Trail::Trail ( )

inline

Definition at line 290 of file sat_base.h.

◆ Trail() [2/2]

operations_research::sat::Trail::Trail ( const Trail & )

delete

This type is neither copyable nor movable.

Member Function Documentation

◆ Assignment()

const VariablesAssignment & operations_research::sat::Trail::Assignment ( ) const

inline

Definition at line 462 of file sat_base.h.

◆ AssignmentType()

int operations_research::sat::Trail::AssignmentType ( BooleanVariable var ) const

inline

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.

Definition at line 671 of file sat_base.h.

◆ ChangeReason()

void operations_research::sat::Trail::ChangeReason	(	int	trail_index,
		int	propagator_id )

inline

Explicitly overwrite the reason so that the given propagator will be asked for it. This is currently only used by the BinaryImplicationGraph.

Definition at line 408 of file sat_base.h.

◆ CurrentDecisionLevel()

int operations_research::sat::Trail::CurrentDecisionLevel ( ) const

inline

Definition at line 427 of file sat_base.h.

◆ DebugString()

std::string operations_research::sat::Trail::DebugString ( ) const

inline

Print the current literals on the trail.

Definition at line 470 of file sat_base.h.

◆ Enqueue()

void operations_research::sat::Trail::Enqueue	(	Literal	true_literal,
		int	propagator_id )

inline

Definition at line 317 of file sat_base.h.

◆ EnqueueSearchDecision()

void operations_research::sat::Trail::EnqueueSearchDecision ( Literal true_literal )

inline

Specific Enqueue() version for the search decision.

Definition at line 323 of file sat_base.h.

◆ EnqueueWithSameReasonAs()

void operations_research::sat::Trail::EnqueueWithSameReasonAs	(	Literal	true_literal,
		BooleanVariable	reference_var )

inline

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.

Definition at line 335 of file sat_base.h.

◆ EnqueueWithStoredReason()

ABSL_MUST_USE_RESULT bool operations_research::sat::Trail::EnqueueWithStoredReason ( Literal true_literal )

inline

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.

Definition at line 347 of file sat_base.h.

◆ EnqueueWithUnitReason()

void operations_research::sat::Trail::EnqueueWithUnitReason ( Literal true_literal )

inline

Specific Enqueue() version for a fixed variable.

Definition at line 328 of file sat_base.h.

◆ FailingClause()

absl::Span< const Literal > operations_research::sat::Trail::FailingClause ( ) const

inline

Returns the last conflict.

Definition at line 439 of file sat_base.h.

◆ FailingSatClause()

SatClause * operations_research::sat::Trail::FailingSatClause ( ) const

inline

Definition at line 450 of file sat_base.h.

◆ FastEnqueue()

void operations_research::sat::Trail::FastEnqueue ( Literal true_literal )

inline

Definition at line 310 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [1/2]

std::vector< Literal > * operations_research::sat::Trail::GetEmptyVectorToStoreReason ( ) const

inline

Shortcut for GetEmptyVectorToStoreReason(Index()).

Definition at line 402 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [2/2]

std::vector< Literal > * operations_research::sat::Trail::GetEmptyVectorToStoreReason ( int trail_index ) const

inline

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.

Definition at line 393 of file sat_base.h.

◆ Index()

int operations_research::sat::Trail::Index ( ) const

inline

Definition at line 455 of file sat_base.h.

◆ Info()

const AssignmentInfo & operations_research::sat::Trail::Info ( BooleanVariable var ) const

inline

Definition at line 463 of file sat_base.h.

◆ IteratorAt()

std::vector< Literal >::const_iterator operations_research::sat::Trail::IteratorAt ( int index ) const

inline

This accessor can return trail_.end(). operator[] cannot. This allows normal std:vector operations, such as assign(begin, end).

Definition at line 458 of file sat_base.h.

◆ MutableConflict()

std::vector< Literal > * operations_research::sat::Trail::MutableConflict ( )

inline

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.

Definition at line 433 of file sat_base.h.

◆ NumberOfEnqueues()

int64_t operations_research::sat::Trail::NumberOfEnqueues ( ) const

inline

Definition at line 454 of file sat_base.h.

◆ NumVariables()

int operations_research::sat::Trail::NumVariables ( ) const

inline

Getters.

Definition at line 453 of file sat_base.h.

◆ operator=()

Trail & operations_research::sat::Trail::operator= ( const Trail & )

delete

◆ operator[]()

const Literal & operations_research::sat::Trail::operator[] ( int index ) const

inline

Definition at line 461 of file sat_base.h.

◆ Reason()

absl::Span< const Literal > operations_research::sat::Trail::Reason	(	BooleanVariable	var,
		int64_t	conflict_id = -1 ) const

inline

Returns the reason why this variable was assigned.

Note: 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.

If conflict_id >= 0, this indicate that this was called as part of the first-UIP procedure. It has a few implication:

The reason do not need to be cached and can be adapted to the current conflict.
Some data can be reused between two calls about the same conflict.
Note however that if the reason is a simple clause, we shouldn't adapt it because we rely on extra fact in the first UIP code where we detect subsumed clauses for instance.

Special case for AssignmentType::kSameReasonAs to avoid a recursive call.

Fast-track for cached reason.

Definition at line 680 of file sat_base.h.

◆ ReferenceVarWithSameReason()

BooleanVariable operations_research::sat::Trail::ReferenceVarWithSameReason ( BooleanVariable var ) const

inline

If a variable was propagated with EnqueueWithSameReasonAs(), returns its reference variable. Otherwise return the given variable.

Note: we don't use AssignmentType() here.

Definition at line 659 of file sat_base.h.

◆ RegisterDebugChecker()

void operations_research::sat::Trail::RegisterDebugChecker ( std::function< bool(absl::Span< const Literal > clause)> checker )

inline

Definition at line 479 of file sat_base.h.

◆ RegisterPropagator()

void operations_research::sat::Trail::RegisterPropagator ( SatPropagator * propagator )

inline

Registers a propagator. This assigns a unique id to this propagator and calls SetPropagatorId() on it.

Definition at line 650 of file sat_base.h.

◆ Resize()

void operations_research::sat::Trail::Resize ( int num_variables )

inline

Todo: (user): these vectors are not always used. Initialize them dynamically.

Definition at line 638 of file sat_base.h.

◆ SetCurrentPropagatorId()

void operations_research::sat::Trail::SetCurrentPropagatorId ( int propagator_id )

inline

Enqueues the assignment that make the given literal true on the trail. This should only be called on unassigned variables.

Definition at line 307 of file sat_base.h.

◆ SetDecisionLevel()

void operations_research::sat::Trail::SetDecisionLevel ( int level )

inline

Changes the decision level used by the next Enqueue().

Definition at line 426 of file sat_base.h.

◆ SetFailingSatClause()

void operations_research::sat::Trail::SetFailingSatClause ( SatClause * clause )

inline

Specific SatClause interface so we can update the conflict clause activity.

Note: MutableConflict() automatically sets this to nullptr, so we can know whether or not the last conflict was caused by a clause.

Definition at line 449 of file sat_base.h.

◆ Untrail()

void operations_research::sat::Trail::Untrail ( int target_trail_index )

inline

Reverts the trail and underlying assignment to the given target trail index. Note that we do not touch the assignment info.

Definition at line 416 of file sat_base.h.

The documentation for this class was generated from the following file:

ortools/sat/sat_base.h

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Trail() [1/2]

◆ Trail() [2/2]

Member Function Documentation

◆ Assignment()

◆ AssignmentType()

◆ ChangeReason()

◆ CurrentDecisionLevel()

◆ DebugString()

◆ Enqueue()

◆ EnqueueSearchDecision()

◆ EnqueueWithSameReasonAs()

◆ EnqueueWithStoredReason()

◆ EnqueueWithUnitReason()

◆ FailingClause()

◆ FailingSatClause()

◆ FastEnqueue()

◆ GetEmptyVectorToStoreReason() [1/2]

◆ GetEmptyVectorToStoreReason() [2/2]

◆ Index()

◆ Info()

◆ IteratorAt()

◆ MutableConflict()

◆ NumberOfEnqueues()

◆ NumVariables()

◆ operator=()

◆ operator[]()

◆ Reason()

◆ ReferenceVarWithSameReason()

◆ RegisterDebugChecker()

◆ RegisterPropagator()

◆ Resize()

◆ SetCurrentPropagatorId()

◆ SetDecisionLevel()

◆ SetFailingSatClause()

◆ Untrail()