OR-Tools  8.2
Trail

Detailed Description

Definition at line 233 of file sat_base.h.

Public Member Functions

 Trail (Model *model)
 
 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 LiteralReason (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 LiteralFailingClause () const
 
void SetFailingSatClause (SatClause *clause)
 
SatClauseFailingSatClause () const
 
int NumVariables () const
 
int64 NumberOfEnqueues () const
 
int Index () const
 
const Literaloperator[] (int index) const
 
const VariablesAssignmentAssignment () const
 
const AssignmentInfoInfo (BooleanVariable var) const
 
std::string DebugString ()
 

Constructor & Destructor Documentation

◆ Trail() [1/2]

Trail ( Model model)
inlineexplicit

Definition at line 235 of file sat_base.h.

◆ Trail() [2/2]

Trail ( )
inline

Definition at line 237 of file sat_base.h.

Member Function Documentation

◆ Assignment()

const VariablesAssignment& Assignment ( ) const
inline

Definition at line 380 of file sat_base.h.

◆ AssignmentType()

int AssignmentType ( BooleanVariable  var) const
inline

Definition at line 572 of file sat_base.h.

◆ ChangeReason()

void ChangeReason ( int  trail_index,
int  propagator_id 
)
inline

Definition at line 335 of file sat_base.h.

◆ CurrentDecisionLevel()

int CurrentDecisionLevel ( ) const
inline

Definition at line 355 of file sat_base.h.

◆ DebugString()

std::string DebugString ( )
inline

Definition at line 388 of file sat_base.h.

◆ Dequeue()

void Dequeue ( )
inline

Definition at line 351 of file sat_base.h.

◆ Enqueue()

void Enqueue ( Literal  true_literal,
int  propagator_id 
)
inline

Definition at line 250 of file sat_base.h.

◆ EnqueueSearchDecision()

void EnqueueSearchDecision ( Literal  true_literal)
inline

Definition at line 260 of file sat_base.h.

◆ EnqueueWithSameReasonAs()

void EnqueueWithSameReasonAs ( Literal  true_literal,
BooleanVariable  reference_var 
)
inline

Definition at line 272 of file sat_base.h.

◆ EnqueueWithStoredReason()

ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason ( Literal  true_literal)
inline

Definition at line 284 of file sat_base.h.

◆ EnqueueWithUnitReason()

void EnqueueWithUnitReason ( Literal  true_literal)
inline

Definition at line 265 of file sat_base.h.

◆ FailingClause()

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

Definition at line 367 of file sat_base.h.

◆ FailingSatClause()

SatClause* FailingSatClause ( ) const
inline

Definition at line 373 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [1/2]

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

Definition at line 329 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [2/2]

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

Definition at line 320 of file sat_base.h.

◆ Index()

int Index ( ) const
inline

Definition at line 378 of file sat_base.h.

◆ Info()

const AssignmentInfo& Info ( BooleanVariable  var) const
inline

Definition at line 381 of file sat_base.h.

◆ MutableConflict()

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

Definition at line 361 of file sat_base.h.

◆ NumberOfEnqueues()

int64 NumberOfEnqueues ( ) const
inline

Definition at line 377 of file sat_base.h.

◆ NumVariables()

int NumVariables ( ) const
inline

Definition at line 376 of file sat_base.h.

◆ operator[]()

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

Definition at line 379 of file sat_base.h.

◆ Reason()

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

Definition at line 581 of file sat_base.h.

◆ ReferenceVarWithSameReason()

BooleanVariable ReferenceVarWithSameReason ( BooleanVariable  var) const
inline

Definition at line 560 of file sat_base.h.

◆ RegisterPropagator()

void RegisterPropagator ( SatPropagator propagator)
inline

Definition at line 551 of file sat_base.h.

◆ Resize()

void Resize ( int  num_variables)
inline

Definition at line 539 of file sat_base.h.

◆ SetDecisionLevel()

void SetDecisionLevel ( int  level)
inline

Definition at line 354 of file sat_base.h.

◆ SetFailingSatClause()

void SetFailingSatClause ( SatClause clause)
inline

Definition at line 372 of file sat_base.h.

◆ Untrail()

void Untrail ( int  target_trail_index)
inline

Definition at line 343 of file sat_base.h.


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