Google OR-Tools v9.15
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research::sat::Trail Class Reference

Detailed Description

Definition at line 331 of file sat_base.h.

#include <sat_base.h>

Classes

class  EnqueueHelper

Public Types

using ConflictResolutionFunction

Public Member Functions

 Trail ()
 Trail (const Trail &)=delete
Trail & operator= (const Trail &)=delete
void Resize (int num_variables)
void RegisterPropagator (SatPropagator *propagator)
void Enqueue (Literal true_literal, int propagator_id)
void EnqueueAtLevel (Literal true_literal, int propagator_id, int level)
EnqueueHelper GetEnqueueHelper (int propagator_id)
void EnqueueSearchDecision (Literal true_literal)
void EnqueueAssumption (Literal assumptions)
void OverrideDecision (int level, Literal literal)
const std::vector< LiteralWithTrailIndex > & Decisions () const
void EnqueueWithUnitReason (Literal true_literal)
void EnqueueWithUnitReason (ClauseId clause_id, Literal true_literal)
void EnqueueWithSameReasonAs (Literal true_literal, BooleanVariable reference_var)
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason (ClauseId clause_id, Literal true_literal)
absl::Span< const Literal > Reason (BooleanVariable var, int64_t conflict_id=-1) const
int AssignmentType (BooleanVariable var) const
ClauseId GetUnitClauseId (BooleanVariable var) const
ClauseId GetStoredReasonClauseId (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)
int PrepareBacktrack (int level)
void Untrail (int target_trail_index)
int CurrentDecisionLevel () const
std::vector< Literal > * MutableConflict ()
int64_t conflict_timestamp () const
absl::Span< const Literal > FailingClause () const
void SetFailingSatClause (SatClause *clause)
SatClause * FailingSatClause () const
ClauseId FailingClauseId () const
int NumVariables () const
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
int AssignmentLevel (Literal lit) const
std::string DebugString () const
void RegisterDebugChecker (std::function< bool(absl::Span< const Literal > clause)> checker)
bool ChronologicalBacktrackingEnabled () const
void EnableChronologicalBacktracking (bool enable)
void SetConflictResolutionFunction (ConflictResolutionFunction resolution)
ConflictResolutionFunction GetConflictResolutionFunction ()
int NumReimplicationsOnLastUntrail () const

Member Typedef Documentation

◆ ConflictResolutionFunction

using operations_research::sat::Trail::ConflictResolutionFunction
Initial value:
std::function<void(
std::vector<Literal>* conflict,
std::vector<Literal>* reason_used_to_infer_the_conflict,
std::vector<SatClause*>* subsumed_clauses)>

Definition at line 687 of file sat_base.h.

Constructor & Destructor Documentation

◆ Trail() [1/2]

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

Definition at line 333 of file sat_base.h.

◆ Trail() [2/2]

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

Member Function Documentation

◆ Assignment()

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

Definition at line 654 of file sat_base.h.

◆ AssignmentLevel()

int operations_research::sat::Trail::AssignmentLevel ( Literal lit) const
inline

Definition at line 661 of file sat_base.h.

◆ AssignmentType()

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

Definition at line 942 of file sat_base.h.

◆ ChangeReason()

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

Definition at line 576 of file sat_base.h.

◆ ChronologicalBacktrackingEnabled()

bool operations_research::sat::Trail::ChronologicalBacktrackingEnabled ( ) const
inline

Definition at line 678 of file sat_base.h.

◆ conflict_timestamp()

int64_t operations_research::sat::Trail::conflict_timestamp ( ) const
inline

Definition at line 621 of file sat_base.h.

◆ CurrentDecisionLevel()

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

Definition at line 607 of file sat_base.h.

◆ DebugString()

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

Definition at line 664 of file sat_base.h.

◆ Decisions()

const std::vector< LiteralWithTrailIndex > & operations_research::sat::Trail::Decisions ( ) const
inline

Definition at line 451 of file sat_base.h.

◆ EnableChronologicalBacktracking()

void operations_research::sat::Trail::EnableChronologicalBacktracking ( bool enable)
inline

Definition at line 682 of file sat_base.h.

