OR-Tools  8.2
Classes | Public Types | Public Member Functions | Protected Attributes | List of all members
IntegerTrail

Detailed Description

Definition at line 540 of file integer.h.

Public Types

using LazyReasonFunction = std::function< void(IntegerLiteral literal_to_explain, int trail_index_of_literal, std::vector< Literal > *literals, std::vector< int > *dependencies)>
 

Public Member Functions

 IntegerTrail (Model *model)
 
 ~IntegerTrail () final
 
bool Propagate (Trail *trail) final
 
void Untrail (const Trail &trail, int literal_trail_index) final
 
absl::Span< const Literal > Reason (const Trail &trail, int trail_index) const final
 
IntegerVariable NumIntegerVariables () const
 
void ReserveSpaceForNumVariables (int num_vars)
 
IntegerVariable AddIntegerVariable (IntegerValue lower_bound, IntegerValue upper_bound)
 
IntegerVariable AddIntegerVariable (const Domain &domain)
 
const Domain & InitialVariableDomain (IntegerVariable var) const
 
bool UpdateInitialDomain (IntegerVariable var, Domain domain)
 
IntegerVariable GetOrCreateConstantIntegerVariable (IntegerValue value)
 
int NumConstantVariables () const
 
IntegerVariable AddIntegerVariable ()
 
bool IsOptional (IntegerVariable i) const
 
bool IsCurrentlyIgnored (IntegerVariable i) const
 
Literal IsIgnoredLiteral (IntegerVariable i) const
 
LiteralIndex OptionalLiteralIndex (IntegerVariable i) const
 
void MarkIntegerVariableAsOptional (IntegerVariable i, Literal is_considered)
 
IntegerValue LowerBound (IntegerVariable i) const
 
IntegerValue UpperBound (IntegerVariable i) const
 
bool IsFixed (IntegerVariable i) const
 
IntegerValue LowerBound (AffineExpression expr) const
 
IntegerValue UpperBound (AffineExpression expr) const
 
bool IsFixed (AffineExpression expr) const
 
IntegerLiteral LowerBoundAsLiteral (IntegerVariable i) const
 
IntegerLiteral UpperBoundAsLiteral (IntegerVariable i) const
 
bool IntegerLiteralIsTrue (IntegerLiteral l) const
 
bool IntegerLiteralIsFalse (IntegerLiteral l) const
 
IntegerValue LevelZeroLowerBound (IntegerVariable var) const
 
IntegerValue LevelZeroUpperBound (IntegerVariable var) const
 
bool IsFixedAtLevelZero (IntegerVariable var) const
 
