14#ifndef OR_TOOLS_SAT_INTERVALS_H_
15#define OR_TOOLS_SAT_INTERVALS_H_
20#include "absl/types/span.h"
61 IntervalVariable
CreateInterval(IntegerVariable start, IntegerVariable end,
62 IntegerVariable size, IntegerValue fixed_size,
63 LiteralIndex is_present);
66 LiteralIndex is_present,
67 bool add_linear_relation);
97 IntegerVariable
SizeVar(IntervalVariable i)
const {
102 return sizes_[i].var;
104 IntegerVariable
StartVar(IntervalVariable i)
const {
109 return starts_[i].var;
111 IntegerVariable
EndVar(IntervalVariable i)
const {
120 IntegerValue
MinSize(IntervalVariable i)
const {
125 IntegerValue
MaxSize(IntervalVariable i)
const {
131 std::vector<IntervalVariable> result;
199 absl::Span<const int> tasks);
223 IntegerValue
SizeMin(
int t)
const {
return cached_duration_min_[t]; }
228 IntegerValue
StartMin(
int t)
const {
return cached_start_min_[t]; }
229 IntegerValue
EndMin(
int t)
const {
return cached_end_min_[t]; }
230 IntegerValue
StartMax(
int t)
const {
return -cached_negated_start_max_[t]; }
231 IntegerValue
EndMax(
int t)
const {
return -cached_negated_end_max_[t]; }
248 return cached_shifted_start_min_[t];
297 return &integer_reason_;
309 ABSL_MUST_USE_RESULT
bool IncreaseStartMin(
int t, IntegerValue new_start_min);
310 ABSL_MUST_USE_RESULT
bool DecreaseEndMax(
int t, IntegerValue new_start_max);
319 const std::vector<AffineExpression>&
Starts()
const {
return starts_; }
320 const std::vector<AffineExpression>&
Ends()
const {
return ends_; }
321 const std::vector<AffineExpression>&
Sizes()
const {
return sizes_; }
330 bool watch_start_max =
true,
331 bool watch_end_max =
true)
const;
339 IntegerValue event) {
340 CHECK(other_helper !=
nullptr);
341 other_helper_ = other_helper;
342 event_for_other_helper_ = event;
359 void InitSortedVectors();
360 void UpdateCachedValues(
int t);
369 void AddOtherReason(
int t);
372 void ImportOtherReasons();
379 bool current_time_direction_ =
true;
383 std::vector<AffineExpression> starts_;
384 std::vector<AffineExpression> ends_;
385 std::vector<AffineExpression> sizes_;
386 std::vector<LiteralIndex> reason_for_presence_;
390 std::vector<AffineExpression> minus_starts_;
391 std::vector<AffineExpression> minus_ends_;
394 int previous_level_ = 0;
397 std::vector<IntegerValue> cached_duration_min_;
398 std::vector<IntegerValue> cached_start_min_;
399 std::vector<IntegerValue> cached_end_min_;
400 std::vector<IntegerValue> cached_negated_start_max_;
401 std::vector<IntegerValue> cached_negated_end_max_;
402 std::vector<IntegerValue> cached_shifted_start_min_;
403 std::vector<IntegerValue> cached_negated_shifted_end_max_;
406 std::vector<TaskTime> task_by_increasing_start_min_;
407 std::vector<TaskTime> task_by_increasing_end_min_;
408 std::vector<TaskTime> task_by_decreasing_start_max_;
409 std::vector<TaskTime> task_by_decreasing_end_max_;
413 std::vector<TaskTime> task_by_increasing_shifted_start_min_;
414 std::vector<TaskTime> task_by_negated_shifted_end_max_;
415 bool recompute_shifted_start_min_ =
true;
416 bool recompute_negated_shifted_end_max_ =
true;
420 bool recompute_all_cache_ =
true;
421 std::vector<bool> recompute_cache_;
424 std::vector<Literal> literal_reason_;
425 std::vector<IntegerLiteral> integer_reason_;
429 IntegerValue event_for_other_helper_;
430 std::vector<bool> already_added_to_other_reasons_;
438 return integer_trail_->
IsFixed(starts_[t]);
442 return integer_trail_->
IsFixed(ends_[t]);
446 return integer_trail_->
IsFixed(sizes_[t]);
464 integer_reason_.clear();
465 literal_reason_.clear();
468 already_added_to_other_reasons_.assign(
NumTasks(),
false);
476 literal_reason_.push_back(
Literal(reason_for_presence_[t]).Negated());
484 literal_reason_.push_back(
Literal(reason_for_presence_[t]));
491 integer_reason_.push_back(
497 int t, IntegerValue lower_bound) {
505 int t, IntegerValue lower_bound) {
509 integer_reason_.push_back(starts_[t].
GreaterOrEqual(lower_bound));
514 int t, IntegerValue upper_bound) {
518 if (integer_trail_->
UpperBound(starts_[t]) <= upper_bound) {
520 integer_reason_.push_back(starts_[t].
LowerOrEqual(upper_bound));
525 integer_reason_.push_back(
529 integer_reason_.push_back(
536 int t, IntegerValue lower_bound) {
540 if (integer_trail_->
LowerBound(ends_[t]) >= lower_bound) {
547 integer_reason_.push_back(
551 integer_reason_.push_back(
558 int t, IntegerValue upper_bound) {
562 integer_reason_.push_back(ends_[t].
LowerOrEqual(upper_bound));
567 int t, IntegerValue energy_min, IntegerValue
time) {
588 IntervalVariable v) {
594inline std::function<IntegerVariable(
const Model&)>
EndVar(IntervalVariable v) {
601 IntervalVariable v) {
626 IntervalVariable v) {
644 IntegerVariable start, IntegerVariable end, IntegerVariable size) {
668 IntegerValue(size), is_present.
Index());
672inline std::function<IntervalVariable(Model*)>
677 const IntegerVariable start =
679 const IntegerVariable end =
683 integer_trail->MarkIntegerVariableAsOptional(end, is_present);
690 IntegerVariable start, IntegerVariable end, IntegerVariable size,
694 start, end, size, IntegerValue(0), is_present.
Index());
698inline std::function<IntervalVariable(Model*)>
713 IntervalVariable parent,
const std::vector<IntervalVariable>& members) {
718 std::vector<Literal> presences;
719 std::vector<IntegerValue> sizes;
722 std::vector<LiteralWithCoeff> sat_ct;
723 for (
const IntervalVariable member : members) {
725 const Literal is_present = intervals->PresenceLiteral(member);
726 sat_ct.push_back({is_present, Coefficient(1)});
734 CHECK(integer_trail->IsFixed(intervals->Size(member)));
735 presences.push_back(is_present);
736 sizes.push_back(intervals->MinSize(member));
739 model->Add(
IsOneOf(intervals->SizeVar(parent), presences, sizes));
745 std::vector<IntegerVariable> starts;
746 starts.reserve(members.size());
747 for (
const IntervalVariable member : members) {
748 starts.push_back(intervals->StartVar(member));
754 std::vector<IntegerVariable> ends;
755 ends.reserve(members.size());
756 for (
const IntervalVariable member : members) {
757 ends.push_back(intervals->EndVar(member));
#define DCHECK_LE(val1, val2)
#define CHECK_EQ(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK(condition)
An Assignment is a variable -> domains mapping, used to report solutions to the user.
bool IsFixed(IntegerVariable i) const
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
bool InPropagationLoop() const
IntegerValue UpperBound(IntegerVariable i) const
void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered)
IntegerValue LowerBound(IntegerVariable i) const
bool IsOptional(IntegerVariable i) const
IntegerVariable SizeVar(IntervalVariable i) const
AffineExpression End(IntervalVariable i) const
IntegerValue MaxSize(IntervalVariable i) const
AffineExpression Start(IntervalVariable i) const
Literal PresenceLiteral(IntervalVariable i) const
std::vector< IntervalVariable > AllIntervals() const
IntegerVariable StartVar(IntervalVariable i) const
IntegerValue MinSize(IntervalVariable i) const
IntervalsRepository(Model *model)
IntegerVariable EndVar(IntervalVariable i) const
bool IsPresent(IntervalVariable i) const
AffineExpression Size(IntervalVariable i) const
bool IsAbsent(IntervalVariable i) const
bool IsOptional(IntervalVariable i) const
IntervalVariable CreateInterval(IntegerVariable start, IntegerVariable end, IntegerVariable size, IntegerValue fixed_size, LiteralIndex is_present)
LiteralIndex Index() const
Class that owns everything related to a particular optimization model.
std::vector< Literal > * MutableLiteralReason()
bool StartIsFixed(int t) const
IntegerValue ShiftedStartMin(int t) const
IntegerValue EndMin(int t) const
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
const std::vector< AffineExpression > & Starts() const
const std::vector< TaskTime > & TaskByDecreasingEndMax()
std::vector< IntegerLiteral > * MutableIntegerReason()
void SetLevel(int level) final
ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t)
SchedulingConstraintHelper(const std::vector< IntervalVariable > &tasks, Model *model)
void AddSizeMinReason(int t)
const std::vector< TaskTime > & TaskByIncreasingStartMin()
void AddStartMinReason(int t, IntegerValue lower_bound)
void WatchAllTasks(int id, GenericLiteralWatcher *watcher, bool watch_start_max=true, bool watch_end_max=true) const
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
void AddPresenceReason(int t)
const std::vector< TaskTime > & TaskByIncreasingEndMin()
void ResetFromSubset(const SchedulingConstraintHelper &other, absl::Span< const int > tasks)
bool IsPresent(int t) const
bool SizeIsFixed(int t) const
void AddEnergyAfterReason(int t, IntegerValue energy_min, IntegerValue time)
bool InPropagationLoop() const
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t, IntegerLiteral lit)
void RegisterWith(GenericLiteralWatcher *watcher)
std::string TaskDebugString(int t) const
void AddEndMinReason(int t, IntegerValue lower_bound)
bool EndIsFixed(int t) const
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_start_min)
const std::vector< AffineExpression > & Sizes() const
void SynchronizeAndSetTimeDirection(bool is_forward)
bool IsAbsent(int t) const
IntegerValue EndMax(int t) const
ABSL_MUST_USE_RESULT bool ReportConflict()
ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_start_max)
bool IsOptional(int t) const
IntegerValue StartMin(int t) const
const std::vector< TaskTime > & TaskByDecreasingStartMax()
ABSL_MUST_USE_RESULT bool PushTaskPresence(int t)
void AddAbsenceReason(int t)
Literal PresenceLiteral(int index) const
void AddEndMaxReason(int t, IntegerValue upper_bound)
void SetOtherHelper(SchedulingConstraintHelper *other_helper, IntegerValue event)
IntegerValue StartMax(int t) const
const std::vector< TaskTime > & TaskByIncreasingShiftedStartMin()
void AddReasonForBeingBefore(int before, int after)
void AddStartMaxReason(int t, IntegerValue upper_bound)
const std::vector< AffineExpression > & Ends() const
IntegerValue SizeMax(int t) const
IntegerValue SizeMin(int t) const
const VariablesAssignment & Assignment() const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
std::function< IntegerVariable(const Model &)> SizeVar(IntervalVariable v)
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
std::function< IntegerVariable(const Model &)> EndVar(IntervalVariable v)
std::function< void(Model *)> BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
const LiteralIndex kNoLiteralIndex(-1)
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
std::function< IntegerVariable(const Model &)> StartVar(IntervalVariable v)
std::function< void(Model *)> PartialIsOneOfVar(IntegerVariable target_var, const std::vector< IntegerVariable > &vars, const std::vector< Literal > &selectors)
DEFINE_INT_TYPE(ClauseIndex, int)
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithOptionalVariables(int64 min_start, int64 max_end, int64 size, Literal is_present)
const IntegerVariable kNoIntegerVariable(-1)
const IntervalVariable kNoIntervalVariable(-1)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
std::function< IntervalVariable(Model *)> NewIntervalWithVariableSize(int64 min_start, int64 max_end, int64 min_size, int64 max_size)
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
std::function< bool(const Model &)> IsOptional(IntervalVariable v)
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithVariableSize(int64 min_start, int64 max_end, int64 min_size, int64 max_size, Literal is_present)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
std::function< int64(const Model &)> MinSize(IntervalVariable v)
std::function< int64(const Model &)> MaxSize(IntervalVariable v)
std::function< Literal(const Model &)> IsPresentLiteral(IntervalVariable v)
std::function< void(Model *)> IntervalWithAlternatives(IntervalVariable parent, const std::vector< IntervalVariable > &members)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
bool operator<(TaskTime other) const
bool operator>(TaskTime other) const