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

Detailed Description

Definition at line 688 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 FixedValue (IntegerVariable i) const
 
IntegerValue LowerBound (AffineExpression expr) const
 
IntegerValue UpperBound (AffineExpression expr) const
 
bool IsFixed (AffineExpression expr) const
 
IntegerValue FixedValue (AffineExpression expr) const
 
IntegerLiteral LowerBoundAsLiteral (IntegerVariable i) const
 
IntegerLiteral UpperBoundAsLiteral (IntegerVariable i) const
 
IntegerLiteral LowerBoundAsLiteral (AffineExpression expr) const
 
IntegerLiteral UpperBoundAsLiteral (AffineExpression expr) const
 
bool IntegerLiteralIsTrue (IntegerLiteral l) const
 
bool IntegerLiteralIsFalse (IntegerLiteral l) const
 
IntegerValue LevelZeroLowerBound (IntegerVariable var) const
 
IntegerValue LevelZeroUpperBound (IntegerVariable var) const
 
IntegerValue LevelZeroLowerBound (AffineExpression exp) const
 
IntegerValue LevelZeroUpperBound (AffineExpression exp) const
 
bool IsFixedAtLevelZero (IntegerVariable var) const
 
bool IsFixedAtLevelZero (AffineExpression expr) const
 
IntegerValue ConditionalLowerBound (Literal l, IntegerVariable i) const
 
IntegerValue ConditionalLowerBound (Literal l, AffineExpression expr) 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 SafeEnqueue (IntegerLiteral i_lit, 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)
 
ABSL_MUST_USE_RESULT bool RootLevelEnqueue (IntegerLiteral i_lit)
 
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_t num_enqueues () const
 
int64_t timestamp () const
 
int64_t 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
 
void NotifyThatPropagationWasAborted ()
 
IntegerVariable NextVariableToBranchOnInPropagationLoop () const
 
bool CurrentBranchHadAnIncompletePropagation ()
 
IntegerVariable FirstUnassignedVariable () const
 
bool HasPendingRootLevelDeduction () const
 
void RegisterDebugChecker (std::function< bool(absl::Span< const Literal > clause, absl::Span< const IntegerLiteral > integers)> checker)
 
void SetPropagatorId (int id)
 
int PropagatorId () const
 
bool PropagatePreconditionsAreSatisfied (const Trail &trail) const
 
bool PropagationIsDone (const Trail &trail) const
 
virtual bool IsEmpty () 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 951 of file integer.h.

Constructor & Destructor Documentation

◆ IntegerTrail()

IntegerTrail ( Model *  model)
inlineexplicit

Definition at line 690 of file integer.h.

◆ ~IntegerTrail()

~IntegerTrail ( )
final

Definition at line 675 of file integer.cc.

Member Function Documentation

◆ AddIntegerVariable() [1/3]

IntegerVariable AddIntegerVariable ( )
inline

Definition at line 763 of file integer.h.

◆ AddIntegerVariable() [2/3]

IntegerVariable AddIntegerVariable ( const Domain &  domain)

Definition at line 844 of file integer.cc.

◆ AddIntegerVariable() [3/3]

IntegerVariable AddIntegerVariable ( IntegerValue  lower_bound,
IntegerValue  upper_bound 
)

Definition at line 811 of file integer.cc.

◆ AppendNewBounds()

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

Definition at line 2049 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 1006 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 1235 of file integer.cc.

◆ ConditionalLowerBound() [1/2]

IntegerValue ConditionalLowerBound ( Literal  l,
AffineExpression  expr 
) const
inline

Definition at line 1583 of file integer.h.

◆ ConditionalLowerBound() [2/2]

IntegerValue ConditionalLowerBound ( Literal  l,
IntegerVariable  i 
) const
inline

Definition at line 1574 of file integer.h.

◆ CurrentBranchHadAnIncompletePropagation()

bool CurrentBranchHadAnIncompletePropagation ( )

Definition at line 1494 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 1228 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 1279 of file integer.cc.

◆ Enqueue() [3/3]

bool Enqueue ( IntegerLiteral  i_lit,
LazyReasonFunction  lazy_reason 
)

Definition at line 1287 of file integer.cc.

◆ EnqueueLiteral()

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

Definition at line 1387 of file integer.cc.

◆ FindTrailIndexOfVarBefore()

int FindTrailIndexOfVarBefore ( IntegerVariable  var,
int  threshold 
) const

Definition at line 914 of file integer.cc.

◆ FirstUnassignedVariable()

IntegerVariable FirstUnassignedVariable ( ) const