◆ Enqueue()

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

Definition at line 350 of file sat_base.h.

◆ EnqueueAssumption()

void operations_research::sat::Trail::EnqueueAssumption ( Literal assumptions)
inline

Definition at line 433 of file sat_base.h.

◆ EnqueueAtLevel()

void operations_research::sat::Trail::EnqueueAtLevel ( Literal true_literal,
int propagator_id,
int level )
inline

Definition at line 358 of file sat_base.h.

◆ EnqueueSearchDecision()

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

Definition at line 425 of file sat_base.h.

◆ EnqueueWithSameReasonAs()

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

Definition at line 469 of file sat_base.h.

◆ EnqueueWithStoredReason()

ABSL_MUST_USE_RESULT bool operations_research::sat::Trail::EnqueueWithStoredReason ( ClauseId clause_id,
Literal true_literal )
inline

Definition at line 484 of file sat_base.h.

◆ EnqueueWithUnitReason() [1/2]

void operations_research::sat::Trail::EnqueueWithUnitReason ( ClauseId clause_id,
Literal true_literal )
inline

Definition at line 461 of file sat_base.h.

◆ EnqueueWithUnitReason() [2/2]

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

Definition at line 456 of file sat_base.h.

◆ FailingClause()

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

Definition at line 624 of file sat_base.h.

◆ FailingClauseId()

ClauseId operations_research::sat::Trail::FailingClauseId ( ) const
inline

Definition at line 642 of file sat_base.h.

◆ FailingSatClause()

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

Definition at line 638 of file sat_base.h.

◆ GetConflictResolutionFunction()

ConflictResolutionFunction operations_research::sat::Trail::GetConflictResolutionFunction ( )
inline

Definition at line 696 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [1/2]

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

Definition at line 569 of file sat_base.h.

◆ GetEmptyVectorToStoreReason() [2/2]

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

Definition at line 560 of file sat_base.h.

◆ GetEnqueueHelper()

EnqueueHelper operations_research::sat::Trail::GetEnqueueHelper ( int propagator_id)
inline

Definition at line 418 of file sat_base.h.

◆ GetStoredReasonClauseId()

ClauseId operations_research::sat::Trail::GetStoredReasonClauseId ( BooleanVariable var) const
inline

Definition at line 547 of file sat_base.h.

◆ GetUnitClauseId()

ClauseId operations_research::sat::Trail::GetUnitClauseId ( BooleanVariable var) const
inline

Definition at line 537 of file sat_base.h.

◆ Index()

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

Definition at line 647 of file sat_base.h.

◆ Info()

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

Definition at line 655 of file sat_base.h.

◆ IteratorAt()

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

Definition at line 650 of file sat_base.h.

◆ MutableConflict()

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

Definition at line 613 of file sat_base.h.

◆ NumberOfEnqueues()

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

Definition at line 646 of file sat_base.h.

◆ NumReimplicationsOnLastUntrail()

int operations_research::sat::Trail::NumReimplicationsOnLastUntrail ( ) const
inline

Definition at line 700 of file sat_base.h.

◆ NumVariables()

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

Definition at line 645 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 653 of file sat_base.h.

◆ OverrideDecision()

void operations_research::sat::Trail::OverrideDecision ( int level,
Literal literal )
inline

Definition at line 443 of file sat_base.h.

◆ PrepareBacktrack()

int operations_research::sat::Trail::PrepareBacktrack ( int level)
inline

Definition at line 587 of file sat_base.h.

◆ Reason()

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

Definition at line 951 of file sat_base.h.

◆ ReferenceVarWithSameReason()

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

Definition at line 930 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 673 of file sat_base.h.

◆ RegisterPropagator()

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

Definition at line 919 of file sat_base.h.

◆ Resize()

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

Definition at line 902 of file sat_base.h.

◆ SetConflictResolutionFunction()

void operations_research::sat::Trail::SetConflictResolutionFunction ( ConflictResolutionFunction resolution)
inline

Definition at line 692 of file sat_base.h.

◆ SetFailingSatClause()

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

Definition at line 634 of file sat_base.h.

◆ Untrail()

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

Definition at line 595 of file sat_base.h.

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