OR-Tools  9.6
Public Member Functions | List of all members
Trail

Detailed Description

Definition at line 247 of file sat_base.h.

Public Member Functions

 Trail ()
 
void Resize (int num_variables)
 
void RegisterPropagator (SatPropagator *propagator)
 
void Enqueue (Literal true_literal, int propagator_id)
 
void EnqueueSearchDecision (Literal true_literal)
 
void EnqueueWithUnitReason (Literal true_literal)
 
void EnqueueWithSameReasonAs (Literal true_literal, BooleanVariable reference_var)
 
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason (Literal true_literal)
 
absl::Span< const Literal > Reason (BooleanVariable var) const
 
int AssignmentType (BooleanVariable var) const
 
BooleanVariable ReferenceVarWithSameReason (BooleanVariable var) const
 
std::vector< Literal > * GetEmptyVectorToStoreReason (int trail_index) const
 
std::vector< Literal > * GetEmptyVectorToStoreReason () const
 
void ChangeReason (int trail_index, int propagator_id)
 
void Untrail (int target_trail_index)
 
void Dequeue ()
 
void SetDecisionLevel (int level)
 
int CurrentDecisionLevel () const
 
std::vector< Literal > * MutableConflict ()
 
absl::Span< const Literal > FailingClause () const
 
void SetFailingSatClause (SatClause *clause)
 
SatClause * FailingSatClause () const
 
int NumVariables () const
 
int64_t NumberOfEnqueues () const
 
int Index () const
 
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 ()
 
void RegisterDebugChecker (std::function< bool(absl::Span< const Literal > clause)> checker)
 

Constructor & Destructor Documentation

◆ Trail()

Trail ( )
inline

Definition at line 249 of file sat_base.h.

Member Function Documentation

◆ Assignment()

const VariablesAssignment& Assignment ( ) const
inline

Definition at line 402 of file sat_base.h.

◆ AssignmentType()

int AssignmentType ( BooleanVariable  var) const
inline

Definition at line 608 of file sat_base.h.

◆ ChangeReason()

void ChangeReason ( int  trail_index,
int  propagator_id 
)
inline

Definition at line 347 of file sat_base.h.

◆ CurrentDecisionLevel()

int CurrentDecisionLevel ( ) const
inline

Definition at line 367 of file sat_base.h.

◆ DebugString()

std::string DebugString ( )
inline

Definition at line 410 of file sat_base.h.

◆ Dequeue()

void Dequeue ( )
inline

Definition at line 363 of file sat_base.h.

◆ Enqueue()

void Enqueue ( Literal  true_literal,
int  propagator_id 
)
inline

Definition at line 262 of file sat_base.h.

◆ EnqueueSearchDecision()

void EnqueueSearchDecision ( Literal  true_literal)
inline

Definition at line 272 of file sat_base.h.

◆ EnqueueWithSameReasonAs()

void EnqueueWithSameReasonAs ( Literal  true_literal,
BooleanVariable  reference_var 
)
inline

Definition at line 284 of file sat_base.h.

◆ EnqueueWithStoredReason()

ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason ( Literal  true_literal)
inline

Definition at line 296 of file sat_base.h.

◆ EnqueueWithUnitReason()

void EnqueueWithUnitReason ( Literal  true_literal)
inline

Definition at line 277 of file sat_base.h.

◆ FailingClause()

absl::Span<const Literal> FailingClause ( ) const
inline

Definition at line 379 of file sat_base.h.

◆ FailingSatClause()

SatClause* FailingSatClause ( ) const
inline

Definition at line 390 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [1/2]

std::vector<Literal>* GetEmptyVectorToStoreReason ( ) const
inline

Definition at line 341 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [2/2]

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

Definition at line 332 of file sat_base.h.

◆ Index()

int Index ( ) const
inline

Definition at line 395 of file sat_base.h.

◆ Info()

const AssignmentInfo& Info ( BooleanVariable  var) const
inline

Definition at line 403 of file sat_base.h.

◆ IteratorAt()

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

Definition at line 398 of file sat_base.h.

◆ MutableConflict()

std::vector<Literal>* MutableConflict ( )
inline

Definition at line 373 of file sat_base.h.

◆ NumberOfEnqueues()

int64_t NumberOfEnqueues ( ) const
inline

Definition at line 394 of file sat_base.h.

◆ NumVariables()

int NumVariables ( ) const
inline

Definition at line 393 of file sat_base.h.

◆ operator[]()

const Literal& operator[] ( int  index) const
inline

Definition at line 401 of file sat_base.h.

◆ Reason()

absl::Span< const Literal > Reason ( BooleanVariable  var) const
inline

Definition at line 617 of file sat_base.h.

◆ ReferenceVarWithSameReason()

BooleanVariable ReferenceVarWithSameReason ( BooleanVariable  var) const
inline

Definition at line 596 of file sat_base.h.

◆ RegisterDebugChecker()

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

Definition at line 419 of file sat_base.h.

◆ RegisterPropagator()

void RegisterPropagator ( SatPropagator *  propagator)
inline

Definition at line 587 of file sat_base.h.

◆ Resize()

void Resize ( int  num_variables)
inline

Definition at line 575 of file sat_base.h.

◆ SetDecisionLevel()

void SetDecisionLevel ( int  level)
inline

Definition at line 366 of file sat_base.h.

◆ SetFailingSatClause()

void SetFailingSatClause ( SatClause *  clause)
inline

Definition at line 389 of file sat_base.h.

◆ Untrail()

void Untrail ( int  target_trail_index)
inline

Definition at line 355 of file sat_base.h.

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