Definition at line 1498 of file integer.cc.

◆ FixedValue() [1/2]

IntegerValue FixedValue ( AffineExpression  expr) const
inline

Definition at line 1614 of file integer.h.

◆ FixedValue() [2/2]

IntegerValue FixedValue ( IntegerVariable  i) const
inline

Definition at line 1569 of file integer.h.

◆ GetOrCreateConstantIntegerVariable()

IntegerVariable GetOrCreateConstantIntegerVariable ( IntegerValue  value)

Definition at line 893 of file integer.cc.

◆ HasPendingRootLevelDeduction()

bool HasPendingRootLevelDeduction ( ) const
inline

Definition at line 1059 of file integer.h.

◆ Index()

int Index ( ) const
inline

Definition at line 1031 of file integer.h.

◆ InitialVariableDomain()

const Domain & InitialVariableDomain ( IntegerVariable  var) const

Definition at line 852 of file integer.cc.

◆ InPropagationLoop()

bool InPropagationLoop ( ) const

Definition at line 1447 of file integer.cc.

◆ IntegerLiteralIsFalse()

bool IntegerLiteralIsFalse ( IntegerLiteral  l) const
inline

Definition at line 1635 of file integer.h.

◆ IntegerLiteralIsTrue()

bool IntegerLiteralIsTrue ( IntegerLiteral  l) const
inline

Definition at line 1631 of file integer.h.

◆ IsCurrentlyIgnored()

bool IsCurrentlyIgnored ( IntegerVariable  i) const
inline

Definition at line 775 of file integer.h.

◆ IsEmpty()

virtual bool IsEmpty ( ) const
inlinevirtualinherited

Reimplemented in PbConstraints, and BinaryImplicationGraph.

Definition at line 538 of file sat_base.h.

◆ IsFixed() [1/2]

bool IsFixed ( AffineExpression  expr) const
inline

Definition at line 1609 of file integer.h.

◆ IsFixed() [2/2]

bool IsFixed ( IntegerVariable  i) const
inline

Definition at line 1565 of file integer.h.

◆ IsFixedAtLevelZero() [1/2]

bool IsFixedAtLevelZero ( AffineExpression  expr) const
inline

Definition at line 1668 of file integer.h.

◆ IsFixedAtLevelZero() [2/2]

bool IsFixedAtLevelZero ( IntegerVariable  var) const
inline

Definition at line 1651 of file integer.h.

◆ IsIgnoredLiteral()

Literal IsIgnoredLiteral ( IntegerVariable  i) const
inline

Definition at line 780 of file integer.h.

◆ IsOptional()

bool IsOptional ( IntegerVariable  i) const
inline

Definition at line 772 of file integer.h.

◆ LevelZeroLowerBound() [1/2]

IntegerValue LevelZeroLowerBound ( AffineExpression  exp) const
inline

Definition at line 1656 of file integer.h.

◆ LevelZeroLowerBound() [2/2]

IntegerValue LevelZeroLowerBound ( IntegerVariable  var) const
inline

Definition at line 1641 of file integer.h.

◆ LevelZeroUpperBound() [1/2]

IntegerValue LevelZeroUpperBound ( AffineExpression  exp) const
inline

Definition at line 1662 of file integer.h.

◆ LevelZeroUpperBound() [2/2]

IntegerValue LevelZeroUpperBound ( IntegerVariable  var) const
inline

Definition at line 1646 of file integer.h.

◆ LowerBound() [1/2]

IntegerValue LowerBound ( AffineExpression  expr) const
inline

Definition at line 1599 of file integer.h.

◆ LowerBound() [2/2]

IntegerValue LowerBound ( IntegerVariable  i) const
inline

Definition at line 1557 of file integer.h.

◆ LowerBoundAsLiteral() [1/2]

IntegerLiteral LowerBoundAsLiteral ( AffineExpression  expr) const
inline

Definition at line 1619 of file integer.h.

◆ LowerBoundAsLiteral() [2/2]

IntegerLiteral LowerBoundAsLiteral ( IntegerVariable  i) const
inline

Definition at line 1589 of file integer.h.

◆ MarkIntegerVariableAsOptional()

void MarkIntegerVariableAsOptional ( IntegerVariable  i,
Literal  is_considered 
)
inline

Definition at line 789 of file integer.h.

◆ MergeReasonInto()

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

Definition at line 1879 of file integer.cc.

◆ NextVariableToBranchOnInPropagationLoop()

IntegerVariable NextVariableToBranchOnInPropagationLoop ( ) const