void RelaxLinearReason (IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
 
void AppendRelaxedLinearReason (IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
 
void RelaxLinearReason (IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< int > *trail_indices) const
 
void RemoveLevelZeroBounds (std::vector< IntegerLiteral > *reason) const
 
ABSL_MUST_USE_RESULT bool Enqueue (IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
 
ABSL_MUST_USE_RESULT bool ConditionalEnqueue (Literal lit, IntegerLiteral i_lit, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason)
 
ABSL_MUST_USE_RESULT bool Enqueue (IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason, int trail_index_with_same_reason)
 
ABSL_MUST_USE_RESULT bool Enqueue (IntegerLiteral i_lit, LazyReasonFunction lazy_reason)
 
void EnqueueLiteral (Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
 
std::vector< Literal > ReasonFor (IntegerLiteral literal) const
 
void MergeReasonInto (absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const
 
int64 num_enqueues () const
 
int64 timestamp () const
 
int64 num_level_zero_enqueues () const
 
void RegisterWatcher (SparseBitset< IntegerVariable > *p)
 
bool ReportConflict (absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
 
bool ReportConflict (absl::Span< const IntegerLiteral > integer_reason)
 
bool VariableLowerBoundIsFromLevelZero (IntegerVariable var) const
 
void RegisterReversibleClass (ReversibleInterface *rev)
 
int Index () const
 
void AppendNewBounds (std::vector< IntegerLiteral > *output) const
 
int FindTrailIndexOfVarBefore (IntegerVariable var, int threshold) const
 
bool InPropagationLoop () const
 
IntegerVariable NextVariableToBranchOnInPropagationLoop () const
 
bool CurrentBranchHadAnIncompletePropagation ()
 
IntegerVariable FirstUnassignedVariable () const
 
bool HasPendingRootLevelDeduction () const
 
void SetPropagatorId (int id)
 
int PropagatorId () const
 
bool PropagatePreconditionsAreSatisfied (const Trail &trail) const
 
bool PropagationIsDone (const Trail &trail) const
 

Protected Attributes

const std::string name_
 
int propagator_id_
 
int propagation_trail_index_
 

Member Typedef Documentation

◆ LazyReasonFunction

using LazyReasonFunction = std::function<void( IntegerLiteral literal_to_explain, int trail_index_of_literal, std::vector<Literal>* literals, std::vector<int>* dependencies)>

Definition at line 767 of file integer.h.

Constructor & Destructor Documentation

◆ IntegerTrail()

IntegerTrail ( Model *  model)
inlineexplicit

Definition at line 542 of file integer.h.

◆ ~IntegerTrail()

~IntegerTrail ( )
final

Definition at line 473 of file integer.cc.

Member Function Documentation

◆ AddIntegerVariable() [1/3]

IntegerVariable AddIntegerVariable ( )
inline

Definition at line 613 of file integer.h.

◆ AddIntegerVariable() [2/3]

IntegerVariable AddIntegerVariable ( const Domain &  domain)

Definition at line 636 of file integer.cc.

◆ AddIntegerVariable() [3/3]

IntegerVariable AddIntegerVariable ( IntegerValue  lower_bound,
IntegerValue  upper_bound 
)

Definition at line 603 of file integer.cc.

◆ AppendNewBounds()

void AppendNewBounds ( std::vector< IntegerLiteral > *  output) const

Definition at line 1728 of file integer.cc.

◆ AppendRelaxedLinearReason()

void AppendRelaxedLinearReason ( IntegerValue  slack,
absl::Span< const IntegerValue >  coeffs,
absl::Span< const IntegerVariable >  vars,
std::vector< IntegerLiteral > *  reason 
) const

Definition at line 807 of file integer.cc.

◆ ConditionalEnqueue()

bool ConditionalEnqueue ( Literal  lit,
IntegerLiteral  i_lit,
std::vector< Literal > *  literal_reason,
std::vector< IntegerLiteral > *  integer_reason 
)

Definition at line 996 of file integer.cc.

◆ CurrentBranchHadAnIncompletePropagation()

bool CurrentBranchHadAnIncompletePropagation ( )

Definition at line 1186 of file integer.cc.

◆ Enqueue() [1/3]

bool Enqueue ( IntegerLiteral  i_lit,
absl::Span< const Literal >  literal_reason,
absl::Span< const IntegerLiteral >  integer_reason 
)

Definition at line 989 of file integer.cc.

◆ Enqueue() [2/3]

bool Enqueue ( IntegerLiteral  i_lit,
absl::Span< const Literal >  literal_reason,
absl::Span< const IntegerLiteral >  integer_reason,
int  trail_index_with_same_reason 
)

Definition at line 1025 of file integer.cc.

◆ Enqueue() [3/3]

bool Enqueue ( IntegerLiteral  i_lit,
LazyReasonFunction  lazy_reason 
)

Definition at line 1033 of file integer.cc.

◆ EnqueueLiteral()

void EnqueueLiteral ( Literal  literal,
absl::Span< const Literal >  literal_reason,
absl::Span< const IntegerLiteral >  integer_reason 
)

Definition at line 1087 of file integer.cc.

◆ FindTrailIndexOfVarBefore()

int FindTrailIndexOfVarBefore ( IntegerVariable  var,
int  threshold 
) const

Definition at line 716 of file integer.cc.

◆ FirstUnassignedVariable()

IntegerVariable FirstUnassignedVariable ( ) const

Definition at line 1190 of file integer.cc.

◆ GetOrCreateConstantIntegerVariable()

IntegerVariable GetOrCreateConstantIntegerVariable ( IntegerValue  value)

Definition at line 695 of file integer.cc.

◆ HasPendingRootLevelDeduction()

bool HasPendingRootLevelDeduction ( ) const
inline

Definition at line 864 of file integer.h.

◆ Index()

int Index ( ) const
inline

Definition at line 837 of file integer.h.

◆ InitialVariableDomain()

const Domain & InitialVariableDomain ( IntegerVariable  var) const

Definition at line 644 of file integer.cc.

◆ InPropagationLoop()

bool InPropagationLoop ( ) const

Definition at line 1147 of file integer.cc.

◆ IntegerLiteralIsFalse()

bool IntegerLiteralIsFalse ( IntegerLiteral  l) const
inline

Definition at line 1344 of file integer.h.

◆ IntegerLiteralIsTrue()

bool IntegerLiteralIsTrue ( IntegerLiteral  l) const
inline

Definition at line 1340 of file integer.h.

◆ IsCurrentlyIgnored()

bool IsCurrentlyIgnored ( IntegerVariable  i) const
inline

Definition at line 625 of file integer.h.

◆ IsFixed() [1/2]

bool IsFixed ( AffineExpression  expr) const
inline

Definition at line 1325 of file integer.h.

◆ IsFixed() [2/2]

bool IsFixed ( IntegerVariable  i) const
inline

Definition at line 1308 of file integer.h.

◆ IsFixedAtLevelZero()

bool IsFixedAtLevelZero ( IntegerVariable  var) const
inline

Definition at line 1360 of file integer.h.

◆ IsIgnoredLiteral()

Literal IsIgnoredLiteral ( IntegerVariable  i) const
inline

Definition at line 630 of file integer.h.

◆ IsOptional()

bool IsOptional ( IntegerVariable  i) const
inline

Definition at line 622 of file integer.h.

◆ LevelZeroLowerBound()

IntegerValue LevelZeroLowerBound ( IntegerVariable  var) const
inline

Definition at line 1350 of file integer.h.

◆ LevelZeroUpperBound()

IntegerValue LevelZeroUpperBound ( IntegerVariable  var) const
inline

Definition at line 1355 of file integer.h.

◆ LowerBound() [1/2]

IntegerValue LowerBound ( AffineExpression  expr) const
inline

Definition at line 1314 of file integer.h.

◆ LowerBound() [2/2]

IntegerValue LowerBound ( IntegerVariable  i) const
inline

Definition at line 1300 of file integer.h.

◆ LowerBoundAsLiteral()

IntegerLiteral LowerBoundAsLiteral ( IntegerVariable  i) const
inline

Definition at line 1330 of file integer.h.

◆ MarkIntegerVariableAsOptional()

void MarkIntegerVariableAsOptional ( IntegerVariable  i,
Literal  is_considered 
)
inline

Definition at line 639 of file integer.h.

◆ MergeReasonInto()

void MergeReasonInto ( absl::Span< const IntegerLiteral >  literals,
std::vector< Literal > *  output 
) const

Definition at line 1570 of file integer.cc.

◆ NextVariableToBranchOnInPropagationLoop()

IntegerVariable NextVariableToBranchOnInPropagationLoop ( ) const

Definition at line 1157 of file integer.cc.

◆ num_enqueues()

int64 num_enqueues ( ) const
inline

Definition at line 794 of file integer.h.

◆ num_level_zero_enqueues()

int64 num_level_zero_enqueues ( ) const
inline

Definition at line 798 of file integer.h.

◆ NumConstantVariables()

int NumConstantVariables ( ) const

Definition at line 710 of file integer.cc.

◆ NumIntegerVariables()

IntegerVariable NumIntegerVariables ( ) const
inline

Definition at line 565 of file integer.h.

◆ OptionalLiteralIndex()

LiteralIndex OptionalLiteralIndex ( IntegerVariable  i) const
inline

Definition at line 634 of file integer.h.

◆ Propagate()

bool Propagate ( Trail *  trail)
finalvirtual

Implements SatPropagator.

Definition at line 480 of file integer.cc.

◆ PropagatePreconditionsAreSatisfied()

bool PropagatePreconditionsAreSatisfied ( const Trail &  trail) const
inlineinherited

Definition at line 517 of file sat_base.h.

◆ PropagationIsDone()

bool PropagationIsDone ( const Trail &  trail) const
inlineinherited

Definition at line 500 of file sat_base.h.

◆ PropagatorId()

int PropagatorId ( ) const
inlineinherited

Definition at line 453 of file sat_base.h.

◆ Reason()

absl::Span< const Literal > Reason ( const Trail &  trail,
int  trail_index 
) const
finalvirtual

Reimplemented from SatPropagator.

Definition at line 1708 of file integer.cc.

◆ ReasonFor()

std::vector< Literal > ReasonFor ( IntegerLiteral  literal) const

Definition at line 1562 of file integer.cc.

◆ RegisterReversibleClass()

void RegisterReversibleClass ( ReversibleInterface *  rev)
inline

Definition at line 833 of file integer.h.

◆ RegisterWatcher()

void RegisterWatcher ( SparseBitset< IntegerVariable > *  p)
inline

Definition at line 803 of file integer.h.

◆ RelaxLinearReason() [1/2]

void RelaxLinearReason ( IntegerValue  slack,
absl::Span< const IntegerValue >  coeffs,
std::vector< int > *  trail_indices 
) const

Definition at line 822 of file integer.cc.

◆ RelaxLinearReason() [2/2]

void RelaxLinearReason ( IntegerValue  slack,
absl::Span< const IntegerValue >  coeffs,
std::vector< IntegerLiteral > *  reason 
) const

Definition at line 785 of file integer.cc.

◆ RemoveLevelZeroBounds()

void RemoveLevelZeroBounds ( std::vector< IntegerLiteral > *  reason) const

Definition at line 919 of file integer.cc.

◆ ReportConflict() [1/2]

bool ReportConflict ( absl::Span< const IntegerLiteral >  integer_reason)
inline

Definition at line 818 of file integer.h.

◆ ReportConflict() [2/2]

bool ReportConflict ( absl::Span< const Literal >  literal_reason,
absl::Span< const IntegerLiteral >  integer_reason 
)
inline

Definition at line 810 of file integer.h.

◆ ReserveSpaceForNumVariables()

void ReserveSpaceForNumVariables ( int  num_vars)

Definition at line 592 of file integer.cc.

◆ SetPropagatorId()

void SetPropagatorId ( int  id)
inlineinherited

Definition at line 452 of file sat_base.h.

◆ timestamp()

int64 timestamp ( ) const
inline

Definition at line 795 of file integer.h.

◆ Untrail()

void Untrail ( const Trail &  trail,
int  literal_trail_index 
)
finalvirtual

Reimplemented from SatPropagator.

Definition at line 543 of file integer.cc.

◆ UpdateInitialDomain()

bool UpdateInitialDomain ( IntegerVariable  var,
Domain  domain 
)

Definition at line 648 of file integer.cc.

◆ UpperBound() [1/2]

IntegerValue UpperBound ( AffineExpression  expr) const
inline

Definition at line 1320 of file integer.h.

◆ UpperBound() [2/2]

IntegerValue UpperBound ( IntegerVariable  i) const
inline

Definition at line 1304 of file integer.h.

◆ UpperBoundAsLiteral()

IntegerLiteral UpperBoundAsLiteral ( IntegerVariable  i) const
inline

Definition at line 1335 of file integer.h.

◆ VariableLowerBoundIsFromLevelZero()

bool VariableLowerBoundIsFromLevelZero ( IntegerVariable  var) const
inline

Definition at line 827 of file integer.h.

Member Data Documentation

◆ name_

const std::string name_
protectedinherited

Definition at line 505 of file sat_base.h.

◆ propagation_trail_index_

int propagation_trail_index_
protectedinherited

Definition at line 507 of file sat_base.h.

◆ propagator_id_

int propagator_id_
protectedinherited

Definition at line 506 of file sat_base.h.

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