This is meant as an helper to deal with enforcement for any constraint. More...

#include <linear_propagation.h>

Inheritance diagram for operations_research::sat::EnforcementPropagator:

Public Member Functions
	EnforcementPropagator (Model *model)

bool	Propagate (Trail *trail) final
	SatPropagator interface.

void	Untrail (const Trail &trail, int trail_index) final

EnforcementId	Register (absl::Span< const Literal > enforcement, std::function< void(EnforcementId, EnforcementStatus)> callback=nullptr)

void	AddEnforcementReason (EnforcementId id, std::vector< Literal > *reason) const
	Add the enforcement reason to the given vector.

ABSL_MUST_USE_RESULT bool	PropagateWhenFalse (EnforcementId id, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)

EnforcementStatus	Status (EnforcementId id) const

EnforcementStatus	DebugStatus (EnforcementId id)

absl::Span< const Literal >	GetEnforcementLiterals (EnforcementId id) const
	Returns the enforcement literals of the given id.

Public Member Functions inherited from operations_research::sat::SatPropagator
	SatPropagator (const std::string &name)

	SatPropagator (const SatPropagator &)=delete
	This type is neither copyable nor movable.

SatPropagator &	operator= (const SatPropagator &)=delete

virtual	~SatPropagator ()=default

void	SetPropagatorId (int id)
	Sets/Gets this propagator unique id.

int	PropagatorId () const

virtual absl::Span< const Literal >	Reason (const Trail &, int, int64_t) const

bool	PropagatePreconditionsAreSatisfied (const Trail &trail) const
	######################## Implementations below ########################

bool	PropagationIsDone (const Trail &trail) const
	Returns true iff all the trail was inspected by this propagator.

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_

Detailed Description

This is meant as an helper to deal with enforcement for any constraint.

Definition at line 65 of file linear_propagation.h.

Constructor & Destructor Documentation

◆ EnforcementPropagator()

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

explicit

Note: this will be after the integer trail since rev_int_repository_ depends on IntegerTrail.

Sentinel - also start of next Register().

Definition at line 71 of file linear_propagation.cc.

Member Function Documentation

◆ AddEnforcementReason()

void operations_research::sat::EnforcementPropagator::AddEnforcementReason	(	EnforcementId	id,
		std::vector< Literal > *	reason ) const

Add the enforcement reason to the given vector.

Definition at line 250 of file linear_propagation.cc.

◆ DebugStatus()

EnforcementStatus operations_research::sat::EnforcementPropagator::DebugStatus ( EnforcementId id )

Recompute the status from the current assignment. This should only used in DCHECK().

Definition at line 361 of file linear_propagation.cc.

◆ GetEnforcementLiterals()

absl::Span< const Literal > operations_research::sat::EnforcementPropagator::GetEnforcementLiterals ( EnforcementId id ) const

inline

Returns the enforcement literals of the given id.

Definition at line 101 of file linear_propagation.h.

◆ Propagate()

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

finalvirtual

SatPropagator interface.

We keep the same watcher.

Change the watcher.

We also mark some constraint false.

Compute the enforcement status of any constraint added at a positive level. This is only needed until we are back to level zero.

Implements operations_research::sat::SatPropagator.

Definition at line 85 of file linear_propagation.cc.

◆ PropagateWhenFalse()

bool operations_research::sat::EnforcementPropagator::PropagateWhenFalse	(	EnforcementId	id,
		absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

Try to propagate when the enforced constraint is not satisfiable. This is currently in O(enforcement_size).

Try to propagate when the enforced constraint is not satisfiable. This is currently in O(enforcement_size);

We also change the status right away.

Definition at line 259 of file linear_propagation.cc.

◆ Register()

EnforcementId operations_research::sat::EnforcementPropagator::Register	(	absl::Span< const Literal >	enforcement,
		std::function< void(EnforcementId, EnforcementStatus)>	callback = nullptr )

Adds a new constraint to the class and register a callback that will be called on status change. Note that we also call the callback with the initial status if different from CANNOT_PROPAGATE when added.

It is better to not call this for empty enforcement list, but you can. A negative id means the level zero status will never change, and only the first call to callback() should be necessary, we don't save it.

Adds a new constraint to the class and returns the constraint id.

Note: we accept empty enforcement list so that client code can be used regardless of the presence of enforcement or not. A negative id means the constraint is never enforced, and should be ignored.

Make sure we always have enough room for the literal and its negation.

Return special indices if never/always enforced.

The default status at level zero.

Make sure we watch correct literals.

We need to watch one of the literals at highest level.

Change status, call callback and set up untrail if the status is different from EnforcementStatus::CANNOT_PROPAGATE.

Because this is the default status, we still need to call the callback.

Tricky: if we added something at a positive level, and its status is not CANNOT_PROPAGATE, then we might need to fix it on backtrack.

Definition at line 142 of file linear_propagation.cc.

◆ Status()

EnforcementStatus operations_research::sat::EnforcementPropagator::Status ( EnforcementId id ) const

inline

Definition at line 94 of file linear_propagation.h.

◆ Untrail()

void operations_research::sat::EnforcementPropagator::Untrail	(	const Trail &	,
		int	trail_index )

finalvirtual

Reverts the state so that all the literals with a trail index greater or equal to the given one are not processed for propagation. Note that the trail current decision level is already reverted before this is called.

Todo: (user): Currently this is called at each Backtrack(), but we could bundle the calls in case multiple conflict one after the other are detected even before the Propagate() call of a SatPropagator is called.

Todo: (user): It is not yet 100% the case, but this can be guaranteed to be called with a trail index that will always be the start of a new decision level.

Simply revert the status change.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 125 of file linear_propagation.cc.

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

ortools/sat/linear_propagation.h
ortools/sat/linear_propagation.cc

Public Member Functions

Additional Inherited Members