operations_research::sat::IntegerTrail Class Reference

Detailed Description

Definition at line 523 of file integer.h.

#include <integer.h>

Inheritance diagram for operations_research::sat::IntegerTrail:

Public Member Functions
	IntegerTrail (Model *model)
	IntegerTrail (const IntegerTrail &)=delete
IntegerTrail &	operator= (const IntegerTrail &)=delete
	~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, int64_t conflict_id) const final
const IntegerReason &	IntegerConflict ()
const IntegerReason &	GetIntegerReason (GlobalTrailIndex index, std::optional< IntegerValue > needed_bound)
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 ()
IntegerValue	LowerBound (IntegerVariable i) const
IntegerValue	UpperBound (IntegerVariable i) const
const IntegerValue *	LowerBoundsData () const
bool	IsFixed (IntegerVariable i) const
IntegerValue	FixedValue (IntegerVariable i) const
IntegerValue	LowerBound (AffineExpression expr) const
IntegerValue	UpperBound (AffineExpression expr) const
IntegerValue	UpperBound (LinearExpression2 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
bool	IsTrueAtLevelZero (IntegerLiteral l) const
IntegerValue	LevelZeroLowerBound (IntegerVariable var) const
IntegerValue	LevelZeroUpperBound (IntegerVariable var) const
IntegerValue	LevelZeroLowerBound (AffineExpression exp) const
IntegerValue	LevelZeroUpperBound (AffineExpression exp) const
IntegerValue	LevelZeroLowerBound (LinearExpression2 expr) const
IntegerValue	LevelZeroUpperBound (LinearExpression2 expr) 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
IntegerValue	ConditionalUpperBound (Literal l, IntegerVariable i) const
IntegerValue	ConditionalUpperBound (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_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	SafeEnqueue (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	EnqueueWithLazyReason (IntegerLiteral i_lit, int id, IntegerValue propagation_slack, LazyReasonInterface *explainer)
std::vector< Literal > &	ClearedMutableTmpLiterals ()
std::vector< IntegerLiteral > &	ClearedMutableTmpIntegerLiterals ()
ABSL_MUST_USE_RESULT bool	RootLevelEnqueue (IntegerLiteral i_lit)
ABSL_MUST_USE_RESULT bool	EnqueueLiteral (Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
ABSL_MUST_USE_RESULT bool	SafeEnqueueLiteral (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)
IntegerVariable	VarAtIndex (int integer_trail_index) const
IntegerLiteral	IntegerLiteralAtIndex (int integer_trail_index) const
int	GetFirstIndexBefore (IntegerVariable var, GlobalTrailIndex source_index, int starting_integer_index)
int	PreviousTrailIndex (int integer_trail_index) const
GlobalTrailIndex	GlobalIndexAt (int integer_index) const
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
void	AppendNewBoundsFrom (int base_index, 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	UseNewConflictResolution ()
ReasonIndex	AppendReasonToInternalBuffers (absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
absl::Span< const IntegerLiteral >	IntegerReasonAsSpan (ReasonIndex index) const
absl::Span< const Literal >	LiteralReasonAsSpan (ReasonIndex index) const
Public Member Functions inherited from operations_research::sat::SatPropagator
	SatPropagator (const std::string &name)
	SatPropagator (const SatPropagator &)=delete
SatPropagator &	operator= (const SatPropagator &)=delete
virtual	~SatPropagator ()=default
void	SetPropagatorId (int id)
int	PropagatorId () const
virtual void	Reimply (Trail *, int)
bool	PropagatePreconditionsAreSatisfied (const Trail &trail) const
bool	PropagationIsDone (const Trail &trail) const
const std::string &	name () const
virtual bool	IsEmpty () const

Additional Inherited Members
Protected Attributes inherited from operations_research::sat::SatPropagator
const std::string	name_
int	propagator_id_
int	propagation_trail_index_

Constructor & Destructor Documentation

IntegerTrail() [1/2]

operations_research::sat::IntegerTrail::IntegerTrail ( Model * model )

inlineexplicit

Definition at line 525 of file integer.h.

IntegerTrail() [2/2]

operations_research::sat::IntegerTrail::IntegerTrail ( const IntegerTrail & )

delete

~IntegerTrail()

operations_research::sat::IntegerTrail::~IntegerTrail ( )

final

Definition at line 716 of file integer.cc.

Member Function Documentation

AddIntegerVariable() [1/3]

IntegerVariable operations_research::sat::IntegerTrail::AddIntegerVariable ( )

inline

Definition at line 621 of file integer.h.

AddIntegerVariable() [2/3]

IntegerVariable operations_research::sat::IntegerTrail::AddIntegerVariable

(

const Domain &

domain

)

Definition at line 887 of file integer.cc.

AddIntegerVariable() [3/3]

IntegerVariable operations_research::sat::IntegerTrail::AddIntegerVariable	(	IntegerValue	lower_bound,
		IntegerValue	upper_bound )

Definition at line 856 of file integer.cc.

AppendNewBounds()

void operations_research::sat::IntegerTrail::AppendNewBounds

(

std::vector< IntegerLiteral > *

output

)

const

Definition at line 2406 of file integer.cc.

AppendNewBoundsFrom()

void operations_research::sat::IntegerTrail::AppendNewBoundsFrom	(	int	base_index,
		std::vector< IntegerLiteral > *	output ) const

Definition at line 2412 of file integer.cc.

AppendReasonToInternalBuffers()

ReasonIndex operations_research::sat::IntegerTrail::AppendReasonToInternalBuffers	(	absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

Definition at line 1646 of file integer.cc.

AppendRelaxedLinearReason()

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

Definition at line 1068 of file integer.cc.

ClearedMutableTmpIntegerLiterals()

std::vector< IntegerLiteral > & operations_research::sat::IntegerTrail::ClearedMutableTmpIntegerLiterals ( )

inline

Definition at line 810 of file integer.h.

ClearedMutableTmpLiterals()

std::vector< Literal > & operations_research::sat::IntegerTrail::ClearedMutableTmpLiterals ( )

inline

Definition at line 806 of file integer.h.

ConditionalEnqueue()

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

Definition at line 1361 of file integer.cc.

ConditionalLowerBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalLowerBound ( Literal l, AffineExpression expr ) const

inline

Definition at line 1563 of file integer.h.

ConditionalLowerBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalLowerBound ( Literal l, IntegerVariable i ) const

inline

Definition at line 1554 of file integer.h.

ConditionalUpperBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalUpperBound ( Literal l, AffineExpression expr ) const

inline

Definition at line 1574 of file integer.h.

ConditionalUpperBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalUpperBound ( Literal l, IntegerVariable i ) const

inline

Definition at line 1569 of file integer.h.

CurrentBranchHadAnIncompletePropagation()

bool operations_research::sat::IntegerTrail::CurrentBranchHadAnIncompletePropagation

(

)

Definition at line 1624 of file integer.cc.

Enqueue() [1/3]

ABSL_MUST_USE_RESULT bool operations_research::sat::IntegerTrail::Enqueue ( IntegerLiteral i_lit )

inline

Definition at line 745 of file integer.h.

Enqueue() [2/3]

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

inline

Definition at line 748 of file integer.h.

Enqueue() [3/3]

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

inline

Definition at line 786 of file integer.h.

EnqueueLiteral()

bool operations_research::sat::IntegerTrail::EnqueueLiteral	(	Literal	literal,
		absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

Definition at line 1498 of file integer.cc.

EnqueueWithLazyReason()

ABSL_MUST_USE_RESULT bool operations_research::sat::IntegerTrail::EnqueueWithLazyReason ( IntegerLiteral i_lit, int id, IntegerValue propagation_slack, LazyReasonInterface * explainer )

inline

Definition at line 795 of file integer.h.

FindTrailIndexOfVarBefore()

int operations_research::sat::IntegerTrail::FindTrailIndexOfVarBefore	(	IntegerVariable	var,
		int	threshold ) const

Definition at line 965 of file integer.cc.

FirstUnassignedVariable()

IntegerVariable operations_research::sat::IntegerTrail::FirstUnassignedVariable

(

)

const

Definition at line 1628 of file integer.cc.

FixedValue() [1/2]

IntegerValue operations_research::sat::IntegerTrail::FixedValue ( AffineExpression expr ) const

inline

Definition at line 1619 of file integer.h.

FixedValue() [2/2]

IntegerValue operations_research::sat::IntegerTrail::FixedValue ( IntegerVariable i ) const

inline

Definition at line 1549 of file integer.h.

GetFirstIndexBefore()

int operations_research::sat::IntegerTrail::GetFirstIndexBefore ( IntegerVariable var, GlobalTrailIndex source_index, int starting_integer_index )

inline

Definition at line 873 of file integer.h.

GetIntegerReason()

const IntegerReason & operations_research::sat::IntegerTrail::GetIntegerReason	(	GlobalTrailIndex	index,
		std::optional< IntegerValue >	needed_bound )

Definition at line 2367 of file integer.cc.

GetOrCreateConstantIntegerVariable()

IntegerVariable operations_research::sat::IntegerTrail::GetOrCreateConstantIntegerVariable

(

IntegerValue

value

)

Definition at line 944 of file integer.cc.

GlobalIndexAt()

GlobalTrailIndex operations_research::sat::IntegerTrail::GlobalIndexAt ( int integer_index ) const

inline

Definition at line 893 of file integer.h.

HasPendingRootLevelDeduction()

bool operations_research::sat::IntegerTrail::HasPendingRootLevelDeduction ( ) const

inline

Definition at line 975 of file integer.h.

Index()

int operations_research::sat::IntegerTrail::Index ( ) const

inline

Definition at line 941 of file integer.h.

InitialVariableDomain()

const Domain & operations_research::sat::IntegerTrail::InitialVariableDomain

(

IntegerVariable

var

)

const

Definition at line 895 of file integer.cc.

InPropagationLoop()

bool operations_research::sat::IntegerTrail::InPropagationLoop

(

)

const

Definition at line 1577 of file integer.cc.

IntegerConflict()

const IntegerReason & operations_research::sat::IntegerTrail::IntegerConflict ( )

inline

Definition at line 553 of file integer.h.

IntegerLiteralAtIndex()

IntegerLiteral operations_research::sat::IntegerTrail::IntegerLiteralAtIndex ( int integer_trail_index ) const

inline

Definition at line 868 of file integer.h.

IntegerLiteralIsFalse()

bool operations_research::sat::IntegerTrail::IntegerLiteralIsFalse ( IntegerLiteral l ) const

inline

Definition at line 1640 of file integer.h.

IntegerLiteralIsTrue()

bool operations_research::sat::IntegerTrail::IntegerLiteralIsTrue ( IntegerLiteral l ) const

inline

Definition at line 1636 of file integer.h.

IntegerReasonAsSpan()

absl::Span< const IntegerLiteral > operations_research::sat::IntegerTrail::IntegerReasonAsSpan

(

ReasonIndex

index

)

const

Definition at line 2028 of file integer.cc.

IsFixed() [1/2]

bool operations_research::sat::IntegerTrail::IsFixed ( AffineExpression expr ) const

inline

Definition at line 1614 of file integer.h.

IsFixed() [2/2]

bool operations_research::sat::IntegerTrail::IsFixed ( IntegerVariable i ) const

inline

Definition at line 1545 of file integer.h.

IsFixedAtLevelZero() [1/2]

bool operations_research::sat::IntegerTrail::IsFixedAtLevelZero ( AffineExpression expr ) const

inline

Definition at line 1703 of file integer.h.

IsFixedAtLevelZero() [2/2]

bool operations_research::sat::IntegerTrail::IsFixedAtLevelZero ( IntegerVariable var ) const

inline

Definition at line 1662 of file integer.h.

IsTrueAtLevelZero()

bool operations_research::sat::IntegerTrail::IsTrueAtLevelZero ( IntegerLiteral l ) const

inline

Definition at line 1644 of file integer.h.

LevelZeroLowerBound() [1/3]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroLowerBound ( AffineExpression exp ) const

inline

Definition at line 1667 of file integer.h.

LevelZeroLowerBound() [2/3]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroLowerBound ( IntegerVariable var ) const

inline

Definition at line 1650 of file integer.h.

LevelZeroLowerBound() [3/3]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroLowerBound ( LinearExpression2 expr ) const

inline

Definition at line 1679 of file integer.h.

LevelZeroUpperBound() [1/3]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroUpperBound ( AffineExpression exp ) const

inline

Definition at line 1673 of file integer.h.

LevelZeroUpperBound() [2/3]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroUpperBound ( IntegerVariable var ) const

inline

Definition at line 1657 of file integer.h.

LevelZeroUpperBound() [3/3]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroUpperBound ( LinearExpression2 expr ) const

inline

Definition at line 1691 of file integer.h.

LiteralReasonAsSpan()

absl::Span< const Literal > operations_research::sat::IntegerTrail::LiteralReasonAsSpan

(

ReasonIndex

index

)

const

Definition at line 2073 of file integer.cc.

LowerBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::LowerBound ( AffineExpression expr ) const

inline

Definition at line 1590 of file integer.h.

LowerBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::LowerBound ( IntegerVariable i ) const

inline

Definition at line 1537 of file integer.h.

LowerBoundAsLiteral() [1/2]

IntegerLiteral operations_research::sat::IntegerTrail::LowerBoundAsLiteral ( AffineExpression expr ) const

inline

Definition at line 1624 of file integer.h.

LowerBoundAsLiteral() [2/2]

IntegerLiteral operations_research::sat::IntegerTrail::LowerBoundAsLiteral ( IntegerVariable i ) const

inline

Definition at line 1580 of file integer.h.

LowerBoundsData()

const IntegerValue * operations_research::sat::IntegerTrail::LowerBoundsData ( ) const

inline

Definition at line 631 of file integer.h.

MergeReasonInto()

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

Definition at line 2102 of file integer.cc.

NextVariableToBranchOnInPropagationLoop()

IntegerVariable operations_research::sat::IntegerTrail::NextVariableToBranchOnInPropagationLoop

(

)

const

Definition at line 1595 of file integer.cc.

NotifyThatPropagationWasAborted()

void operations_research::sat::IntegerTrail::NotifyThatPropagationWasAborted

(

)

Definition at line 1587 of file integer.cc.

num_enqueues()

int64_t operations_research::sat::IntegerTrail::num_enqueues ( ) const

inline

Definition at line 851 of file integer.h.

num_level_zero_enqueues()

int64_t operations_research::sat::IntegerTrail::num_level_zero_enqueues ( ) const

inline

Definition at line 855 of file integer.h.

NumConstantVariables()

int operations_research::sat::IntegerTrail::NumConstantVariables

(

)

const

Definition at line 959 of file integer.cc.

NumIntegerVariables()

IntegerVariable operations_research::sat::IntegerTrail::NumIntegerVariables ( ) const

inline

Definition at line 573 of file integer.h.

operator=()

IntegerTrail & operations_research::sat::IntegerTrail::operator= ( const IntegerTrail & )

delete

PreviousTrailIndex()

int operations_research::sat::IntegerTrail::PreviousTrailIndex ( int integer_trail_index ) const

inline

Definition at line 887 of file integer.h.

Propagate()

bool operations_research::sat::IntegerTrail::Propagate ( Trail * trail )

finalvirtual

Implements operations_research::sat::SatPropagator.

Definition at line 723 of file integer.cc.

Reason()

absl::Span< const Literal > operations_research::sat::IntegerTrail::Reason ( const Trail & trail, int trail_index, int64_t conflict_id ) const

finalvirtual

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 2328 of file integer.cc.

ReasonFor()

std::vector< Literal > operations_research::sat::IntegerTrail::ReasonFor

(

IntegerLiteral

literal

)

const

Definition at line 2096 of file integer.cc.

RegisterDebugChecker()

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

inline

Definition at line 982 of file integer.h.

RegisterReversibleClass()

void operations_research::sat::IntegerTrail::RegisterReversibleClass ( ReversibleInterface * rev )

inline

Definition at line 937 of file integer.h.

RegisterWatcher()

void operations_research::sat::IntegerTrail::RegisterWatcher ( SparseBitset< IntegerVariable > * p )

inline

Definition at line 860 of file integer.h.

RelaxLinearReason() [1/2]

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

Definition at line 1083 of file integer.cc.

RelaxLinearReason() [2/2]

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

Definition at line 1046 of file integer.cc.

RemoveLevelZeroBounds()

void operations_research::sat::IntegerTrail::RemoveLevelZeroBounds

(

std::vector< IntegerLiteral > *

reason

)

const

Definition at line 1180 of file integer.cc.

ReportConflict() [1/2]

bool operations_research::sat::IntegerTrail::ReportConflict ( absl::Span< const IntegerLiteral > integer_reason )

inline

Definition at line 926 of file integer.h.

ReportConflict() [2/2]

bool operations_research::sat::IntegerTrail::ReportConflict ( absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason )

inline

Definition at line 905 of file integer.h.

ReserveSpaceForNumVariables()

void operations_research::sat::IntegerTrail::ReserveSpaceForNumVariables

(

int

num_vars

)

Definition at line 840 of file integer.cc.

RootLevelEnqueue()

bool operations_research::sat::IntegerTrail::RootLevelEnqueue

(

IntegerLiteral

i_lit

)

Definition at line 1285 of file integer.cc.

SafeEnqueue() [1/2]

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

Definition at line 1336 of file integer.cc.

SafeEnqueue() [2/2]

bool operations_research::sat::IntegerTrail::SafeEnqueue	(	IntegerLiteral	i_lit,
		absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

Definition at line 1341 of file integer.cc.

SafeEnqueueLiteral()

bool operations_research::sat::IntegerTrail::SafeEnqueueLiteral	(	Literal	literal,
		absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

Definition at line 1504 of file integer.cc.

timestamp()

int64_t operations_research::sat::IntegerTrail::timestamp ( ) const

inline

Definition at line 852 of file integer.h.

Untrail()

void operations_research::sat::IntegerTrail::Untrail ( const Trail & trail, int literal_trail_index )

finalvirtual

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 787 of file integer.cc.

UpdateInitialDomain()

bool operations_research::sat::IntegerTrail::UpdateInitialDomain	(	IntegerVariable	var,
		Domain	domain )

Definition at line 905 of file integer.cc.

UpperBound() [1/3]

IntegerValue operations_research::sat::IntegerTrail::UpperBound ( AffineExpression expr ) const

inline

Definition at line 1595 of file integer.h.

UpperBound() [2/3]

IntegerValue operations_research::sat::IntegerTrail::UpperBound ( IntegerVariable i ) const

inline

Definition at line 1541 of file integer.h.

UpperBound() [3/3]

IntegerValue operations_research::sat::IntegerTrail::UpperBound ( LinearExpression2 expr ) const

inline

Definition at line 1600 of file integer.h.

UpperBoundAsLiteral() [1/2]

IntegerLiteral operations_research::sat::IntegerTrail::UpperBoundAsLiteral ( AffineExpression expr ) const

inline

Definition at line 1630 of file integer.h.

UpperBoundAsLiteral() [2/2]

IntegerLiteral operations_research::sat::IntegerTrail::UpperBoundAsLiteral ( IntegerVariable i ) const

inline

Definition at line 1585 of file integer.h.

UseNewConflictResolution()

void operations_research::sat::IntegerTrail::UseNewConflictResolution ( )

inline

Definition at line 996 of file integer.h.

VarAtIndex()

IntegerVariable operations_research::sat::IntegerTrail::VarAtIndex ( int integer_trail_index ) const

inline

Definition at line 865 of file integer.h.

VariableLowerBoundIsFromLevelZero()

bool operations_research::sat::IntegerTrail::VariableLowerBoundIsFromLevelZero ( IntegerVariable var ) const

inline

Definition at line 931 of file integer.h.

---

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

• ortools/sat/integer.h
• ortools/sat/integer.cc