Definition at line 1465 of file integer.cc.

◆ NotifyThatPropagationWasAborted()

void NotifyThatPropagationWasAborted ( )

Definition at line 1457 of file integer.cc.

◆ num_enqueues()

int64_t num_enqueues ( ) const
inline

Definition at line 988 of file integer.h.

◆ num_level_zero_enqueues()

int64_t num_level_zero_enqueues ( ) const
inline

Definition at line 992 of file integer.h.

◆ NumConstantVariables()

int NumConstantVariables ( ) const

Definition at line 908 of file integer.cc.

◆ NumIntegerVariables()

IntegerVariable NumIntegerVariables ( ) const
inline

Definition at line 715 of file integer.h.

◆ OptionalLiteralIndex()

LiteralIndex OptionalLiteralIndex ( IntegerVariable  i) const
inline

Definition at line 784 of file integer.h.

◆ Propagate()

bool Propagate ( Trail *  trail)
finalvirtual

Implements SatPropagator.

Definition at line 682 of file integer.cc.

◆ PropagatePreconditionsAreSatisfied()

bool PropagatePreconditionsAreSatisfied ( const Trail &  trail) const
inlineinherited

Definition at line 553 of file sat_base.h.

◆ PropagationIsDone()

bool PropagationIsDone ( const Trail &  trail) const
inlineinherited

Definition at line 530 of file sat_base.h.

◆ PropagatorId()

int PropagatorId ( ) const
inlineinherited

Definition at line 483 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 2029 of file integer.cc.

◆ ReasonFor()

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

Definition at line 1873 of file integer.cc.

◆ RegisterDebugChecker()

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

Definition at line 1066 of file integer.h.

◆ RegisterReversibleClass()

void RegisterReversibleClass ( ReversibleInterface *  rev)
inline

Definition at line 1027 of file integer.h.

◆ RegisterWatcher()

void RegisterWatcher ( SparseBitset< IntegerVariable > *  p)
inline

Definition at line 997 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 1021 of file integer.cc.

◆ RelaxLinearReason() [2/2]

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

Definition at line 984 of file integer.cc.

◆ RemoveLevelZeroBounds()

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

Definition at line 1118 of file integer.cc.

◆ ReportConflict() [1/2]

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

Definition at line 1012 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 1004 of file integer.h.

◆ ReserveSpaceForNumVariables()

void ReserveSpaceForNumVariables ( int  num_vars)

Definition at line 797 of file integer.cc.

◆ RootLevelEnqueue()

bool RootLevelEnqueue ( IntegerLiteral  i_lit)

Definition at line 1188 of file integer.cc.

◆ SafeEnqueue()

bool SafeEnqueue ( IntegerLiteral  i_lit,
absl::Span< const IntegerLiteral >  integer_reason 
)

Definition at line 1211 of file integer.cc.

◆ SetPropagatorId()

void SetPropagatorId ( int  id)
inlineinherited

Definition at line 482 of file sat_base.h.

◆ timestamp()

int64_t timestamp ( ) const
inline

Definition at line 989 of file integer.h.

◆ Untrail()

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

Reimplemented from SatPropagator.

Definition at line 748 of file integer.cc.

◆ UpdateInitialDomain()

bool UpdateInitialDomain ( IntegerVariable  var,
Domain  domain 
)

Definition at line 862 of file integer.cc.

◆ UpperBound() [1/2]

IntegerValue UpperBound ( AffineExpression  expr) const
inline

Definition at line 1604 of file integer.h.

◆ UpperBound() [2/2]

IntegerValue UpperBound ( IntegerVariable  i) const
inline

Definition at line 1561 of file integer.h.

◆ UpperBoundAsLiteral() [1/2]

IntegerLiteral UpperBoundAsLiteral ( AffineExpression  expr) const
inline

Definition at line 1625 of file integer.h.

◆ UpperBoundAsLiteral() [2/2]

IntegerLiteral UpperBoundAsLiteral ( IntegerVariable  i) const
inline

Definition at line 1594 of file integer.h.

◆ VariableLowerBoundIsFromLevelZero()

bool VariableLowerBoundIsFromLevelZero ( IntegerVariable  var) const
inline

Definition at line 1021 of file integer.h.

Member Data Documentation

◆ name_

const std::string name_
protectedinherited

Definition at line 541 of file sat_base.h.

◆ propagation_trail_index_

int propagation_trail_index_
protectedinherited

Definition at line 543 of file sat_base.h.

◆ propagator_id_

int propagator_id_
protectedinherited

Definition at line 542 of file sat_base.h.

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