23#include "absl/log/check.h"
24#include "absl/strings/str_cat.h"
25#include "absl/types/span.h"
43 std::vector<AffineExpression> starts, std::vector<AffineExpression> ends,
44 std::vector<AffineExpression> sizes,
45 std::vector<LiteralIndex> reason_for_presence,
Model* model)
47 sat_solver_(model->GetOrCreate<
SatSolver>()),
52 starts_(
std::move(starts)),
53 ends_(
std::move(ends)),
54 sizes_(
std::move(sizes)),
55 reason_for_presence_(
std::move(reason_for_presence)),
56 capacity_(starts_.size()),
57 cached_size_min_(new IntegerValue[capacity_]),
58 cached_start_min_(new IntegerValue[capacity_]),
59 cached_end_min_(new IntegerValue[capacity_]),
60 cached_negated_start_max_(new IntegerValue[capacity_]),
61 cached_negated_end_max_(new IntegerValue[capacity_]),
62 cached_shifted_start_min_(new IntegerValue[capacity_]),
63 cached_negated_shifted_end_max_(new IntegerValue[capacity_]) {
64 DCHECK_EQ(starts_.size(), ends_.size());
65 DCHECK_EQ(starts_.size(), sizes_.size());
66 DCHECK_EQ(starts_.size(), reason_for_presence_.size());
68 minus_starts_.clear();
69 minus_starts_.reserve(starts_.size());
71 minus_ends_.reserve(starts_.size());
72 for (
int i = 0;
i < starts_.size(); ++
i) {
73 minus_starts_.push_back(starts_[
i].Negated());
74 minus_ends_.push_back(ends_[
i].Negated());
86 sat_solver_(model->GetOrCreate<
SatSolver>()),
91 cached_size_min_(new IntegerValue[capacity_]),
92 cached_start_min_(new IntegerValue[capacity_]),
93 cached_end_min_(new IntegerValue[capacity_]),
94 cached_negated_start_max_(new IntegerValue[capacity_]),
95 cached_negated_end_max_(new IntegerValue[capacity_]),
96 cached_shifted_start_min_(new IntegerValue[capacity_]),
97 cached_negated_shifted_end_max_(new IntegerValue[capacity_]) {
98 starts_.resize(num_tasks);
103 recompute_all_cache_ =
true;
104 for (
const int id : propagator_ids_) watcher_->CallOnNextPropagate(
id);
109 const std::vector<int>& watch_indices) {
110 for (
const int t : watch_indices) recompute_cache_.Set(t);
111 for (
const int id : propagator_ids_) watcher_->CallOnNextPropagate(
id);
116 const int id = watcher->
Register(
this);
117 const int num_tasks = starts_.size();
118 for (
int t = 0; t < num_tasks; ++t) {
130 watcher_->WatchLiteral(
Literal(reason_for_presence_[t]),
id);
136bool SchedulingConstraintHelper::UpdateCachedValues(
int t) {
139 IntegerValue smin = integer_trail_->
LowerBound(starts_[t]);
140 IntegerValue smax = integer_trail_->
UpperBound(starts_[t]);
141 IntegerValue emin = integer_trail_->
LowerBound(ends_[t]);
142 IntegerValue emax = integer_trail_->
UpperBound(ends_[t]);
150 std::max(IntegerValue(0), integer_trail_->
LowerBound(sizes_[t]));
151 IntegerValue dmax = integer_trail_->
UpperBound(sizes_[t]);
159 if (smin + dmin - emax > 0) {
166 if (smax + dmax - emin < 0) {
180 smin = std::max(smin, emin - dmax);
181 smax = std::min(smax, emax - dmin);
182 dmin = std::max(dmin, emin - smax);
183 emin = std::max(emin, smin + dmin);
184 emax = std::min(emax, smax + dmax);
186 if (emin != cached_end_min_[t]) {
187 recompute_energy_profile_ =
true;
192 recompute_by_start_max_ =
true;
193 recompute_by_end_min_ =
true;
195 cached_start_min_[t] = smin;
196 cached_end_min_[t] = emin;
197 cached_negated_start_max_[t] = -smax;
198 cached_negated_end_max_[t] = -emax;
199 cached_size_min_[t] = dmin;
202 const IntegerValue new_shifted_start_min = emin - dmin;
203 if (new_shifted_start_min != cached_shifted_start_min_[t]) {
204 recompute_energy_profile_ =
true;
205 recompute_shifted_start_min_ =
true;
206 cached_shifted_start_min_[t] = new_shifted_start_min;
208 const IntegerValue new_negated_shifted_end_max = -(smax + dmin);
209 if (new_negated_shifted_end_max != cached_negated_shifted_end_max_[t]) {
210 recompute_negated_shifted_end_max_ =
true;
211 cached_negated_shifted_end_max_[t] = new_negated_shifted_end_max;
218 current_time_direction_ = other.current_time_direction_;
220 const int num_tasks = tasks.size();
221 CHECK_LE(num_tasks, capacity_);
222 starts_.resize(num_tasks);
223 ends_.resize(num_tasks);
224 minus_ends_.resize(num_tasks);
225 minus_starts_.resize(num_tasks);
226 sizes_.resize(num_tasks);
227 reason_for_presence_.resize(num_tasks);
228 for (
int i = 0;
i < num_tasks; ++
i) {
229 const int t = tasks[
i];
230 starts_[
i] = other.starts_[t];
231 ends_[
i] = other.ends_[t];
232 minus_ends_[
i] = other.minus_ends_[t];
233 minus_starts_[
i] = other.minus_starts_[t];
234 sizes_[
i] = other.sizes_[t];
235 reason_for_presence_[
i] = other.reason_for_presence_[t];
242void SchedulingConstraintHelper::InitSortedVectors() {
243 const int num_tasks = starts_.size();
245 recompute_all_cache_ =
true;
246 recompute_cache_.
Resize(num_tasks);
247 non_fixed_intervals_.resize(num_tasks);
248 for (
int t = 0; t < num_tasks; ++t) {
249 non_fixed_intervals_[t] = t;
250 recompute_cache_.
Set(t);
254 CHECK_LE(num_tasks, capacity_);
256 task_by_increasing_start_min_.resize(num_tasks);
257 task_by_increasing_end_min_.resize(num_tasks);
258 task_by_increasing_negated_start_max_.resize(num_tasks);
259 task_by_decreasing_end_max_.resize(num_tasks);
260 task_by_increasing_shifted_start_min_.resize(num_tasks);
261 task_by_negated_shifted_end_max_.resize(num_tasks);
262 for (
int t = 0; t < num_tasks; ++t) {
263 task_by_increasing_start_min_[t].task_index = t;
264 task_by_increasing_end_min_[t].task_index = t;
265 task_by_increasing_negated_start_max_[t].task_index = t;
266 task_by_decreasing_end_max_[t].task_index = t;
268 task_by_increasing_shifted_start_min_[t].task_index = t;
269 task_by_increasing_shifted_start_min_[t].presence_lit =
270 reason_for_presence_[t];
271 task_by_negated_shifted_end_max_[t].task_index = t;
272 task_by_negated_shifted_end_max_[t].presence_lit = reason_for_presence_[t];
275 recompute_by_start_max_ =
true;
276 recompute_by_end_min_ =
true;
277 recompute_energy_profile_ =
true;
278 recompute_shifted_start_min_ =
true;
279 recompute_negated_shifted_end_max_ =
true;
283 if (current_time_direction_ != is_forward) {
284 current_time_direction_ = is_forward;
286 std::swap(starts_, minus_ends_);
287 std::swap(ends_, minus_starts_);
289 std::swap(task_by_increasing_start_min_, task_by_decreasing_end_max_);
290 std::swap(task_by_increasing_end_min_,
291 task_by_increasing_negated_start_max_);
292 std::swap(recompute_by_end_min_, recompute_by_start_max_);
293 std::swap(task_by_increasing_shifted_start_min_,
294 task_by_negated_shifted_end_max_);
296 recompute_energy_profile_ =
true;
297 std::swap(cached_start_min_, cached_negated_end_max_);
298 std::swap(cached_end_min_, cached_negated_start_max_);
299 std::swap(cached_shifted_start_min_, cached_negated_shifted_end_max_);
300 std::swap(recompute_shifted_start_min_, recompute_negated_shifted_end_max_);
310 if (sat_solver_->num_backtracks() != saved_num_backtracks_) {
311 recompute_all_cache_ =
true;
312 saved_num_backtracks_ = sat_solver_->num_backtracks();
315 if (recompute_all_cache_) {
316 for (
const int t : non_fixed_intervals_) {
317 if (!UpdateCachedValues(t))
return false;
322 if (sat_solver_->CurrentDecisionLevel() == 0) {
324 for (
const int t : non_fixed_intervals_) {
329 non_fixed_intervals_[new_size++] = t;
331 non_fixed_intervals_.resize(new_size);
334 for (
const int t : recompute_cache_) {
335 if (!UpdateCachedValues(t))
return false;
338 recompute_cache_.ClearAll();
339 recompute_all_cache_ =
false;
346 int a,
int b,
bool add_reason_if_after) {
353 const IntegerValue conditional_ub = precedence_relations_->UpperBound(expr);
354 const IntegerValue level_zero_ub = integer_trail_->LevelZeroUpperBound(expr);
355 const IntegerValue expr_ub = std::min(conditional_ub, level_zero_ub);
358 const IntegerValue ub_of_end_minus_start = expr_ub + needed_offset;
359 const IntegerValue distance = -ub_of_end_minus_start;
360 if (add_reason_if_after && distance >= 0 && level_zero_ub > conditional_ub) {
361 precedence_relations_->AddReasonForUpperBoundLowerThan(
374 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
378 if (after.
coeff != 1)
return true;
379 if (before.
coeff != 1)
return true;
382 if (before.
var == after.
var) {
386 sat_solver_->NotifyThatModelIsUnsat();
393 if (precedence_relations_->AddUpperBound(expr, -offset)) {
398 -offset.value(), model_);
403 {int64_t{1}, int64_t{-1}}, -offset.value(),
406 if (sat_solver_->ModelIsUnsat())
return false;
411absl::Span<const TaskTime>
413 for (
TaskTime& ref : task_by_increasing_start_min_) {
414 ref.time =
StartMin(ref.task_index);
417 task_by_increasing_start_min_.end());
418 return task_by_increasing_start_min_;
421absl::Span<const TaskTime>
423 if (!recompute_by_end_min_)
return task_by_increasing_end_min_;
424 for (
TaskTime& ref : task_by_increasing_end_min_) {
425 ref.time =
EndMin(ref.task_index);
428 task_by_increasing_end_min_.end());
429 recompute_by_end_min_ =
false;
430 return task_by_increasing_end_min_;
433absl::Span<const TaskTime>
435 if (!recompute_by_start_max_)
return task_by_increasing_negated_start_max_;
436 for (
TaskTime& ref : task_by_increasing_negated_start_max_) {
437 ref.time = cached_negated_start_max_[ref.task_index];
440 task_by_increasing_negated_start_max_.end());
441 recompute_by_start_max_ =
false;
442 return task_by_increasing_negated_start_max_;
445absl::Span<const TaskTime>
447 for (
TaskTime& ref : task_by_decreasing_end_max_) {
448 ref.time =
EndMax(ref.task_index);
451 task_by_decreasing_end_max_.end(), std::greater<TaskTime>());
452 return task_by_decreasing_end_max_;
455absl::Span<const CachedTaskBounds>
457 if (recompute_shifted_start_min_) {
458 recompute_shifted_start_min_ =
false;
459 bool is_sorted =
true;
463 is_sorted = is_sorted && ref.time >= previous;
466 if (is_sorted)
return task_by_increasing_shifted_start_min_;
468 task_by_increasing_shifted_start_min_.end());
470 return task_by_increasing_shifted_start_min_;
474const std::vector<SchedulingConstraintHelper::ProfileEvent>&
476 if (energy_profile_.empty()) {
478 for (
int t = 0; t < num_tasks; ++t) {
479 energy_profile_.push_back(
480 {cached_shifted_start_min_[t], t,
true});
481 energy_profile_.push_back({cached_end_min_[t], t,
false});
484 if (!recompute_energy_profile_)
return energy_profile_;
486 const int t = ref.task;
488 ref.time = cached_shifted_start_min_[t];
490 ref.time = cached_end_min_[t];
495 recompute_energy_profile_ =
false;
496 return energy_profile_;
502 AddOtherReason(before);
503 AddOtherReason(after);
507 std::vector<IntegerVariable> vars;
508 std::vector<IntegerValue> coeffs;
511 const IntegerValue smax_before =
StartMax(before);
512 if (smax_before >= integer_trail_->UpperBound(starts_[before])) {
514 vars.push_back(
NegationOf(starts_[before].var));
515 coeffs.push_back(starts_[before].coeff);
519 vars.push_back(
NegationOf(ends_[before].var));
520 coeffs.push_back(ends_[before].coeff);
523 vars.push_back(sizes_[before].var);
524 coeffs.push_back(sizes_[before].coeff);
529 const IntegerValue emin_after =
EndMin(after);
530 if (emin_after <= integer_trail_->
LowerBound(ends_[after])) {
532 vars.push_back(ends_[after].var);
533 coeffs.push_back(ends_[after].coeff);
537 vars.push_back(starts_[after].var);
538 coeffs.push_back(starts_[after].coeff);
541 vars.push_back(sizes_[after].var);
542 coeffs.push_back(sizes_[after].coeff);
546 DCHECK_LT(smax_before, emin_after);
547 const IntegerValue slack = emin_after - smax_before - 1;
548 integer_trail_->AppendRelaxedLinearReason(slack, coeffs, vars,
553 CHECK(other_helper_ ==
nullptr);
554 return integer_trail_->Enqueue(lit, literal_reason_, integer_reason_);
563 return integer_trail_->ConditionalEnqueue(
566 return integer_trail_->Enqueue(lit, literal_reason_, integer_reason_);
571bool SchedulingConstraintHelper::PushIntervalBound(
int t,
IntegerLiteral lit) {
574 if (!UpdateCachedValues(t))
return false;
575 recompute_cache_.
Clear(t);
600 return PushIntervalBound(t, ends_[t].
LowerOrEqual(value));
604 integer_trail_->EnqueueLiteral(l, literal_reason_, integer_reason_);
615 literal_reason_.push_back(
Literal(reason_for_presence_[t]).Negated());
619 integer_trail_->EnqueueLiteral(
Literal(reason_for_presence_[t]).Negated(),
620 literal_reason_, integer_reason_);
631 literal_reason_.push_back(
Literal(reason_for_presence_[t]));
635 integer_trail_->EnqueueLiteral(
Literal(reason_for_presence_[t]),
636 literal_reason_, integer_reason_);
642 return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
649 propagator_ids_.push_back(
id);
652void SchedulingConstraintHelper::AddOtherReason(
int t) {
653 if (other_helper_ ==
nullptr || already_added_to_other_reasons_[t])
return;
654 already_added_to_other_reasons_[t] =
true;
655 const int mapped_t = map_to_other_helper_[t];
666 literal_reason_.insert(literal_reason_.end(),
667 other_helper.literal_reason_.begin(),
668 other_helper.literal_reason_.end());
669 integer_reason_.insert(integer_reason_.end(),
670 other_helper.integer_reason_.begin(),
671 other_helper.integer_reason_.end());
675 return absl::StrCat(
"t=", t,
" is_present=",
680 "]",
" start=[",
StartMin(t).value(),
",",
682 ",",
EndMax(t).value(),
"]");
687 IntegerValue
end)
const {
688 return std::min(std::min(
end - start,
SizeMin(t)),
693 IntegerValue start_min, IntegerValue start_max, IntegerValue end_min,
694 IntegerValue end_max, IntegerValue size_min, IntegerValue demand_min,
695 absl::Span<const LiteralValueValue> filtered_energy,
696 IntegerValue window_start, IntegerValue window_end) {
697 if (window_end <= window_start)
return IntegerValue(0);
700 if (end_min <= window_start)
return IntegerValue(0);
701 if (start_max >= window_end)
return IntegerValue(0);
702 const IntegerValue window_size = window_end - window_start;
703 const IntegerValue simple_energy_min =
704 demand_min * std::min({end_min - window_start, window_end - start_max,
705 size_min, window_size});
706 if (filtered_energy.empty())
return simple_energy_min;
709 for (
const auto [lit, fixed_size, fixed_demand] : filtered_energy) {
710 const IntegerValue alt_end_min = std::max(end_min, start_min + fixed_size);
711 const IntegerValue alt_start_max =
712 std::min(start_max, end_max - fixed_size);
713 const IntegerValue energy_min =
715 std::min({alt_end_min - window_start, window_end - alt_start_max,
716 fixed_size, window_size});
717 result = std::min(result, energy_min);
720 return std::max(simple_energy_min, result);
724 absl::Span<const AffineExpression> demands,
728 sat_solver_(model->GetOrCreate<
SatSolver>()),
730 demands_(demands.
begin(), demands.
end()),
732 const int num_tasks = helper->
NumTasks();
733 decomposed_energies_.resize(num_tasks);
736 energy_is_quadratic_.resize(num_tasks,
false);
745 const int num_tasks = helper_->NumTasks();
746 if (demands_.size() != num_tasks)
return;
747 for (
int t = 0; t < num_tasks; ++t) {
750 decomposed_energies_[t] = product_decomposer_->TryToDecompose(size, demand);
754IntegerValue SchedulingDemandHelper::SimpleEnergyMin(
int t)
const {
759IntegerValue SchedulingDemandHelper::DecomposedEnergyMin(
int t)
const {
762 for (
const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
764 return fixed_size * fixed_demand;
767 result = std::min(result, fixed_size * fixed_demand);
773IntegerValue SchedulingDemandHelper::SimpleEnergyMax(
int t)
const {
778IntegerValue SchedulingDemandHelper::DecomposedEnergyMax(
int t)
const {
781 for (
const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
782 if (assignment_.LiteralIsTrue(lit)) {
783 return fixed_size * fixed_demand;
785 if (assignment_.LiteralIsFalse(lit))
continue;
786 result = std::max(result, fixed_size * fixed_demand);
793 const int num_tasks = cached_energies_min_.size();
794 const bool is_at_level_zero = sat_solver_->CurrentDecisionLevel() == 0;
795 for (
int t = 0; t < num_tasks; ++t) {
797 if (is_at_level_zero) {
799 for (
int i = 0;
i < decomposed_energies_[t].size(); ++
i) {
800 if (assignment_.LiteralIsFalse(decomposed_energies_[t][
i].literal)) {
803 decomposed_energies_[t][new_size++] = decomposed_energies_[t][
i];
805 decomposed_energies_[t].resize(new_size);
808 cached_energies_min_[t] =
809 std::max(SimpleEnergyMin(t), DecomposedEnergyMin(t));
811 energy_is_quadratic_[t] =
812 decomposed_energies_[t].empty() && !demands_.empty() &&
813 !integer_trail_->IsFixed(demands_[t]) && !helper_->SizeIsFixed(t);
814 cached_energies_max_[t] =
815 std::min(SimpleEnergyMax(t), DecomposedEnergyMax(t));
823 DCHECK_LT(t, demands_.size());
824 return integer_trail_->LowerBound(demands_[t]);
828 DCHECK_LT(t, demands_.size());
829 return integer_trail_->UpperBound(demands_[t]);
833 return integer_trail_->IsFixed(demands_[t]);
837 if (helper_->IsAbsent(t))
return true;
838 if (value <
EnergyMin(t))
return helper_->PushTaskAbsence(t);
840 if (!decomposed_energies_[t].empty()) {
841 for (
const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
842 if (fixed_size * fixed_demand > value) {
845 if (assignment_.LiteralIsFalse(lit))
continue;
846 if (assignment_.LiteralIsTrue(lit)) {
848 if (helper_->PresenceLiteral(t) != lit) {
849 helper_->MutableLiteralReason()->push_back(lit.
Negated());
851 return helper_->PushTaskAbsence(t);
853 if (helper_->IsPresent(t)) {
855 DCHECK(!helper_->IsOptional(t) || helper_->PresenceLiteral(t) != lit);
856 helper_->AddPresenceReason(t);
857 if (!helper_->PushLiteral(lit.
Negated()))
return false;
863 VLOG(3) <<
"Cumulative energy missed propagation";
869 DCHECK_LT(t, demands_.size());
871 helper_->MutableIntegerReason()->push_back(
872 integer_trail_->LowerBoundAsLiteral(demands_[t].var));
877 IntegerValue min_demand) {
878 DCHECK_LT(t, demands_.size());
880 helper_->MutableIntegerReason()->push_back(
887 const IntegerValue value = cached_energies_min_[t];
888 if (DecomposedEnergyMin(t) >= value) {
889 auto* reason = helper_->MutableLiteralReason();
890 const int old_size = reason->size();
891 for (
const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
892 if (assignment_.LiteralIsTrue(lit)) {
893 reason->resize(old_size);
894 reason->push_back(lit.
Negated());
896 }
else if (fixed_size * fixed_demand < value &&
897 assignment_.LiteralIsFalse(lit)) {
898 reason->push_back(lit);
901 }
else if (SimpleEnergyMin(t) >= value) {
903 helper_->AddSizeMinReason(t);
909 if (helper_->IsPresent(t)) {
910 if (!decomposed_energies_[t].empty()) {
917 builder->
AddTerm(demands_[t], IntegerValue(1));
919 }
else if (!helper_->IsAbsent(t)) {
927 if (decomposed_energies_[index].empty())
return {};
928 if (sat_solver_->CurrentDecisionLevel() == 0) {
930 return decomposed_energies_[index];
934 std::vector<LiteralValueValue> result;
935 for (
const auto& e : decomposed_energies_[index]) {
936 if (assignment_.LiteralIsFalse(e.literal))
continue;
943 const std::vector<std::vector<LiteralValueValue>>& energies) {
944 DCHECK_EQ(energies.size(), helper_->NumTasks());
945 decomposed_energies_ = energies;
949 int t, IntegerValue window_start, IntegerValue window_end) {
951 helper_->StartMin(t), helper_->StartMax(t), helper_->EndMin(t),
952 helper_->EndMax(t), helper_->SizeMin(t),
DemandMin(t),
959 int t, IntegerValue window_start, IntegerValue window_end) {
960 const IntegerValue actual_energy_min =
962 if (actual_energy_min == 0)
return;
966 const IntegerValue start_max = helper_->StartMax(t);
967 const IntegerValue end_min = helper_->EndMin(t);
968 const IntegerValue min_overlap =
969 helper_->GetMinOverlap(t, window_start, window_end);
970 const IntegerValue simple_energy_min =
DemandMin(t) * min_overlap;
971 if (simple_energy_min == actual_energy_min) {
973 helper_->AddSizeMinReason(t);
974 helper_->AddStartMaxReason(t, start_max);
975 helper_->AddEndMinReason(t, end_min);
980 const IntegerValue start_min = helper_->StartMin(t);
981 const IntegerValue end_max = helper_->EndMax(t);
982 DCHECK(!decomposed_energies_[t].empty());
983 helper_->AddStartMinReason(t, start_min);
984 helper_->AddStartMaxReason(t, start_max);
985 helper_->AddEndMinReason(t, end_min);
986 helper_->AddEndMaxReason(t, end_max);
988 auto* literal_reason = helper_->MutableLiteralReason();
989 const int old_size = literal_reason->size();
991 DCHECK(!decomposed_energies_[t].empty());
992 for (
const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
994 if (assignment_.LiteralIsTrue(lit)) {
995 literal_reason->resize(old_size);
996 literal_reason->push_back(lit.
Negated());
999 if (assignment_.LiteralIsFalse(lit)) {
1000 const IntegerValue alt_em = std::max(end_min, start_min + fixed_size);
1001 const IntegerValue alt_sm = std::min(start_max, end_max - fixed_size);
1002 const IntegerValue energy_min =
1004 std::min({alt_em - window_start, window_end - alt_sm, fixed_size});
1005 if (energy_min >= actual_energy_min)
continue;
1006 literal_reason->push_back(lit);
1013 std::vector<IntegerVariable>* vars,
1016 for (
int t = 0; t < helper->
NumTasks(); ++t) {
1019 vars->push_back(helper->
Starts()[t].var);
1023 vars->push_back(helper->
Sizes()[t].var);
1027 vars->push_back(helper->
Ends()[t].var);
1037 vars->push_back(view);
1044 Model* model, std::vector<IntegerVariable>* vars) {
1047 if (!integer_trail->IsFixed(demand_expr)) {
1048 vars->push_back(demand_expr.var);
1053 for (
const auto& lit_val_val : product) {
1058 vars->push_back(view);
1062 if (!integer_trail->IsFixed(capacity)) {
1063 vars->push_back(capacity.
var);
void Clear(IndexType i)
Sets the bit at position i to 0.
void Resize(IndexType size)
void Set(IndexType i)
Sets the bit at position i to 1.
void SetPropagatorPriority(int id, int priority)
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
int Register(PropagatorInterface *propagator)
Registers a propagator and returns its unique ids.
ABSL_MUST_USE_RESULT bool LiteralOrNegationHasView(Literal lit, IntegerVariable *view=nullptr, bool *view_is_direct=nullptr) const
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
IntegerValue UpperBound(IntegerVariable i) const
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff=IntegerValue(1))
void AddTerm(IntegerVariable var, IntegerValue coeff)
T Add(std::function< T(Model *)> f)
Helper class to express a product as a linear constraint.
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
absl::Span< const TaskTime > TaskByIncreasingStartMin()
void AddReasonForBeingBefore(int before, int after)
Produces a relaxed reason for StartMax(before) < EndMin(after).
void AddStartMaxReason(int t, IntegerValue upper_bound)
ABSL_MUST_USE_RESULT bool IncreaseEndMin(int t, IntegerValue value)
IntegerValue ShiftedStartMin(int t) const
void WatchAllTasks(int id)
std::vector< IntegerLiteral > * MutableIntegerReason()
void RegisterWith(GenericLiteralWatcher *watcher)
absl::Span< const TaskTime > TaskByIncreasingNegatedStartMax()
bool SizeIsFixed(int t) const
void AddSizeMaxReason(int t, IntegerValue upper_bound)
IntegerValue StartMax(int t) const
bool PropagatePrecedence(int a, int b)
ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue value)
int NumTasks() const
Returns the number of task.
ABSL_MUST_USE_RESULT bool ReportConflict()
absl::Span< const AffineExpression > Sizes() const
ABSL_MUST_USE_RESULT bool PushLiteral(Literal l)
const std::vector< ProfileEvent > & GetEnergyProfile()
ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t)
bool IsPresent(int t) const
void SetTimeDirection(bool is_forward)
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t, IntegerLiteral lit)
Literal PresenceLiteral(int index) const
void AddSizeMinReason(int t)
absl::Span< const AffineExpression > Starts() const
void AddEndMaxReason(int t, IntegerValue upper_bound)
absl::Span< const AffineExpression > Ends() const
ABSL_MUST_USE_RESULT bool ResetFromSubset(const SchedulingConstraintHelper &other, absl::Span< const int > tasks)
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue value)
IntegerValue SizeMax(int t) const
void AddEndMinReason(int t, IntegerValue lower_bound)
IntegerValue StartMin(int t) const
void ClearReason()
Functions to clear and then set the current reason.
bool StartIsFixed(int t) const
SchedulingConstraintHelper(std::vector< AffineExpression > starts, std::vector< AffineExpression > ends, std::vector< AffineExpression > sizes, std::vector< LiteralIndex > reason_for_presence, Model *model)
IntegerValue SizeMin(int t) const
bool EndIsFixed(int t) const
absl::Span< const CachedTaskBounds > TaskByIncreasingShiftedStartMin()
absl::Span< const TaskTime > TaskByDecreasingEndMax()
ABSL_MUST_USE_RESULT bool SynchronizeAndSetTimeDirection(bool is_forward)
ABSL_MUST_USE_RESULT bool PushTaskPresence(int t)
IntegerValue EndMax(int t) const
bool IsAbsent(int t) const
IntegerValue EndMin(int t) const
bool IsOptional(int t) const
std::string TaskDebugString(int t) const
Returns a string with the current task bounds.
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
void ImportOtherReasons(const SchedulingConstraintHelper &other_helper)
IntegerValue GetCurrentMinDistanceBetweenTasks(int a, int b, bool add_reason_if_after=false)
IntegerValue GetMinOverlap(int t, IntegerValue start, IntegerValue end) const
std::vector< Literal > * MutableLiteralReason()
void AddStartMinReason(int t, IntegerValue lower_bound)
absl::Span< const TaskTime > TaskByIncreasingEndMin()
void AddDemandMinReason(int t)
std::vector< LiteralValueValue > FilteredDecomposedEnergy(int index)
bool DemandIsFixed(int t) const
bool CacheAllEnergyValues()
IntegerValue EnergyMinInWindow(int t, IntegerValue window_start, IntegerValue window_end)
const std::vector< std::vector< LiteralValueValue > > & DecomposedEnergies() const
void AddEnergyMinReason(int t)
void InitDecomposedEnergies()
void AddEnergyMinInWindowReason(int t, IntegerValue window_start, IntegerValue window_end)
IntegerValue DemandMax(int t) const
SchedulingDemandHelper(absl::Span< const AffineExpression > demands, SchedulingConstraintHelper *helper, Model *model)
void OverrideDecomposedEnergies(const std::vector< std::vector< LiteralValueValue > > &energies)
Visible for testing.
const std::vector< AffineExpression > & Demands() const
ABSL_MUST_USE_RESULT bool DecreaseEnergyMax(int t, IntegerValue value)
IntegerValue DemandMin(int t) const
ABSL_MUST_USE_RESULT bool AddLinearizedDemand(int t, LinearConstraintBuilder *builder) const
IntegerValue EnergyMin(int t) const
bool LiteralIsFalse(Literal literal) const
bool LiteralIsTrue(Literal literal) const
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
const LiteralIndex kNoLiteralIndex(-1)
std::function< int64_t(const Model &)> LowerBound(IntegerVariable v)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64_t ub)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
void AddIntegerVariableFromIntervals(const SchedulingConstraintHelper *helper, Model *model, std::vector< IntegerVariable > *vars, int mask)
void AppendVariablesFromCapacityAndDemands(const AffineExpression &capacity, SchedulingDemandHelper *demands_helper, Model *model, std::vector< IntegerVariable > *vars)
void AddWeightedSumLowerOrEqual(absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const int64_t > coefficients, int64_t upper_bound, Model *model)
enforcement_literals => sum <= upper_bound
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64_t lb)
IntegerValue CapProdI(IntegerValue a, IntegerValue b)
Overflows and saturated arithmetic.
IntegerValue ComputeEnergyMinInWindow(IntegerValue start_min, IntegerValue start_max, IntegerValue end_min, IntegerValue end_max, IntegerValue size_min, IntegerValue demand_min, absl::Span< const LiteralValueValue > filtered_energy, IntegerValue window_start, IntegerValue window_end)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
void IncrementalSort(int max_comparisons, Iterator begin, Iterator end, Compare comp=Compare{}, bool is_stable=false)
ClosedInterval::Iterator begin(ClosedInterval interval)
IntegerLiteral Negated() const
The negation of x >= bound is x <= bound - 1.
static LinearExpression2 Difference(IntegerVariable v1, IntegerVariable v2)
Build (v1 - v2)