63 LiteralIndex is_present,
64 bool add_linear_relation) {
66 const IntervalVariable
i(starts_.size());
67 starts_.push_back(start);
69 sizes_.push_back(size);
70 is_present_.push_back(is_present);
72 std::vector<Literal> enforcement_literals;
74 enforcement_literals.push_back(
Literal(is_present));
77 if (add_linear_relation) {
109 auto it = disjunctive_precedences_.find({a,
b});
110 if (it != disjunctive_precedences_.end())
return it->second.Index();
112 std::vector<Literal> enforcement_literals;
114 enforcement_literals.push_back(a.
is_present.value());
116 if (
b.is_present.has_value()) {
117 enforcement_literals.push_back(
b.is_present.value());
120 auto remove_fixed = [assignment =
121 &assignment_](std::vector<Literal>& literals) {
123 for (
const Literal l : literals) {
126 if (assignment->LiteralIsTrue(l))
continue;
127 if (assignment->LiteralIsFalse(l))
return false;
128 literals[new_size++] = l;
130 literals.resize(new_size);
134 if (sat_solver_->CurrentDecisionLevel() == 0) {
140 if (integer_trail_->UpperBound(a.
start) < integer_trail_->LowerBound(
b.end)) {
141 if (sat_solver_->CurrentDecisionLevel() == 0) {
149 if (integer_trail_->UpperBound(
b.start) < integer_trail_->LowerBound(a.
end)) {
150 if (sat_solver_->CurrentDecisionLevel() == 0) {
158 if (relations_maps_->GetLevelZeroPrecedenceStatus(a.
end,
b.start) ==
160 relations_maps_->GetLevelZeroPrecedenceStatus(
b.end, a.
start) ==
177 const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
179 disjunctive_precedences_.insert({{a,
b}, a_before_b});
180 disjunctive_precedences_.insert({{
b, a}, a_before_b.
Negated()});
183 if (enforcement_literals.empty()) {
184 relations_maps_->AddReifiedPrecedenceIfNonTrivial(a_before_b, a.
end,
186 relations_maps_->AddReifiedPrecedenceIfNonTrivial(a_before_b.
Negated(),
190 enforcement_literals.push_back(a_before_b);
192 enforcement_literals.pop_back();
194 enforcement_literals.push_back(a_before_b.
Negated());
196 enforcement_literals.pop_back();
200 if (sat_solver_->CurrentDecisionLevel() == 0) {
206 for (
const Literal l : enforcement_literals) {
207 implications_->AddBinaryClause(l, a_before_b);
215 const LiteralIndex index = relations_maps_->GetReifiedPrecedence(x, y);
220 if (relations_maps_->GetLevelZeroPrecedenceStatus(x, y) !=
226 const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
228 relations_maps_->AddReifiedPrecedenceIfNonTrivial(x_before_y, x, y);
259 const std::vector<IntervalVariable>& variables,
260 bool register_as_disjunctive_helper) {
261 const auto it = helper_repository_.find(variables);
262 if (it != helper_repository_.end())
return it->second;
263 std::vector<AffineExpression> starts;
264 std::vector<AffineExpression> ends;
265 std::vector<AffineExpression> sizes;
266 std::vector<LiteralIndex> reason_for_presence;
268 const int num_variables = variables.size();
269 starts.reserve(num_variables);
270 ends.reserve(num_variables);
271 sizes.reserve(num_variables);
272 reason_for_presence.reserve(num_variables);
274 for (
const IntervalVariable
i : variables) {
280 sizes.push_back(
Size(
i));
281 starts.push_back(
Start(
i));
282 ends.push_back(
End(
i));
286 std::move(starts), std::move(ends), std::move(sizes),
287 std::move(reason_for_presence), model_);
289 helper_repository_[variables] = helper;
290 model_->TakeOwnership(helper);
291 if (register_as_disjunctive_helper) {
292 disjunctive_helpers_.push_back(helper);
298 const std::vector<IntervalVariable>& x_variables,
299 const std::vector<IntervalVariable>& y_variables) {
301 no_overlap_2d_helper_repository_.find({x_variables, y_variables});
302 if (it != no_overlap_2d_helper_repository_.end())
return it->second;
304 std::vector<AffineExpression> x_starts;
305 std::vector<AffineExpression> x_ends;
306 std::vector<AffineExpression> x_sizes;
307 std::vector<LiteralIndex> x_reason_for_presence;
309 for (
const IntervalVariable
i : x_variables) {
315 x_sizes.push_back(
Size(
i));
316 x_starts.push_back(
Start(
i));
317 x_ends.push_back(
End(
i));
319 std::vector<AffineExpression> y_starts;
320 std::vector<AffineExpression> y_ends;
321 std::vector<AffineExpression> y_sizes;
322 std::vector<LiteralIndex> y_reason_for_presence;
324 for (
const IntervalVariable
i : y_variables) {
330 y_sizes.push_back(
Size(
i));
331 y_starts.push_back(
Start(
i));
332 y_ends.push_back(
End(
i));
335 std::move(x_starts), std::move(x_ends), std::move(x_sizes),
336 std::move(x_reason_for_presence), std::move(y_starts), std::move(y_ends),
337 std::move(y_sizes), std::move(y_reason_for_presence), model_);
339 no_overlap_2d_helper_repository_[{x_variables, y_variables}] = helper;
340 model_->TakeOwnership(helper);
346 absl::Span<const AffineExpression> demands) {
347 const std::pair<SchedulingConstraintHelper*, std::vector<AffineExpression>>
349 std::vector<AffineExpression>(demands.begin(), demands.end())};
350 const auto it = demand_helper_repository_.find(key);
351 if (it != demand_helper_repository_.end())
return it->second;
355 model_->TakeOwnership(demand_helper);
356 demand_helper_repository_[key] = demand_helper;
357 return demand_helper;