#include <disjunctive.h>

Inheritance diagram for operations_research::sat::DisjunctiveNotLast:

Public Member Functions
	DisjunctiveNotLast (bool time_direction, SchedulingConstraintHelper helper, Model model=nullptr)

bool	Propagate () final

int	RegisterWith (GenericLiteralWatcher *watcher)

Public Member Functions inherited from operations_research::sat::PropagatorInterface
	PropagatorInterface ()=default

virtual	~PropagatorInterface ()=default

virtual bool	IncrementalPropagate (const std::vector< int > &)

Detailed Description

Definition at line 285 of file disjunctive.h.

Constructor & Destructor Documentation

◆ DisjunctiveNotLast()

operations_research::sat::DisjunctiveNotLast::DisjunctiveNotLast	(	bool	time_direction,
		SchedulingConstraintHelper *	helper,
		Model *	model = nullptr )

inline

Definition at line 287 of file disjunctive.h.

Member Function Documentation

◆ Propagate()

bool operations_research::sat::DisjunctiveNotLast::Propagate ( )

finalvirtual

This will be called after one or more literals that are watched by this propagator changed. It will also always be called on the first propagation cycle after registration.

Split problem into independent part.

The situation is trickier here, and we use two windows:

The classical "start_min_window_" as in the other propagator.
A second window, that includes all the task with a start_max inside [window_start, window_end].

Now, a task from the second window can be detected to be "not last" by only looking at the task in the first window. Tasks to the left do not cause issue for the task to be last, and tasks to the right will not lower the end-min of the task under consideration.

Add to start_max_window_ all the task whose start_max fall into [window_start, window_end).

Note: we add task whose presence is still unknown here.

If this is the case, we cannot propagate more than the detectable precedence propagator. Note that this continue must happen after we computed start_max_window_ though.

Process current window.

Implements operations_research::sat::PropagatorInterface.

Definition at line 1345 of file disjunctive.cc.

◆ RegisterWith()

int operations_research::sat::DisjunctiveNotLast::RegisterWith ( GenericLiteralWatcher * watcher )

Definition at line 1545 of file disjunctive.cc.

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