#include <precedences.h>

Public Member Functions
	BinaryRelationsMaps (Model *model)
	~BinaryRelationsMaps ()
void	AddRelationBounds (LinearExpression2 expr, IntegerValue lb, IntegerValue ub)
RelationStatus	GetLevelZeroStatus (LinearExpression2 expr, IntegerValue lb, IntegerValue ub) const
RelationStatus	GetLevelZeroPrecedenceStatus (AffineExpression a, AffineExpression b) const
	Return the status of a <= b;.
void	AddReifiedPrecedenceIfNonTrivial (Literal l, AffineExpression a, AffineExpression b)
LiteralIndex	GetReifiedPrecedence (AffineExpression a, AffineExpression b)
bool	AddAffineUpperBound (LinearExpression2 expr, AffineExpression affine_ub)
IntegerValue	UpperBound (LinearExpression2 expr) const
void	AddReasonForUpperBoundLowerThan (LinearExpression2 expr, IntegerValue ub, std::vector< Literal > literal_reason, std::vector< IntegerLiteral > integer_reason) const
std::vector< LinearExpression2 >	GetAllExpressionsWithAffineBounds () const
	Warning, the order will not be deterministic.
int	NumExpressionsWithAffineBounds () const
void	WatchAllLinearExpressions2 (int id)

Detailed Description

Todo: (user): Merge with BinaryRelationRepository. Note that this one provides different indexing though, so it could be kept separate. The LinearExpression2 data structure is also slightly more efficient.

Definition at line 591 of file precedences.h.

Constructor & Destructor Documentation

◆ BinaryRelationsMaps()

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

explicit

Linear scan.

Definition at line 1534 of file precedences.cc.

◆ ~BinaryRelationsMaps()

operations_research::sat::BinaryRelationsMaps::~BinaryRelationsMaps ( )

Definition at line 1568 of file precedences.cc.

Member Function Documentation

◆ AddAffineUpperBound()

bool operations_research::sat::BinaryRelationsMaps::AddAffineUpperBound	(	LinearExpression2	expr,
		AffineExpression	affine_ub )

If the given upper bound evaluate better than the current one we have, this will replace it and returns true, otherwise it returns false.

Note: we never store trivial upper bound (using the current variable domain).

Not better than trivial upper bound.

Not better than the root level upper bound.

We have an affine bound for this expr in the map. Can be exactly the same, a better one or a worse one.

The affine bound is already in the map.

We have gcd * canonical_expr <= affine_ub, so we do need to store a "divisor".

Definition at line 1698 of file precedences.cc.

◆ AddReasonForUpperBoundLowerThan()

void operations_research::sat::BinaryRelationsMaps::AddReasonForUpperBoundLowerThan	(	LinearExpression2	expr,
		IntegerValue	ub,
		std::vector< Literal > *	literal_reason,
		std::vector< IntegerLiteral > *	integer_reason ) const

Todo: (user): If the trivial bound is better, its explanation is different...

Starts by simple bounds.

Add explanation if it is a trivial bound.

None of the bound above are enough, try the affine one. Note that gcd * expr <= ub, is the same as asking why expr <= FloorRatio(ub, gcd).

We want the reason for "expr <= ub", that is the reason for

"gcd * canonical_expr <= ub"
"canonical_expr <= FloorRatio(ub, gcd);

knowing that canonical_expr <= affine_ub / divisor.

Definition at line 1761 of file precedences.cc.

◆ AddReifiedPrecedenceIfNonTrivial()

void operations_research::sat::BinaryRelationsMaps::AddReifiedPrecedenceIfNonTrivial	(	Literal	l,
		AffineExpression	a,
		AffineExpression	b )

Register the fact that l <=> ( a <= b ). These are considered equivalence relation.

Definition at line 1669 of file precedences.cc.

◆ AddRelationBounds()

void operations_research::sat::BinaryRelationsMaps::AddRelationBounds	(	LinearExpression2	expr,
		IntegerValue	lb,
		IntegerValue	ub )

This mainly wraps BestBinaryRelationBounds, but in addition it checks the current LevelZero variable bounds to detect trivially true or false relation.

Todo: (user): Also push them to a global shared repository after remapping IntegerVariable to proto indices.

Definition at line 1614 of file precedences.cc.

◆ GetAllExpressionsWithAffineBounds()

std::vector< LinearExpression2 > operations_research::sat::BinaryRelationsMaps::GetAllExpressionsWithAffineBounds ( ) const

Warning, the order will not be deterministic.

Definition at line 1801 of file precedences.cc.

◆ GetLevelZeroPrecedenceStatus()

RelationStatus operations_research::sat::BinaryRelationsMaps::GetLevelZeroPrecedenceStatus	(	AffineExpression	a,
		AffineExpression	b ) const

Return the status of a <= b;.

Definition at line 1663 of file precedences.cc.

◆ GetLevelZeroStatus()

RelationStatus operations_research::sat::BinaryRelationsMaps::GetLevelZeroStatus	(	LinearExpression2	expr,
		IntegerValue	lb,
		IntegerValue	ub ) const

Returns directly if the status can be derived from the implied bounds.

Relax as best_root_level_bounds_.GetStatus() might have older bounds.

Definition at line 1631 of file precedences.cc.

◆ GetReifiedPrecedence()

LiteralIndex operations_research::sat::BinaryRelationsMaps::GetReifiedPrecedence	(	AffineExpression	a,
		AffineExpression	b )

Returns kNoLiteralIndex if we don't have a literal <=> ( a <= b ), or returns that literal if we have one. Note that we will return the true/false literal if the status is known at level zero.

Definition at line 1682 of file precedences.cc.

◆ NumExpressionsWithAffineBounds()

int operations_research::sat::BinaryRelationsMaps::NumExpressionsWithAffineBounds ( ) const

inline

Definition at line 637 of file precedences.h.

◆ UpperBound()

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

Returns the best known upper-bound of the given LinearExpression2 at the current decision level. If its explanation is needed, it can be queried with the second function.

Definition at line 1740 of file precedences.cc.

◆ WatchAllLinearExpressions2()

void operations_research::sat::BinaryRelationsMaps::WatchAllLinearExpressions2 ( int id )