1 #include <chuffed/core/propagator.h>
2 #include <list>
3 #include <queue>
4 #include <set>
5 #include <iostream>
6
7 using namespace std;
8
9 #define CUMUVERB 0
10
11 // Data types for the Chuffed solver
12 #define CUMU_ARR_INTVAR vec<IntVar*>
13 #define CUMU_MATRIX_INT vec<vec<int> >
14 #define CUMU_ARR_INT vec<int>
15 #define CUMU_INTVAR IntVar*
16 #define CUMU_INT int
17 #define CUMU_BOOL bool
18 #define CUMU_GETMIN(x) x.getMin()
19 #define CUMU_GETMAX(x) x.getMax()
20 #define CUMU_GETMAX0(x) x.getMax()
21 #define CUMU_PT_GETMIN(x) x->getMin()
22 #define CUMU_PT_GETMAX(x) x->getMax()
23 #define CUMU_PT_GETMIN0(x) x->getMin0()
24 #define CUMU_PT_GETMAX0(x) x->getMax0()
25 #define CUMU_PT_ISFIXED(x) x->isFixed()
26
27 #define CUMU_MEMCHECK(ptr) do { if (ptr == NULL) CHUFFED_ERROR("Out of memory!\n"); } while(0)
28
29
30 class CumulativeCalProp : public Propagator {
31 enum ExplDeg {
32 ED_NAIVE,
33 ED_NORMAL,
34 ED_LIFT
35 };
36 // Task-Duration tuple
37 struct TaskDur {
38 int task;
39 int dur_in;
TaskDurCumulativeCalProp::TaskDur40 TaskDur(int _task, int _dur_in) : task(_task), dur_in(_dur_in) {}
41 };
42 // TTEF Update Structure
43 struct TTEFUpdate {
44 int task;
45 int bound_new;
46 int tw_begin;
47 int tw_end;
48 bool is_lb_update;
TTEFUpdateCumulativeCalProp::TTEFUpdate49 TTEFUpdate(int _t, int _n, int _b, int _e, int _l) : task(_t), bound_new(_n),
50 tw_begin(_b), tw_end(_e), is_lb_update(_l) {}
51 };
52 // Compulsory Part of a Task
53 struct CompPart {
54 CUMU_INT begin;
55 CUMU_INT end;
56 CUMU_INT level;
57 CUMU_INT task;
CompPartCumulativeCalProp::CompPart58 CompPart(CUMU_INT b, CUMU_INT e, CUMU_INT l, CUMU_INT t)
59 : begin(b), end(e), level(l), task(t) {}
60 };
61
62 // Resource profile of the resource
63 struct ProfilePart {
64 CUMU_INT begin;
65 CUMU_INT end;
66 CUMU_INT level;
67 set<CUMU_INT> tasks;
ProfilePartCumulativeCalProp::ProfilePart68 ProfilePart(CUMU_INT b, CUMU_INT e, CUMU_INT l, CUMU_INT t)
69 : begin(b), end(e), level(l) { tasks.insert(t); };
ProfilePartCumulativeCalProp::ProfilePart70 ProfilePart() : begin(0), end(0), level(0) {}
71 };
72
73 enum ProfileChange { PROFINC, PROFDEC };
74 struct ProfileChangePt {
75 CUMU_INT time;
76 ProfileChange change;
ProfileChangePtCumulativeCalProp::ProfileChangePt77 ProfileChangePt(CUMU_INT t, ProfileChange c) : time(t), change(c) {}
78 };
79
80 Tint last_unfixed;
81
82 public:
83 string name; // Name of the cumulative constraint for printing statistics
84
85 // Constant Data
86 CUMU_ARR_INTVAR start; // Start time variables of the tasks
87 CUMU_ARR_INTVAR dur; // Durations of the tasks
88 CUMU_ARR_INTVAR usage; // Resource usage of the tasks
89 CUMU_INTVAR limit; // Resource capacity of the resource
90 CUMU_MATRIX_INT calendar2; //Different calendars of the project
91 CUMU_ARR_INT taskCalendar; //Number of calendar that task depends on
92 CUMU_INT rho; //=1 if resource stays engaged, =0 otherwise
93 CUMU_INT resCalendar; //TTEF_cal: Number of calendar that resource depends on
94 int ** calendar;
95 int ** workingPeriods;
96
97 const int minTime; // Minimal time in the calendar
98 const int maxTime; // Maximal time in the calendar
99
100
101 // Options
102 const CUMU_BOOL idem; // Whether the cumulative propagator should be idempotent
103 const CUMU_BOOL tt_check;
104 CUMU_BOOL tt_filt; // Timetabling bounds filtering of the start times
105 CUMU_BOOL ttef_check; // Timetabling-edge-finding consistency check
106 CUMU_BOOL ttef_filt; // Timetabling-edge-finding filtering of the start times
107 const CUMU_BOOL tteef_filt; // Opportunistic timetabling-extended-edge-finding filtering of the start times
108 long ttef_prop_factor;
109
110 ExplDeg ttef_expl_deg;
111
112 // Counters
113 long nb_tt_incons; // Number of timetabling inconsistencies
114 long nb_tt_filt; // Number of timetabling propagations
115 long nb_ttef_incons; // Number of timetabling-edge-finding inconsistencies
116 long nb_ttef_filt; // Number of timetabling-edge-finding propagations
117 long nb_prop_calls;
118 long nb_ttefc_calls;
119 long nb_ttefc_steps;
120 long nb_ttef_lb_calls;
121 long nb_ttef_ub_calls;
122
123 // Parameters
124 CUMU_BOOL bound_update;
125
126 // Structures
127 CUMU_ARR_INT task_id; // Unfixed tasks on the left-hand side and fixed tasks on the right-hand size
128 int * task_id_est;
129 int * task_id_lct;
130 int * tt_after_est;
131 int * tt_after_lct;
132 int * new_est;
133 int * new_lct;
134 int tt_profile_size;
135 struct ProfilePart * tt_profile;
136
137 int * est_2;
138 int * lst_2;
139 int * ect_2;
140 int * lct_2;
141 int * min_energy2;
142 Tint * min_energy2_global;
143 int * free_energy2;
144
145 // Inline functions
146 struct SortEstAsc {
147 CumulativeCalProp *p;
operator ()CumulativeCalProp::SortEstAsc148 bool operator() (int i, int j) { return p->est_2[i] < p->est_2[j]; }
SortEstAscCumulativeCalProp::SortEstAsc149 SortEstAsc(CumulativeCalProp *_p) : p(_p) {}
150 } sort_est_asc;
151
152 struct SortLctAsc {
153 CumulativeCalProp *p;
operator ()CumulativeCalProp::SortLctAsc154 bool operator() (int i, int j) { return p->lct_2[i] < p->lct_2[j]; }
SortLctAscCumulativeCalProp::SortLctAsc155 SortLctAsc(CumulativeCalProp *_p) : p(_p) {}
156 } sort_lct_asc;
157
158 // Constructor
CumulativeCalProp(CUMU_ARR_INTVAR & _start,CUMU_ARR_INTVAR & _dur,CUMU_ARR_INTVAR & _usage,CUMU_INTVAR _limit,CUMU_MATRIX_INT & _cal,CUMU_ARR_INT & _taskCal,CUMU_INT _rho,CUMU_INT _resCalendar,list<string> opt)159 CumulativeCalProp(CUMU_ARR_INTVAR & _start, CUMU_ARR_INTVAR & _dur, CUMU_ARR_INTVAR & _usage,
160 CUMU_INTVAR _limit, CUMU_MATRIX_INT & _cal, CUMU_ARR_INT & _taskCal, CUMU_INT _rho, CUMU_INT _resCalendar,
161 list<string> opt)
162 : name(""), start(_start), dur(_dur), usage(_usage), limit(_limit),
163 calendar2(_cal), taskCalendar(_taskCal), rho(_rho), resCalendar(_resCalendar),
164 minTime(0), maxTime(calendar2[0].size() - 1),
165 idem(false), tt_check(true), tt_filt(true), ttef_check(true), ttef_filt(true), tteef_filt(false),
166 ttef_prop_factor(100),
167 nb_tt_incons(0), nb_tt_filt(0), nb_ttef_incons(0), nb_ttef_filt(0),
168 nb_prop_calls(0), nb_ttefc_calls(0), nb_ttefc_steps(0), nb_ttef_lb_calls(0), nb_ttef_ub_calls(0),
169 bound_update(false),
170 sort_est_asc(this), sort_lct_asc(this)
171 {
172 // Some checks
173 rassert(!tteef_filt || ttef_filt);
174
175 // Overriding option defaults
176 for (list<string>::iterator it = opt.begin(); it != opt.end(); it++) {
177 if (!(*it).compare("tt_filt_on"))
178 tt_filt = true;
179 else if (!(*it).compare("tt_filt_off"))
180 tt_filt = false;
181 if (!(*it).compare("ttef_check_on"))
182 ttef_check = true;
183 else if (!(*it).compare("ttef_check_off"))
184 ttef_check = false;
185 if (!(*it).compare("ttef_filt_on"))
186 ttef_filt = true;
187 else if (!(*it).compare("ttef_filt_off"))
188 ttef_filt = false;
189 else if ((*it).find("__name__") == 0)
190 name = (*it).substr(8);
191 }
192
193 // Creating a copy of the calendars
194 calendar = (int **) malloc(calendar2.size() * sizeof(int *));
195 for(int i = 0; i < calendar2.size(); i++){
196 calendar[i] = (int *) malloc(calendar2[0].size() * sizeof(int));
197 }
198
199 for(int i = 0; i < calendar2.size(); i++){
200 for(int j = 0; j < calendar2[0].size(); j++){
201 calendar[i][j]=calendar2[i][j];
202 }
203 }
204
205 // Memory allocation for the working periods
206 workingPeriods = (int **) malloc(calendar2.size() * sizeof(int *));
207 CUMU_MEMCHECK(workingPeriods);
208 for(int i = 0; i < calendar2.size(); i++){
209 workingPeriods[i] = (int *) malloc(calendar2[0].size() * sizeof(int));
210 CUMU_MEMCHECK(workingPeriods[i]);
211 }
212
213 // Initialisation of the working periods
214 for(int i = 0; i < calendar2.size(); i++){
215 workingPeriods[i][calendar2[0].size()-1] = calendar[i][calendar2[0].size()-1];
216 for(int j = calendar2[0].size()-2; j >= 0; j--){
217 workingPeriods[i][j] = workingPeriods[i][j+1] + calendar[i][j];
218 }
219 }
220
221 // Explanation options
222 //ttef_expl_deg = ED_NAIVE;
223 //ttef_expl_deg = ED_NORMAL; // TODO Not adjusted to calendars yet
224 ttef_expl_deg = ED_LIFT;
225
226 // Allocation of the memory
227 tt_profile = new ProfilePart[calendar2[0].size()]; //[2 * start.size()];
228 tt_profile_size = 0;
229
230 // Memory allocation of the core structures
231 est_2 = (int *) malloc(start.size() * sizeof(int));
232 lst_2 = (int *) malloc(start.size() * sizeof(int));
233 ect_2 = (int *) malloc(start.size() * sizeof(int));
234 lct_2 = (int *) malloc(start.size() * sizeof(int));
235
236 // Memory check
237 CUMU_MEMCHECK(est_2);
238 CUMU_MEMCHECK(lst_2);
239 CUMU_MEMCHECK(ect_2);
240 CUMU_MEMCHECK(lct_2);
241
242 // Allocating memory required by the TTEF inconsistency check or
243 // filtering algorithm
244 if (ttef_check || ttef_filt) {
245 // Memory allocation
246 task_id_est = (int *) malloc(start.size() * sizeof(int));
247 task_id_lct = (int *) malloc(start.size() * sizeof(int));
248 tt_after_est = (int *) malloc(start.size() * sizeof(int));
249 tt_after_lct = (int *) malloc(start.size() * sizeof(int));
250 min_energy2 = (int *) malloc(start.size() * sizeof(int));
251 min_energy2_global = (Tint *) malloc(start.size() * sizeof(Tint));
252 free_energy2 = (int *) malloc(start.size() * sizeof(int));
253
254 // Memory check
255 CUMU_MEMCHECK(task_id_est);
256 CUMU_MEMCHECK(task_id_lct);
257 CUMU_MEMCHECK(tt_after_est);
258 CUMU_MEMCHECK(tt_after_lct);
259 CUMU_MEMCHECK(min_energy2);
260 CUMU_MEMCHECK(min_energy2_global);
261 CUMU_MEMCHECK(free_energy2);
262
263 // Allocating memory only required by the TTEF filtering
264 // algorithms
265 if (ttef_filt) {
266 // Memory allocation
267 new_est = (int *) malloc(start.size() * sizeof(int));
268 new_lct = (int *) malloc(start.size() * sizeof(int));
269
270 // Memory check
271 CUMU_MEMCHECK(new_est);
272 CUMU_MEMCHECK(new_lct);
273 } else {
274 new_est = NULL;
275 new_lct = NULL;
276 }
277
278 // Initialisation of some arrays
279 for (int i = 0; i < start.size(); i++)
280 min_energy2_global[i] = min_dur(i);
281 } else {
282 task_id_est = NULL;
283 task_id_lct = NULL;
284 tt_after_est = NULL;
285 tt_after_lct = NULL;
286 min_energy2 = NULL;
287 min_energy2_global = NULL;
288 free_energy2 = NULL;
289 }
290
291 // Priority of the propagator
292 priority = 3;
293
294 #if CUMUVERB>1
295 fprintf(stderr, "\tCumulative with n = %d\n", start.size());
296 #endif
297 // Attach to var events
298 for (int i = 0; i < start.size(); i++) {
299 #if CUMUVERB>1
300 fprintf(stderr, "\t%d: %p\n", i, start[i]);
301 #endif
302 start[i]->attach(this, i, EVENT_LU);
303 if (min_dur(i) < max_dur(i)) dur[i]->attach(this, i, EVENT_LF);
304 if (min_usage(i) < max_usage(i)) usage[i]->attach(this, i, EVENT_LF);
305 }
306 limit->attach(this, start.size(), EVENT_UF);
307
308 for (int i = 0; i < start.size(); i++) {
309 task_id.push(i);
310 }
311 last_unfixed = start.size() - 1;
312 }
313
314 // Statistics
printStats()315 void printStats() {
316 fprintf(stderr, "%% Cumulative propagator with calendars statistics");
317 if (name != "")
318 cerr << " for " << name;
319 fprintf(stderr, ":\n");
320 fprintf(stderr, "%%\t#TT incons.: %ld\n", nb_tt_incons);
321 if (tt_filt)
322 fprintf(stderr, "%%\t#TT prop.: %ld\n", nb_tt_filt);
323 if (ttef_check || ttef_filt)
324 fprintf(stderr, "%%\t#TTEF incons.: %ld\n", nb_ttef_incons);
325 if (ttef_check && !ttef_filt) {
326 fprintf(stderr, "%%\t#TTEF calls: %ld\n", nb_ttefc_calls);
327 fprintf(stderr, "%%\t#TTEF cons. steps: %ld\n", nb_ttefc_steps);
328 }
329 if (ttef_filt) {
330 fprintf(stderr, "%%\t#TTEF prop.: %ld\n", nb_ttef_filt);
331 fprintf(stderr, "%%\t#TTEF LB calls: %ld\n", nb_ttef_lb_calls);
332 fprintf(stderr, "%%\t#TTEF UB calls: %ld\n", nb_ttef_ub_calls);
333 }
334 }
335
336
337 /**
338 * Retrieval of parameters
339 **/
340
341 int
getEndTimeForStartTime(const int i,const int start,const int duration)342 getEndTimeForStartTime(const int i, const int start, const int duration) {
343 const int cal_idx = taskCalendar[i] - 1;
344 int end = start + duration;
345 if (end <= maxTime) {
346 int workDays;
347 do {
348 workDays = workingPeriods[cal_idx][start] - workingPeriods[cal_idx][end];
349 end += duration - workDays;
350 } while (workDays < duration && end <= maxTime);
351 assert(workDays == duration || end > maxTime);
352 }
353 if (end > maxTime) {
354 end = maxTime + duration - (workingPeriods[cal_idx][start] - workingPeriods[cal_idx][maxTime]);
355 }
356 return end;
357 }
358
359 int
getStartTimeForEndTime(const int i,const int end,const int duration)360 getStartTimeForEndTime(const int i, const int end, const int duration) {
361 const int cal_idx = taskCalendar[i] - 1;
362 int start = end - duration;
363 if (start >= minTime) {
364 int workDays;
365 do {
366 workDays = workingPeriods[cal_idx][start] - workingPeriods[cal_idx][end];
367 start -= duration - workDays;
368 } while (workDays < duration && start >= minTime);
369 assert(workDays == duration || start < minTime);
370 }
371 if (start < minTime) {
372 start = minTime - duration + (workingPeriods[cal_idx][minTime] - workingPeriods[cal_idx][end]);
373 }
374 return start;
375 }
376
377 void
retrieveCoreParameters(int i)378 retrieveCoreParameters(int i) {
379 // Earliest start time
380 est_2[i] = CUMU_PT_GETMIN(start[i]);
381 // Latest start time
382 lst_2[i] = CUMU_PT_GETMAX(start[i]);
383 // Earliest completion time
384 const int duration = CUMU_PT_GETMIN(dur[i]);
385 ect_2[i] = getEndTimeForStartTime(i, est_2[i], duration);
386 // Latest completion time
387 lct_2[i] = getEndTimeForStartTime(i, lst_2[i], duration);
388 }
389
390 int
retrieveMinEnergy(const int i)391 retrieveMinEnergy(const int i) {
392 int minEn = 0;
393 if (rho == 0) {
394 // Resource is released
395 return minEn = min_usage(i) * min_dur(i);
396 }
397 assert(rho == 1);
398 // Resource stays engaged
399 const int duration = min_dur(i);
400 const int cal_idx = taskCalendar[i] - 1;
401 const int ls = lst_2[i];
402 // Calculate distance when task starts as earliest as possible
403 int end = est_2[i] + duration;
404 int workDays;
405 int distance;
406 do {
407 workDays = workingPeriods[cal_idx][est_2[i]] - workingPeriods[cal_idx][end];
408 end += duration - workDays;
409 } while (workDays < duration);
410 assert(workDays == duration);
411 distance = end - est_2[i];
412 // Calculate minimal distance
413 for (int time = est_2[i] + 1; time <= ls && distance > min_energy2_global[i]; time++) {
414 if (calendar[cal_idx][time - 1] == 1)
415 workDays--;
416 while (workDays < duration) {
417 if (calendar[cal_idx][end] == 1)
418 workDays++;
419 end++;
420 }
421 assert(workDays == duration);
422 distance = min(distance, end - time);
423 }
424 if (distance > min_energy2_global[i])
425 min_energy2_global[i] = distance;
426 return min_usage(i) * distance;
427 }
428
429 int
retrieveFreeEnergy(const int i)430 retrieveFreeEnergy(const int i) {
431 if (rho == 1) {
432 // Resource stays engaged
433 return (min_energy2[i] - min_usage(i) * max(0, ect_2[i] - lst_2[i]));
434 } else {
435 // Resource is released
436 int workDays = workingPeriods[taskCalendar[i]-1][lst_2[i]] - workingPeriods[taskCalendar[i]-1][ect_2[i]];
437 return (min_energy2[i] - min_usage(i) * max(0, workDays));
438 }
439 }
440
441 void
retrieveEnergyParameters(const int i)442 retrieveEnergyParameters(const int i) {
443 // NOTE it is assumpted that the arrays est_2, lst_2, ect_2, and lct_2 are up to date!
444 // Minimal required energy for executing the task
445 min_energy2[i] = retrieveMinEnergy(i);
446 // Free energy
447 free_energy2[i] = retrieveFreeEnergy(i);
448 }
449
450 /**
451 * Inline function for parameters of tasks
452 **/
453 // Earliest start time of task i
454 inline CUMU_INT
est(CUMU_INT i)455 est(CUMU_INT i) { return CUMU_PT_GETMIN(start[i]); }
456 // Latest start time of task i
457 inline CUMU_INT
lst(CUMU_INT i)458 lst(CUMU_INT i) { return CUMU_PT_GETMAX(start[i]); }
459 // Earliest completion time of task i
460 inline CUMU_INT
ect(CUMU_INT i)461 ect(CUMU_INT i) {
462 int t = CUMU_PT_GETMIN(start[i]);
463 int j = 0;
464 while(j < CUMU_PT_GETMIN(dur[i])){
465 if(calendar[taskCalendar[i]-1][t]==1) { j++; }
466 t++;
467 }
468 return t; }
469 // Latest completion time of task i
470 inline CUMU_INT
lct(CUMU_INT i)471 lct(CUMU_INT i) {
472 int t = CUMU_PT_GETMAX(start[i]);
473 int j = 0;
474 while(j < CUMU_PT_GETMIN(dur[i])){
475 if(calendar[taskCalendar[i]-1][t]==1) { j++; }
476 t++;
477 }
478 return t; }
479 // Minimal resource usage of task i
480 inline CUMU_INT
min_usage(CUMU_INT i)481 min_usage(CUMU_INT i) { return CUMU_PT_GETMIN(usage[i]); }
482 // Minimal energy of task i
483 // TTEF_cal: We could consider min_execution_time here, but computation is expensive
484 inline CUMU_INT
min_energy(CUMU_INT i)485 min_energy(CUMU_INT i) {
486 if(rho == 0) { // TTEF_cal: resource is used exactly for p_i time units
487 return min_usage(i) * min_dur(i);
488 }else{ // TTEF_cal: resource stays engaged during breaks / could be used more than p_i time units
489 int duration = min_dur(i);
490 int t = est(i);
491 int ls = lst(i);
492 int distance = lct(i) - t;
493 int j, tau, next;
494 while(t <= ls) {
495 tau = t;
496 j = 0;
497 next = ls+1;
498 while(j < duration){
499 if(calendar[taskCalendar[i]-1][t]==1) {
500 j++;
501 }else if(calendar[taskCalendar[i]-1][t+1]==1) {
502 next = min(next, t+1);
503 }
504 t++;
505 }
506 distance = min(distance, t - tau);
507 if(distance == duration) return min_usage(i) * duration;
508 t = next;
509 }
510 return min_usage(i) * distance;
511 }
512 }
513 // Free Energy
514 inline CUMU_INT
free_energy(CUMU_INT i)515 free_energy(CUMU_INT i) {
516 if (rho == 1) {
517 return (min_energy(i) - min_usage(i) * max(0, ect(i) - lst(i)));
518 } else {
519 int breaks = ect(i) - lst(i) - (workingPeriods[taskCalendar[i]-1][lst(i)] - workingPeriods[taskCalendar[i]-1][ect(i)]);
520 return (min_energy(i) - min_usage(i) * max(0, ect(i) - lst(i) - breaks));
521 }
522 }
523
524 /**
525 * Inline functions for receiving the minimum and maximum of integer
526 * variables
527 **/
528 inline CUMU_INT
min_start0(CUMU_INT i)529 min_start0(CUMU_INT i) { return CUMU_PT_GETMIN0(start[i]); }
530 inline CUMU_INT
max_start0(CUMU_INT i)531 max_start0(CUMU_INT i) { return CUMU_PT_GETMAX0(start[i]); }
532 inline CUMU_INT
min_dur(CUMU_INT i)533 min_dur(CUMU_INT i) { return CUMU_PT_GETMIN(dur[i]); }
534 inline CUMU_INT
max_dur(CUMU_INT i)535 max_dur(CUMU_INT i) { return CUMU_PT_GETMAX(dur[i]); }
536 inline CUMU_INT
min_dur0(CUMU_INT i)537 min_dur0(CUMU_INT i) { return CUMU_PT_GETMIN0(dur[i]); }
538 inline CUMU_INT
max_usage(CUMU_INT i)539 max_usage(CUMU_INT i) { return CUMU_PT_GETMAX(usage[i]); }
540 inline CUMU_INT
min_usage0(CUMU_INT i)541 min_usage0(CUMU_INT i) { return CUMU_PT_GETMIN0(usage[i]); }
542
543 inline CUMU_INT
min_limit()544 min_limit() { return CUMU_PT_GETMIN(limit); }
545 inline CUMU_INT
max_limit()546 max_limit() { return CUMU_PT_GETMAX(limit); }
547 inline CUMU_INT
max_limit0()548 max_limit0() { return CUMU_PT_GETMAX0(limit); }
549
550 // TTEF Propagator
551 // TTEF_cal: errors occurred when using shift_in function etc.; realized it with an integer shift_in
552 // if shift_in == 1 right shift is used; if shift_in == 2 left shift is used
553 void
554 ttef_initialise_parameters();
555 bool
556 ttef_consistency_check(int shift_in);
557 bool
558 ttef_bounds_propagation(int shift_in1, int shift_in2);
559 bool
560 ttef_bounds_propagation_lb(int shift_in, std::queue<TTEFUpdate> & update_queue);
561 bool
562 ttef_bounds_propagation_ub(int shift_in, std::queue<TTEFUpdate> & update_queue);
563 void
564 tteef_bounds_propagation_lb(const int begin, const int end, const int en_avail, const int j,
565 std::queue<TTEFUpdate> & update_queue);
566 void
567 tteef_bounds_propagation_ub(const int begin, const int end, const int en_avail, const int j,
568 std::queue<TTEFUpdate> & update_queue);
569 int
570 ttef_get_new_start_time(const int begin, const int end, const int task, const int min_wdays_in);
571 int
572 ttef_get_new_end_time(const int begin, const int end, const int task, const int min_wdays_in);
573 bool
574 ttef_update_bounds(int shift_in,
575 std::queue<TTEFUpdate> & queue_update);
576 void
577 ttef_explanation_for_update_lb(int shift_in, const int begin, const int end, const int task,
578 int & bound, vec<Lit> & expl);
579 void
580 ttef_explanation_for_update_ub(int shift_in, const int begin, const int end, const int task,
581 int & bound, vec<Lit> & expl);
582
583 int
584 ttef_retrieve_tasks(int shift_in,
585 int begin, int end, int fb_id, list<TaskDur> & tasks_tw, list<TaskDur> & tasks_cp);
586
587 // TTEF Generation of explanations
588 // TTEF_cal: consider breaks between begin and end
589 void
590 ttef_analyse_limit_and_tasks(const int begin, const int end, const int breaks, list<TaskDur> & tasks_tw,
591 list<TaskDur> & tasks_cp, int & en_lift, vec<Lit> & expl);
592 void
593 ttef_analyse_tasks(const int begin, const int end, list<TaskDur> & tasks, int & en_lift, vec<Lit> & expl);
594 int
595 ttef_analyse_tasks_left_shift(const int begin, const int end, const int dur_in, const int task, const int max_dur_lift, int & last_dur);
596 int
597 ttef_analyse_tasks_right_shift(const int begin, const int end, const int dur_in, const int task, const int max_dur_lift, int & last_dur);
598 bool
599 ttef_analyse_tasks_check_expl_lb(const int begin, const int end, const int task, const int dur_in, const int expl_ub);
600 bool
601 ttef_analyse_tasks_check_expl_ub(const int begin, const int end, const int task, const int dur_in, const int expl_ub);
602
603 inline bool
604 is_intersecting(const int begin1, const int end1, const int begin2, const int end2);
605
606
607 inline int
get_free_dur_right_shift2(const int tw_begin,const int tw_end,const int task)608 get_free_dur_right_shift2(const int tw_begin, const int tw_end, const int task)
609 {
610 if (tw_begin > est_2[task] || tw_end <= lst_2[task] || tw_end <= ect_2[task])
611 return 0;
612 const int free_lst = (lst_2[task] < ect_2[task] ? ect_2[task] : lst_2[task]);
613 if (rho == 0) {
614 // Resource is released
615 const int cal_idx = taskCalendar[task] - 1;
616 const int workingDays = workingPeriods[cal_idx][free_lst] - workingPeriods[cal_idx][tw_end];
617 return workingDays;
618 } else {
619 // Resource stays engaged
620 return (tw_end - free_lst);
621 }
622 }
623
624 inline int
get_free_dur_left_shift2(const int tw_begin,const int tw_end,const int task)625 get_free_dur_left_shift2(const int tw_begin, const int tw_end, const int task)
626 {
627 if (tw_end < lct_2[task] || tw_begin >= ect_2[task] || tw_begin >= lst_2[task])
628 return 0;
629 const int free_ect = (lst_2[task] < ect_2[task] ? lst_2[task] : ect_2[task]);
630 if (rho == 0) {
631 // Resource is released
632 const int * wPeriods = workingPeriods[taskCalendar[task] - 1];
633 const int workingDays = wPeriods[tw_begin] - wPeriods[free_ect];
634 return workingDays;
635 } else {
636 // Resource stays engaged
637 return (free_ect - tw_begin);
638 }
639 }
640
641 inline int
get_no_shift(const int tw_begin,const int tw_end,const int est,const int ect,const int lst,const int lct,const int dur_fixed_in,const int task)642 get_no_shift(const int tw_begin, const int tw_end, const int est, const int ect,
643 const int lst, const int lct, const int dur_fixed_in, const int task)
644 {
645 return 0;
646 }
647
648 // Cumulative Propagator
649 CUMU_BOOL
propagate()650 propagate() {
651 #if CUMUVERB>1
652 fprintf(stderr, "Entering cumulative propagation\n");
653 #endif
654 assert(last_unfixed >= 0);
655 // Retrieval of the task's core data and updating
656 // the fixed-task array
657 int new_unfixed = last_unfixed;
658 int tw_begin = maxTime;
659 int tw_end = minTime;
660 for (int ii = new_unfixed; ii >= 0; ii--) {
661 const int i = task_id[ii];
662 // Retrieve core data (est, lst, ect, lct)
663 if (min_dur(i) > 0 && min_usage(i) > 0)
664 retrieveCoreParameters(i);
665 // Compute the time window for consideration
666 tw_begin = min(tw_begin, est_2[i]);
667 tw_end = max(tw_end, lct_2[i]);
668 // Check whether the task 'i' is fixed
669 if ((CUMU_PT_ISFIXED(start[i]) && CUMU_PT_ISFIXED(dur[i]) && CUMU_PT_ISFIXED(usage[i])) || max_dur(i) <= 0 || max_usage(i) <= 0) {
670 // Swaping the id's
671 task_id[ii] = task_id[new_unfixed];
672 task_id[new_unfixed] = i;
673 new_unfixed--;
674 if (min_energy2 != NULL && min_dur(i) > 0 && min_usage(i) > 0) {
675 free_energy2[i] = 0;
676 if (rho == 1) {
677 // Resource stays engaged
678 min_energy2[i] = min_usage(i) * (lct_2[i] - est_2[i]);
679 } else {
680 // Resource is released
681 min_energy2[i] = min_usage(i) * min_dur(i);
682 }
683 }
684 }
685 }
686 tw_begin = minTime;
687 tw_end = maxTime;
688 // Trailing the index of the last unfixed task
689 last_unfixed = new_unfixed;
690 #if CUMUVERB>1
691 fprintf(stderr, "\tEntering cumulative propagation loop\n");
692 #endif
693 // idempotent
694 do {
695 bound_update = false;
696 // Reseting the profile size
697 tt_profile_size = 0;
698 // Time-table propagators
699 if (tt_check || tt_filt) {
700 // Time-table propagation
701 if (! time_table_propagation(task_id, tw_begin, tw_end) ) {
702 // Inconsistency was detected
703 #if CUMUVERB > 1
704 fprintf(stderr, "Leaving cumulative propagation with failure\n");
705 #endif
706 return false;
707 }
708 }
709 //if (!bound_update)
710 // nb_prop_calls++;
711 // Time-table-edge-finding propagation
712 if (!bound_update && last_unfixed > 0 && (ttef_check || ttef_filt)) { // && nb_prop_calls % 100 == 0) {
713 nb_prop_calls++;
714 if (ttef_prop_factor != 0 && nb_prop_calls % ttef_prop_factor != 0)
715 continue;
716 #if CUMUVERB > 0
717 fprintf(stderr, "Entering TTEF\n");
718 #endif
719 // Retrieval of the data required for the TTEF propagation
720 for (int ii = 0; ii <= last_unfixed; ii++) {
721 const int i = task_id[ii];
722 retrieveEnergyParameters(i);
723 }
724 // Initialisation of necessary structures
725 // - Unfixed tasks sorted according earliest start time
726 // - Unfixed tasks sorted according latest completion time
727 // - Energy of the compulsory parts after the latest completion
728 // time of unfixed tasks
729 // - Energy of the compulsory parts after the earliest start
730 // time of unfixed tasks
731 ttef_initialise_parameters();
732
733 // TTEF filtering algorithm
734 if (ttef_filt) {
735 if (!ttef_bounds_propagation(1, 2)) {
736 // Inconsistency was detected
737 return false;
738 }
739 } else {
740 #if CUMUVERB > 0
741 fprintf(stderr, "Entering TTEF Consistency\n");
742 #endif
743 if (!ttef_consistency_check(1)) {
744 // Inconsistency was detected
745 return false;
746 }
747 #if CUMUVERB > 0
748 fprintf(stderr, "Leaving TTEF Consistency\n");
749 #endif
750 }
751 #if CUMUVERB > 0
752 fprintf(stderr, "Leaving TTEF\n");
753 #endif
754 }
755 } while (idem && bound_update);
756 #if CUMUVERB > 0
757 fprintf(stderr, "\tLeaving cumulative propagation loop\n");
758 fprintf(stderr, "Leaving cumulative propagation without failure\n");
759 #endif
760 return true;
761 }
762
763 // Comparison between two compulsory parts
764 static bool
compare_CompParts(CompPart cp1,CompPart cp2)765 compare_CompParts(CompPart cp1, CompPart cp2) {
766 if (cp1.begin < cp2.begin) return true;
767 if (cp1.begin > cp2.begin) return false;
768 // ASSUMPTION
769 // - cp1.begin == cp2.begin
770 if (cp1.end < cp2.end) return true;
771 if (cp1.end > cp2.end) return false;
772 // ASSUMPTION
773 // - cp1.end == cp2.end
774 if (cp1.task < cp2.task) return true;
775 return false;
776 }
777
778
779 // Creation of the resource profile for the time-table consistency check
780 // and propagator
781 CUMU_BOOL
time_table_propagation(CUMU_ARR_INT & task,const int tw_begin,const int tw_end)782 time_table_propagation(CUMU_ARR_INT & task, const int tw_begin, const int tw_end) {
783 list<ProfileChangePt> changes;
784 list<CUMU_INT> comp_task;
785 //int size_profile = 0;
786 #if CUMUVERB>10
787 fprintf(stderr, "\tCompulsory Parts ...\n");
788 #endif
789 get_compulsory_parts2(changes, comp_task, task, 0, task.size(), tw_begin, tw_end);
790 // Proceed if there are compulsory parts
791 if (!changes.empty()) {
792 #if CUMUVERB>1
793 fprintf(stderr, "\tSorting (size %d)...\n", (int) changes.size());
794 #endif
795 // Sorting the start and end points of all the profile
796 changes.sort(compare_ProfileChangePt);
797 #if CUMUVERB>1
798 fprintf(stderr, "\tSorting (size %d)...\n", (int) changes.size());
799 #endif
800 // Counting the number of different profiles
801 tt_profile_size = count_profile(changes);
802 #if CUMUVERB>1
803 fprintf(stderr, "\t#profile parts = %d\n", tt_profile_size);
804 #endif
805 #if CUMUVERB>1
806 fprintf(stderr, "\tProfile Parts ...\n");
807 #endif
808 // Creating the different profile parts
809 create_profile(changes);
810 int i_max_usage = 0;
811 #if CUMUVERB>1
812 fprintf(stderr, "\tFilling of Profile Parts ...\n");
813 #endif
814 // Filling the profile parts with tasks
815 if (!fill_in_profile_parts(tt_profile, tt_profile_size, comp_task, i_max_usage)) {
816 return false;
817 }
818 #if CUMUVERB>10
819 fprintf(stderr, "\tFiltering Resource Limit ...\n");
820 #endif
821 // Filtering of resource limit variable
822 if (!filter_limit(tt_profile, i_max_usage)) {
823 return false;
824 }
825 if (tt_filt) {
826 #if CUMUVERB>10
827 fprintf(stderr, "\tFiltering Start Times ...\n");
828 #endif
829 // Time-table filtering
830 if (!time_table_filtering(tt_profile, tt_profile_size, task, 0, last_unfixed, tt_profile[i_max_usage].level)) {
831 return false;
832 }
833 }
834 }
835 #if CUMUVERB>10
836 fprintf(stderr, "\tEnd of time-table propagation ...\n");
837 #endif
838 return true;
839 }
840
841 void
842 get_compulsory_parts2(
843 list<ProfileChangePt> &changes, list<CUMU_INT> &comp_task, CUMU_ARR_INT & task,
844 CUMU_INT i_start, CUMU_INT i_end, const int tw_begin, const int tw_end
845 );
846
847 // Sets for each profile part its begin and end time in chronological order
848 // Runtime complexity: O(n)
849 //
850 void
create_profile(list<ProfileChangePt> & changes)851 create_profile(list<ProfileChangePt> &changes) {
852 list<ProfileChangePt>::iterator iter = changes.begin();
853 int cur_profile = 0;
854 int cur_time = iter->time;
855 ProfileChange cur_change = iter->change;
856 int no_starts = 1;
857 for (; iter != changes.end(); iter++) {
858 if (iter->time > cur_time && no_starts > 1) {
859 #if CUMUVERB>20
860 fprintf(stderr, "Set times for profile part %d = [%d, %d)\n", cur_profile, cur_time, iter->time);
861 fprintf(stderr, "\t%p; %p; %d\n", tt_profile, this, start.size());
862 #endif
863 set_times_for_profile(cur_profile, cur_time, iter->time);
864 cur_profile++;
865 }
866 no_starts += (iter->change == PROFINC ? 1 : -1);
867 cur_change = iter->change;
868 cur_time = iter->time;
869 }
870 }
871
872 inline void
set_times_for_profile(int i,CUMU_INT begin,CUMU_INT end)873 set_times_for_profile(int i, CUMU_INT begin, CUMU_INT end) {
874 tt_profile[i].begin = begin;
875 tt_profile[i].end = end;
876 tt_profile[i].level = 0;
877 tt_profile[i].tasks.clear();
878 }
879
880 // Filling the profile parts with compulsory parts and checking for a resource
881 // overload
882 CUMU_BOOL
fill_in_profile_parts(ProfilePart * profile,int size,list<CUMU_INT> comp_task,int & i_max_usage)883 fill_in_profile_parts(ProfilePart * profile, int size, list<CUMU_INT> comp_task, int & i_max_usage) {
884 list<CUMU_INT>::iterator iter;
885 int i = 0;
886 CUMU_INT lst_i, ect_i;
887
888 #if CUMUVERB>2
889 fprintf(stderr, "\t\tstart filling profiles (size %d)\n", size);
890 #endif
891 for (iter = comp_task.begin(); iter != comp_task.end(); iter++) {
892 #if CUMUVERB>2
893 fprintf(stderr, "\t\tcomp part = %d\n", *iter);
894 #endif
895 lst_i = lst_2[*iter];
896 ect_i = ect_2[*iter];
897 #if CUMUVERB>2
898 fprintf(stderr, "\t\tFinding first profile part ; est: %d ; lst: %d ; ect: %d ; dur: %d\n",est_2[*iter],lst_i, ect_i, min_dur(*iter));
899 #endif
900 // Find first profile
901 i = find_first_profile(profile, 0, size - 1, lst_i);
902 #if CUMUVERB>2
903 fprintf(stderr, "\t\tAdding comp parts of level %d\n", min_usage(*iter));
904 #endif
905 // Add compulsory part to the profile
906 while (i < size && profile[i].begin < ect_i) {
907
908 if (calendar[taskCalendar[*iter]-1][profile[i].begin] == 1 || rho == 1) {
909
910 #if CUMUVERB>2
911 fprintf(stderr, "\t\t\tAdding comp parts in profile part %d\n", i);
912 #endif
913 profile[i].level += min_usage(*iter);
914 profile[i].tasks.insert(*iter);
915 // Checking if the profile part i is the part with the maximal level
916 //
917 if (profile[i].level > profile[i_max_usage].level) {
918 i_max_usage = i;
919 }
920 // Time-table consistency check
921 //
922 if (profile[i].level > max_limit()) {
923 #if CUMUVERB > 20
924 fprintf(stderr, "\t\t\tResource overload (%d > %d) in profile part %d\n", profile[i].level, max_limit(), i);
925 #endif
926 // Increment the inconsistency counter
927 nb_tt_incons++;
928
929 // The resource is overloaded in this part
930 vec<Lit> expl;
931 if (so.lazy) {
932 CUMU_INT lift_usage = profile[i].level - max_limit() - 1;
933 CUMU_INT begin1, end1;
934 // TODO Different choices to pick the interval
935 // Pointwise explanation
936 begin1 = profile[i].begin + ((profile[i].end - profile[i].begin) / 2);
937 end1 = begin1 + 1;
938 // Generation of the explanation
939 analyse_limit_and_tasks(
940 expl, profile[i].tasks, lift_usage, begin1, end1
941 );
942 }
943 // Submitting of the conflict explanation
944 submit_conflict_explanation(expl);
945 #if CUMUVERB > 20
946 fprintf(stderr, "\texpl size: %d\n",expl.size());
947 fprintf(stderr, "\t\tend filling (conflict)\n");
948 #endif
949 return false;
950 }
951 }
952 i++;
953 }
954 }
955 #if CUMUVERB>2
956 fprintf(stderr, "\t\tend filling (successful)\n");
957 #endif
958 return true;
959 }
960
961 // Finds the profile part that begins at the time unit "lst"
962 // Complexity: O(log(high - low + 1))
963 //
964 int
find_first_profile(ProfilePart * profile,int low,int high,CUMU_INT lst)965 find_first_profile(ProfilePart * profile, int low, int high, CUMU_INT lst) {
966 int median = 0;
967 while (profile[low].begin != lst) {
968 median = low + (high - low + 1) / 2;
969 if (profile[median].begin > lst) {
970 high = median;
971 } else {
972 low = median;
973 }
974 }
975 return low;
976 }
977
978 // Counting the number of profiles
979 //
980 int
count_profile(list<ProfileChangePt> & changes)981 count_profile(list<ProfileChangePt> &changes) {
982 list<ProfileChangePt>::iterator iter = changes.begin();
983 int cur_time = iter->time;
984 int next_time;
985 ProfileChange cur_change = iter->change;
986 int no_starts = ( iter->change == PROFINC ? 1 : 0 );
987 int no_profile = no_starts;
988 iter++;
989
990 #if CUMUVERB>2
991 fprintf( stderr, "\t\t\ttime = %d; change = %d; no_starts = %d; no_profile = %d;\n", cur_time, cur_change, no_starts, no_profile);
992 #endif
993 for (; iter != changes.end(); iter++) {
994 if (iter->change == PROFINC) {
995 if (cur_time < iter->time || cur_change == PROFDEC) {
996 no_profile++;
997 }
998 no_starts++;
999 } else {
1000 // ASSUMPTION
1001 // - iter->change = PROFDEC
1002 no_starts--;
1003 next_time = iter->time;
1004 iter++;
1005 if (iter != changes.end() && no_starts > 0 && iter->time > next_time) {
1006 no_profile++;
1007 }
1008 iter--;
1009 }
1010 cur_time = iter->time;
1011 cur_change = iter->change;
1012 #if CUMUVERB>2
1013 fprintf( stderr, "\t\t\ttime = %d; change = %d; no_starts = %d; no_profile = %d;\n", cur_time, cur_change, no_starts, no_profile);
1014 #endif
1015 }
1016 return no_profile;
1017 }
1018
1019 static bool
compare_ProfileChangePt(ProfileChangePt & pt1,ProfileChangePt & pt2)1020 compare_ProfileChangePt(ProfileChangePt & pt1, ProfileChangePt & pt2) {
1021 if (pt1.time == pt2.time && pt1.change == PROFDEC && pt2.change == PROFINC) return true;
1022 return pt1.time < pt2.time;
1023 }
1024
1025 // Time-table filtering on the lower bound of the resource limit variable
1026 // Complexity:
1027 CUMU_BOOL
1028 filter_limit(ProfilePart * profile, int & i_max_usage);
1029
1030 // Time-table filtering on the start time variables
1031 // Complexity:
1032 CUMU_BOOL
1033 time_table_filtering(ProfilePart profile[], int size, CUMU_ARR_INT & task, int start, int end, CUMU_INT max_usage);
1034 CUMU_BOOL
1035 time_table_filtering_lb(ProfilePart profile[], int low, int high, int task);
1036 CUMU_BOOL
1037 time_table_filtering_ub(ProfilePart profile[], int low, int high, int task);
1038
1039 int
1040 find_first_profile_for_lb(ProfilePart profile[], int low, int high, CUMU_INT t);
1041 int
1042 find_first_profile_for_ub(ProfilePart profile[], int low, int high, CUMU_INT t);
1043
1044 // Analysing the conflict and generation of the explanations
1045 // NOTE: Fixed durations and resource usages are assumed!!!
1046 //
1047 // Explanation is created for the time interval [begin, end), i.e., exluding end.
1048 //
1049 void
1050 analyse_limit_and_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end);
1051 void
1052 analyse_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end);
1053 void
1054 submit_conflict_explanation(vec<Lit> & expl);
1055 Clause *
1056 get_reason_for_update(vec<Lit> & expl);
1057
1058 // TODO Disentailment check
1059 //CUMU_INT
1060 //checkSatisfied() {
1061 // // XXX Until no cumulative propagator is implemented the constraint
1062 // // is always ?satisfied?
1063 // return 1;
1064 //}
1065
1066 // Wrapper to get the negated literal -[[v <= val]] = [[v >= val + 1]]
1067 inline Lit
getNegLeqLit(CUMU_INTVAR v,CUMU_INT val)1068 getNegLeqLit(CUMU_INTVAR v, CUMU_INT val) {
1069 //return v->getLit(val + 1, 2);
1070 return (INT_VAR_LL == v->getType() ? v->getMaxLit() : v->getLit(val + 1, 2));
1071 }
1072 // Wrapper to get the negated literal -[[v >= val]] = [[ v <= val - 1]]
1073 inline Lit
getNegGeqLit(CUMU_INTVAR v,CUMU_INT val)1074 getNegGeqLit(CUMU_INTVAR v, CUMU_INT val) {
1075 //return v->getLit(val - 1, 3);
1076 return (INT_VAR_LL == v->getType() ? v->getMinLit() : v->getLit(val - 1, 3));
1077 }
1078
1079 };
1080
1081 /****
1082 * Functions related to the Time-Table Consistency Check and Propagation
1083 ****/
1084
1085 void
get_compulsory_parts2(list<ProfileChangePt> & changes,list<CUMU_INT> & comp_task,CUMU_ARR_INT & task,CUMU_INT i_start,CUMU_INT i_end,const int tw_begin,const int tw_end)1086 CumulativeCalProp::get_compulsory_parts2(
1087 list<ProfileChangePt> &changes, list<CUMU_INT> &comp_task, CUMU_ARR_INT & task, CUMU_INT i_start, CUMU_INT i_end,
1088 const int tw_begin, const int tw_end
1089 ) {
1090 #if CUMUVERB>2
1091 fprintf(stderr, "\tstart get_compulsory_part from %d to %d\n", i_start, i_end);
1092 #endif
1093 for (int ii = i_start; ii < i_end; ii++) {
1094 const int i = task[ii];
1095 #if CUMUVERB>2
1096 fprintf(stderr, "\t\tii = %d; task[ii] = %d; est %d; dur %d\n", ii, i, est_2[i], min_dur(i));
1097 #endif
1098 // Check whether the task creates a compulsory part and if it falls into
1099 // the considered time window
1100 if (min_dur(i) > 0 && min_usage(i) > 0 && lst_2[i] < ect_2[i] && tw_begin < lct_2[i] && est_2[i] < tw_end) {
1101 #if CUMUVERB>2
1102 fprintf(stderr, "\t\ttask[ii] = %d, comp part [%d, %d)\n", i, lst_2[i], ect_2[i]);
1103 #endif
1104 // Add task to the list
1105 comp_task.push_back(i);
1106 // Add time points to change lists
1107 int t;
1108 changes.push_back( ProfileChangePt(lst_2[i], PROFINC) );
1109 changes.push_back( ProfileChangePt(ect_2[i], PROFDEC) );
1110 if (rho == 0){
1111 // Resource is released
1112 // Calculating the breaks of the task 'i'
1113 for (t = lst_2[i] + 1; t < ect_2[i]; t++){
1114 const int tCal = taskCalendar[i] - 1;
1115 if (calendar[tCal][t] == 1 && calendar[tCal][t-1] == 0) {
1116 changes.push_back( ProfileChangePt(t, PROFINC) );
1117 }
1118 if (calendar[tCal][t] == 0 && calendar[tCal][t-1] == 1) {
1119 changes.push_back( ProfileChangePt(t, PROFDEC) );
1120 }
1121 }
1122 }
1123 }
1124 }
1125 #if CUMUVERB>2
1126 fprintf(stderr, "\tend get_compulsory_part\n");
1127 #endif
1128 }
1129
1130
1131 /***************************************************************************************
1132 * Function for time-table filtering on the lower bound of the resource limit variable *
1133 ***************************************************************************************/
1134
1135 CUMU_BOOL
filter_limit(ProfilePart * profile,int & i)1136 CumulativeCalProp::filter_limit(ProfilePart * profile, int & i) {
1137 if (min_limit() < profile[i].level) {
1138 Clause * reason = NULL;
1139 nb_tt_filt++;
1140 if (so.lazy) {
1141 // Lower bound can be updated
1142 // XXX Determining what time period is the best
1143 int expl_begin = profile[i].begin + ((profile[i].end - profile[i].begin - 1)/2);
1144 int expl_end = expl_begin + 1;
1145 vec<Lit> expl;
1146 // Get the negated literals for the tasks in the profile
1147 analyse_tasks(expl, profile[i].tasks, 0, expl_begin, expl_end);
1148 // Transform literals to a clause
1149 reason = get_reason_for_update(expl);
1150 }
1151 if (! limit->setMin(profile[i].level, reason)) {
1152 // Conflict occurred
1153 return false;
1154 }
1155 // Set bound_update to true
1156 bound_update = true;
1157 }
1158 return true;
1159 }
1160
1161 /******************************************************************
1162 * Functions for Time-Table Filtering on the start time variables *
1163 ******************************************************************/
1164
1165 CUMU_BOOL
time_table_filtering(ProfilePart profile[],int size,CUMU_ARR_INT & task,int i_start,int i_end,CUMU_INT max_usage)1166 CumulativeCalProp::time_table_filtering(ProfilePart profile[], int size, CUMU_ARR_INT & task, int i_start, int i_end, CUMU_INT max_usage) {
1167 for (int ii = i_start; ii <= i_end; ii++) {
1168 const int i = task[ii];
1169 // Skipping tasks with zero duration or usage
1170 if (min_dur(i) <= 0 || min_usage(i) <= 0)
1171 continue;
1172 #if CUMUVERB>2
1173 fprintf(stderr, "TT Filtering of task %d\n", i);
1174 #endif
1175 // Check if the sum of max_usage and the task's usage are greater then the upper bound
1176 // on the resource limit
1177 if (min_usage(i) + max_usage > max_limit()) {
1178 int index;
1179 #if CUMUVERB>2
1180 fprintf(stderr, "Finding the first index for LB ...\n");
1181 #endif
1182 // Find initial profile part for lower bound propagation
1183 //
1184 index = find_first_profile_for_lb(profile, 0, size - 1, est_2[i]);
1185 #if CUMUVERB>2
1186 fprintf(stderr, "Lower bound starting from index %d\n", index);
1187 #endif
1188 // Update the lower bound if possible
1189 if (! time_table_filtering_lb(profile, index, size - 1, i)) {
1190 return false;
1191 }
1192 #if CUMUVERB>2
1193 fprintf(stderr, "Finding the first index for UB ...\n");
1194 #endif
1195 // Find initial profile part for upper bound propagation
1196 index = find_first_profile_for_ub(profile, 0, size - 1, lct_2[task[i]]);
1197 #if CUMUVERB>2
1198 fprintf(stderr, "Upper bound starting from index %d\n", index);
1199 #endif
1200 // Update the upper bound if possible
1201 if (! time_table_filtering_ub(profile, 0, index, i)) {
1202 return false;
1203 }
1204 }
1205 }
1206 return true;
1207 }
1208
1209 // Time-Table Filtering on the Lower Bound of Start Times Variables
1210 //
1211 CUMU_BOOL
time_table_filtering_lb(ProfilePart profile[],int low,int high,int task)1212 CumulativeCalProp::time_table_filtering_lb(ProfilePart profile[], int low, int high, int task) {
1213 int i;
1214 for (i = low; i <= high; i++) {
1215 if (ect_2[task] <= profile[i].begin) {
1216 // No lower bound update possible
1217 break;
1218 }
1219 // ASSUMPTION
1220 // - ect_2[task] > profile[i].begin
1221 if (est_2[task] < profile[i].end && profile[i].level + min_usage(task) > max_limit() ) {
1222 // Possibly a lower bound update if "task" as no compulsory part in the profile
1223 if (lst_2[task] < ect_2[task] && lst_2[task] <= profile[i].begin && profile[i].end <= ect_2[task]) {
1224 // No lower bound update possible for this profile part, because
1225 // "task" has a compulsory part in it
1226 continue ;
1227 }
1228 const int cal_idx = taskCalendar[task] - 1;
1229 const int * wPeriods = workingPeriods[cal_idx];
1230 const int end = min(ect_2[task], profile[i].end);
1231 if (rho == 0 && wPeriods[profile[i].begin] == wPeriods[end])
1232 continue;
1233 #if CUMUVERB>1
1234 fprintf(stderr, "\n----\n");
1235 fprintf(stderr, "setMin of task %d in profile part [%d, %d)\n", task, profile[i].begin, profile[i].end);
1236 fprintf(stderr, "task %d: lst = %d; ect = %d; dur = %d;\n", task, lst_2[task], ect_2[task], min_dur(task));
1237 #endif
1238 int expl_end = profile[i].end;
1239 Clause * reason = NULL;
1240 if (so.lazy) {
1241 // XXX Assumption for the remaining if-statement
1242 // No compulsory part of task in profile[i]!
1243 int lift_usage = profile[i].level + min_usage(task) - max_limit() - 1;
1244 // TODO Choices of different explanation
1245 // Pointwise explanation
1246 expl_end = end;
1247 int expl_begin = expl_end - 1;
1248
1249 vec<Lit> expl;
1250 const int wdays = min_dur(task) - (calendar[cal_idx][expl_end - 1] == 1 ? 0 : 1);
1251 int k = getStartTimeForEndTime(task, end, wdays);
1252 // Get the negated literal for [[start[task] >= ex_end - min_dur(task)]]
1253
1254 #if CUMUVERB>1
1255 fprintf(stderr, "start[%d] => %d ", task, k);
1256 #endif
1257 //expl.push(getNegGeqLit(start[task], expl_end - min_dur(task)));
1258 expl.push(getNegGeqLit(start[task], k));
1259 // Get the negated literal for [[dur[task] >= min_dur(task)]]
1260 if (min_dur0(task) < min_dur(task))
1261 expl.push(getNegGeqLit(dur[task], min_dur(task)));
1262 // Get the negated literal for [[usage[task] >= min_usage(task)]]
1263 if (min_usage0(task) < min_usage(task))
1264 expl.push(getNegGeqLit(usage[task], min_usage(task)));
1265 // Get the negated literals for the tasks in the profile and the resource limit
1266 analyse_limit_and_tasks(expl, profile[i].tasks, lift_usage, expl_begin, expl_end);
1267 #if CUMUVERB>1
1268 fprintf(stderr, " -> start[%d] => %d\n", task, expl_end);
1269 #endif
1270 // Transform literals to a clause
1271 reason = get_reason_for_update(expl);
1272 }
1273 nb_tt_filt++;
1274 // Impose the new lower bound on start[task]
1275 if (! start[task]->setMin(expl_end, reason)) {
1276 // Conflict occurred
1277 return false;
1278 }
1279 // Update task's parameters
1280 retrieveCoreParameters(task);
1281 // Set bound_update to true
1282 bound_update = true;
1283 // Check for the next profile
1284 if (expl_end < profile[i].end) {
1285 i--;
1286 }
1287 }
1288 }
1289 return true;
1290 }
1291
1292 // Time-table filtering on the upper bound of start times variables
1293 //
1294 CUMU_BOOL
time_table_filtering_ub(ProfilePart profile[],int low,int high,int task)1295 CumulativeCalProp::time_table_filtering_ub(ProfilePart profile[], int low, int high, int task) {
1296 int i;
1297 for (i = high; i >= low; i--) {
1298 if (profile[i].end <= lst_2[task]) {
1299 // No upper bound update possible
1300 break;
1301 }
1302 // ASSUMPTION for the remaining for-loop
1303 // - profile[i].end > lst_2[task]
1304 if (profile[i].begin < lct_2[task] && profile[i].level + min_usage(task) > max_limit()) {
1305 // Possibly a upper bound update possible if "task" has no compulsory part
1306 // in this profile part
1307 if (lst_2[task] < ect_2[task] && lst_2[task] <= profile[i].begin && profile[i].end <= ect_2[task]) {
1308 // No lower bound update possible for this profile part, because
1309 // "task" has a compulsory part in it
1310 continue ;
1311 }
1312 // Check whether the task has a working period in the profile part
1313 // if the resource is released
1314 const int cal_idx = taskCalendar[task] - 1;
1315 const int begin = max(lst_2[task], profile[i].begin);
1316 if (rho == 0 && workingPeriods[cal_idx][begin] == workingPeriods[cal_idx][profile[i].end])
1317 continue;
1318
1319 int expl_begin = profile[i].begin;
1320 Clause * reason = NULL;
1321 if (so.lazy) {
1322 // ASSUMPTION for the remaining if-statement
1323 // - No compulsory part of task in profile[i]
1324 int lift_usage = profile[i].level + min_usage(task) - max_limit() - 1;
1325 // TODO Choices of different explanations
1326 // Pointwise explanation
1327 expl_begin = begin;
1328 //expl_begin = max(profile[i].begin, lst_2[task]);
1329 int expl_end = expl_begin + 1;
1330 vec<Lit> expl;
1331 // Get the negated literal for [[start[task] <= expl_begin]]
1332 expl.push(getNegLeqLit(start[task], expl_begin));
1333 // Get the negated literal for [[dur[task] >= min_dur(task)]]
1334 if (min_dur0(task) < min_dur(task))
1335 expl.push(getNegGeqLit(dur[task], min_dur(task)));
1336 // Get the negated literal for [[usage[task] >= min_usage(task)]]
1337 if (min_usage0(task) < min_usage(task))
1338 expl.push(getNegGeqLit(usage[task], min_usage(task)));
1339 // Get the negated literals for the tasks in the profile and the resource limit
1340 analyse_limit_and_tasks(expl, profile[i].tasks, lift_usage, expl_begin, expl_end);
1341 // Transform literals to a clause
1342 reason = get_reason_for_update(expl);
1343 }
1344 int new_lst = expl_begin;
1345 int j = 0;
1346 while (j < min_dur(task)) {
1347 new_lst--;
1348 if (calendar[taskCalendar[task]-1][new_lst] == 1) {
1349 j++;
1350 }
1351 }
1352
1353 nb_tt_filt++;
1354 // Impose the new lower bound on start[task]
1355 //if (! start[task]->setMax(expl_begin - min_dur(task), reason)) {
1356 if (! start[task]->setMax(new_lst, reason)) {
1357 // Conflict occurred
1358 return false;
1359 }
1360 // Update task's core parameters
1361 retrieveCoreParameters(task);
1362 // Set bound_update to true
1363 bound_update = true;
1364 // Check for the next profile
1365 if (profile[i].begin < expl_begin) {
1366 i++;
1367 }
1368 }
1369 }
1370 return true;
1371 }
1372
1373
1374 int
find_first_profile_for_lb(ProfilePart profile[],int low,int high,CUMU_INT t)1375 CumulativeCalProp::find_first_profile_for_lb(ProfilePart profile[], int low, int high, CUMU_INT t) {
1376 int median;
1377 if (profile[low].end > t || low == high) {
1378 return low;
1379 }
1380 if (profile[high].begin <= t) {
1381 return high;
1382 }
1383 #if CUMUVERB>2
1384 fprintf(stderr, "time = %d\n", t);
1385 fprintf(stderr, "profile[low = %d] = [%d, %d); ", low, profile[low].begin, profile[low].end);
1386 fprintf(stderr, "profile[high = %d] = [%d, %d);\n", high, profile[high].begin, profile[high].end);
1387 #endif
1388 // ASSUMPTIONS:
1389 // - profile[low].end <= t
1390 // - profile[high].begin > t
1391 // - low < high
1392 //
1393 while (!(profile[low].end <= t && t <= profile[low + 1].end)) {
1394 median = low + (high - low + 1) / 2;
1395 #if CUMUVERB>2
1396 fprintf(stderr, "profile[lo = %d] = [%d, %d); ", low, profile[low].begin, profile[low].end);
1397 fprintf(stderr, "profile[me = %d] = [%d, %d); ", median, profile[median].begin, profile[median].end);
1398 fprintf(stderr, "profile[hi = %d] = [%d, %d);\n", high, profile[high].begin, profile[high].end);
1399 #endif
1400 if (t < profile[median].end) {
1401 high = median;
1402 //high = median - 1;
1403 low++;
1404 } else {
1405 low = median;
1406 }
1407 }
1408 return low;
1409 }
1410
1411 int
find_first_profile_for_ub(ProfilePart profile[],int low,int high,CUMU_INT t)1412 CumulativeCalProp::find_first_profile_for_ub(ProfilePart profile[], int low, int high, CUMU_INT t) {
1413 int median;
1414 if (profile[high].begin <= t || low == high) {
1415 return high;
1416 }
1417 if (t < profile[low].end) {
1418 return low;
1419 }
1420 // ASSUMPTIONS:
1421 // - profile[high].begin > t
1422 // - profile[low].end <= t
1423 // - low < high
1424 //
1425 while (!(profile[high - 1].begin <= t && t < profile[high].begin)) {
1426 median = low + (high - low + 1) / 2;
1427 if (t < profile[median].begin) {
1428 high = median;
1429 } else {
1430 low = median;
1431 high--;
1432 }
1433 }
1434 return high;
1435 }
1436
1437
1438 /************************************************************************
1439 * Functions for Analysing Conflicts or Bound Updates and Generation of *
1440 * their explanations *
1441 ************************************************************************/
1442
1443 void
analyse_limit_and_tasks(vec<Lit> & expl,set<CUMU_INT> & tasks,CUMU_INT lift_usage,CUMU_INT begin,CUMU_INT end)1444 CumulativeCalProp::analyse_limit_and_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end) {
1445 CUMU_INT diff_limit = max_limit0() - max_limit();
1446 if (diff_limit > 0) {
1447 // Lifting of limit variable if possible
1448 if (diff_limit <= lift_usage) {
1449 // No explanation literal is needed
1450 lift_usage -= diff_limit;
1451 } else {
1452 lift_usage = 0;
1453 // Get explanation for [[limit <= max_limit() + lift_usage]]
1454 #if CUMUVERB > 10
1455 fprintf(stderr, "/\\ limit <= %d ", max_limit() + lift_usage);
1456 #endif
1457 expl.push(getNegLeqLit(limit, max_limit() + lift_usage));
1458 }
1459 }
1460 analyse_tasks(expl, tasks, lift_usage, begin, end);
1461 }
1462
1463 void
analyse_tasks(vec<Lit> & expl,set<CUMU_INT> & tasks,CUMU_INT lift_usage,CUMU_INT begin,CUMU_INT end)1464 CumulativeCalProp::analyse_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end) {
1465 set<CUMU_INT>::iterator iter;
1466 for (iter = tasks.begin(); iter != tasks.end(); iter++) {
1467 const int i = *iter;
1468 #if CUMUVERB > 10
1469 fprintf(stderr, "\ns[%d] in [%d..%d]\n", i, start[i]->getMin(), start[i]->getMax());
1470 #endif
1471 if (min_usage(i) <= lift_usage) {
1472 // Task is not relevant for the resource overload
1473 lift_usage -= min_usage(i);
1474 } else {
1475 const int duration = min_dur(i) - (calendar[taskCalendar[i]-1][end-1] ? 0 : 1);
1476 const int t = getStartTimeForEndTime(i, end, duration);
1477
1478 // Lower bound of the start time variable matters
1479 if(t > min_start0(i)){
1480 // Get explanation for [[start[i] >= end - min_dur(i)]]
1481
1482 #if CUMUVERB > 10
1483 fprintf(stderr, "/\\ start[%d] => %d ", i, t);
1484 #endif
1485 expl.push(getNegGeqLit(start[i], t));
1486 }
1487 if (begin < max_start0(i)) {
1488 // Upper bound of the start time variable matters
1489 // Get explanation for [[start[i] <= begin]]
1490 #if CUMUVERB > 10
1491 fprintf(stderr, "/\\ start[%d] <= %d ", i, begin);
1492 #endif
1493 expl.push(getNegLeqLit(start[i], begin));
1494 }
1495 // Get the negated literal for [[dur[i] >= min_dur(i)]]
1496 if (min_dur0(i) < min_dur(i))
1497 expl.push(getNegGeqLit(dur[i], min_dur(i)));
1498 // Get the negated literal for [[usage[i] >= min_usage(i)]]
1499 const int usage_diff = min_usage(i) - min_usage0(i);
1500 if (usage_diff > 0) {
1501 if (usage_diff <= lift_usage)
1502 lift_usage -= usage_diff;
1503 else
1504 expl.push(getNegGeqLit(usage[i], min_usage(i)));
1505 }
1506 }
1507 }
1508 }
1509
1510 void
submit_conflict_explanation(vec<Lit> & expl)1511 CumulativeCalProp::submit_conflict_explanation(vec<Lit> & expl) {
1512 Clause * reason = NULL;
1513 if (so.lazy) {
1514 reason = Reason_new(expl.size());
1515 int i = 0;
1516 for (; i < expl.size(); i++) { (*reason)[i] = expl[i]; }
1517 }
1518 sat.confl = reason;
1519 }
1520
1521 Clause *
get_reason_for_update(vec<Lit> & expl)1522 CumulativeCalProp::get_reason_for_update(vec<Lit> & expl) {
1523 Clause* reason = Reason_new(expl.size() + 1);
1524 for (int i = 1; i <= expl.size(); i++) {
1525 (*reason)[i] = expl[i-1];
1526 }
1527 return reason;
1528 }
1529
1530
cumulative_cal(vec<IntVar * > & s,vec<IntVar * > & d,vec<IntVar * > & r,IntVar * limit,vec<vec<int>> & cal,vec<int> & taskCal,int rho_in,int resCal_in)1531 void cumulative_cal(vec<IntVar*>& s, vec<IntVar*>& d, vec<IntVar*>& r, IntVar* limit, vec<vec<int> >& cal, vec<int>& taskCal, int rho_in, int resCal_in) {
1532 list<string> opt;
1533 cumulative_cal(s, d, r, limit, cal, taskCal, rho_in, resCal_in);
1534 }
1535
cumulative_cal(vec<IntVar * > & s,vec<IntVar * > & d,vec<IntVar * > & r,IntVar * limit,vec<vec<int>> & cal,vec<int> & taskCal,int rho_in,int resCal_in,list<string> opt)1536 void cumulative_cal(vec<IntVar*>& s, vec<IntVar*>& d, vec<IntVar*>& r, IntVar* limit, vec<vec<int> >& cal, vec<int>& taskCal, int rho_in, int resCal_in, list<string> opt) {
1537 rassert(s.size() == d.size() && s.size() == r.size());
1538 // ASSUMPTION
1539 // - s, d, and r contain the same number of elements
1540
1541 vec<IntVar*> s_new, d_new, r_new;
1542 vec<int> taskCal_new;
1543 int r_sum = 0;
1544
1545 for (int i = 0; i < s.size(); i++) {
1546 if (r[i]->getMax() > 0 && d[i]->getMax() > 0) {
1547 s_new.push(s[i]);
1548 d_new.push(d[i]);
1549 r_new.push(r[i]);
1550 r_sum += r[i]->getMax();
1551 taskCal_new.push(taskCal[i]);
1552 }
1553 }
1554
1555
1556
1557 if (r_sum <= limit->getMin()) return;
1558
1559 // Global cumulative constraint
1560 new CumulativeCalProp(s_new, d_new, r_new, limit, cal, taskCal_new, rho_in, resCal_in, opt);
1561 }
1562
1563 /********************************************
1564 * Functions related to the TTEF propagator
1565 *******************************************/
1566
1567 // Initialisation of various parameters
1568 //
1569 void
ttef_initialise_parameters()1570 CumulativeCalProp::ttef_initialise_parameters() {
1571 int energy = 0;
1572 int p_idx = tt_profile_size - 1;
1573
1574 // Initialisation of the task id's arrays
1575 //
1576 for (int ii = 0; ii <= last_unfixed; ii++) {
1577 task_id_est[ii] = task_id[ii];
1578 task_id_lct[ii] = task_id[ii];
1579 }
1580 if (ttef_filt) {
1581 for (int ii = 0; ii <= last_unfixed; ii++) {
1582 const int i = task_id[ii];
1583 new_est[i] = est_2[i];
1584 new_lct[i] = lct_2[i];
1585 }
1586 }
1587 // Sorting of the task id's arrays
1588 //
1589 sort(task_id_est, task_id_est + last_unfixed + 1, sort_est_asc);
1590 sort(task_id_lct, task_id_lct + last_unfixed + 1, sort_lct_asc);
1591 // Calculation of 'tt_after_est'
1592 //
1593 for (int ii = last_unfixed; ii >= 0; ii--) {
1594 const int i = task_id_est[ii];
1595 if (p_idx < 0 || tt_profile[p_idx].end <= est_2[i]) {
1596 tt_after_est[ii] = energy;
1597 } else if (tt_profile[p_idx].begin <= est_2[i]) {
1598 tt_after_est[ii] = energy + tt_profile[p_idx].level * (tt_profile[p_idx].end - est_2[i]);
1599 } else {
1600 assert(tt_profile[p_idx].begin > est_2[i]);
1601 energy += tt_profile[p_idx].level * (tt_profile[p_idx].end - tt_profile[p_idx].begin);
1602 p_idx--;
1603 ii++;
1604 }
1605 }
1606 // Calculation of 'tt_after_lct'
1607 //
1608 p_idx = tt_profile_size - 1;
1609 energy = 0;
1610 for (int ii = last_unfixed; ii >= 0; ii--) {
1611 unsigned i = task_id_lct[ii];
1612 if (p_idx < 0 || tt_profile[p_idx].end <= lct_2[i]) {
1613 tt_after_lct[ii] = energy;
1614 } else if (tt_profile[p_idx].begin <= lct_2[i]) {
1615 tt_after_lct[ii] = energy + tt_profile[p_idx].level * (tt_profile[p_idx].end - lct_2[i]);
1616 } else {
1617 assert(tt_profile[p_idx].begin > lct_2[i]);
1618 energy += tt_profile[p_idx].level * (tt_profile[p_idx].end - tt_profile[p_idx].begin);
1619 p_idx--;
1620 ii++;
1621 }
1622 }
1623 }
1624
1625 // TTEF Consistency Check
1626 // Assumptions:
1627 // - task_id_est sorted in non-decreasing order of est's
1628 // - task_id_lct sorted in non-decreasing order of lct's
1629 bool
ttef_consistency_check(int shift_in)1630 CumulativeCalProp::ttef_consistency_check(
1631 int shift_in
1632 ) {
1633 assert(last_unfixed > 0);
1634 assert(shift_in == 0 || shift_in == 1);
1635 nb_ttefc_calls++;
1636
1637 // Some constants
1638 const int * rPeriods = workingPeriods[resCalendar - 1];
1639 const int maxLimit = max_limit();
1640
1641 // Some variables
1642 int begin, end, workingDays, dur_shift;
1643 int est_idx_last = last_unfixed;
1644 int i, j, en_req, en_avail;
1645 int en_req_free;
1646 int min_en_avail = -1, lct_idx_last = last_unfixed, i_last = task_id_lct[lct_idx_last];
1647 bool consistent = true;
1648
1649 int dom_jj_last = -1;
1650 int* sumFreeEnergy = new int[last_unfixed + 1];
1651 for (int ii = 0; ii <= last_unfixed; ii++) {
1652 const int i = task_id_est[ii];
1653 sumFreeEnergy[ii] = (ii > 0 ? sumFreeEnergy[ii - 1] : 0) + free_energy2[i];
1654 }
1655
1656 end = lct_2[task_id_lct[last_unfixed]] + 1;
1657
1658 // Outer Loop: iterating over lct in non-increasing order
1659 //
1660 for (int ii = last_unfixed; ii >= 0; ii--) {
1661 i = task_id_lct[ii];
1662 if (end == lct_2[i]) continue;
1663
1664 assert(lct_2[i] < lct_2[i_last] || i == i_last);
1665
1666 // Check whether the current latest completion time have to be considered
1667 // Dominance rule for skipping time intervals
1668 workingDays = lct_2[i_last] - lct_2[i];
1669 if(rho == 0) {
1670 // Resource is released
1671 workingDays = (rPeriods[lct_2[i]] - rPeriods[lct_2[i_last]]);
1672 }
1673 const int free = maxLimit * workingDays - (tt_after_lct[ii] - tt_after_lct[lct_idx_last]);
1674 if (min_en_avail >= free) continue;
1675
1676 lct_idx_last = ii;
1677 i_last = i;
1678 min_en_avail = maxLimit * (lct_2[task_id_lct[last_unfixed]] - est_2[task_id_est[0]]);
1679
1680 end = lct_2[i];
1681 while (est_2[task_id_est[est_idx_last]] >= end) est_idx_last--;
1682 en_req_free = 0;
1683
1684 dom_jj_last = -1;
1685 // Inner Loop: iterating over est in non-increasing order
1686 //
1687 for (int jj = est_idx_last; jj >= 0; jj--) {
1688 nb_ttefc_steps++;
1689 j = task_id_est[jj];
1690
1691 // Dominance rule for skipping time intervals
1692 if (dom_jj_last >= 0) {
1693 // Computing an over-approximation of the required energy in the time
1694 // interval [est_2[j], end)
1695 const int dom_begin = est_2[j];
1696 const int dom_en_comp = tt_after_est[0] - tt_after_est[jj + 1];
1697 const int dom_en_free = sumFreeEnergy[jj] + en_req;
1698 const int dom_wdays = (rho == 1 ? end - dom_begin : rPeriods[dom_begin] - rPeriods[end]);
1699 const int dom_en_avail = maxLimit * dom_wdays - dom_en_comp - dom_en_free;
1700 if (dom_en_avail >= min_en_avail)
1701 break;
1702 }
1703
1704
1705 assert(est_2[j] < end);
1706 begin = est_2[j];
1707 if (lct_2[j] <= end) {
1708 // Task lies in the considered time interval
1709 en_req_free += free_energy2[j];
1710 } else if (shift_in == 1) {
1711 // Task might partially lie in the considered time interval
1712 dur_shift = get_free_dur_right_shift2(begin, end, j);
1713 // Adjusting dur_shift if resource stays engaged
1714 if (rho == 1) {
1715 const int dur_fixed = max(0, ect_2[j] - lst_2[j]);
1716 dur_shift = min(min_energy2[j] / min_usage(j) - dur_fixed, dur_shift);
1717 }
1718 en_req_free += min_usage(j) * dur_shift;
1719 }
1720 en_req = en_req_free + tt_after_est[jj] - tt_after_lct[ii];
1721 // TTEF_cal: Consider resource calendar
1722 workingDays = end - begin;
1723 if (rho == 0) {
1724 // Resource is released
1725 workingDays = rPeriods[begin] - rPeriods[end];
1726 }
1727 en_avail = maxLimit * workingDays - en_req;
1728
1729 if (min_en_avail > en_avail) {
1730 min_en_avail = en_avail;
1731 dom_jj_last = jj;
1732 }
1733
1734 // Check for resource overload
1735 //
1736 if (en_avail < 0) {
1737 consistent = false;
1738 ii = -1;
1739 break;
1740 }
1741 }
1742 }
1743
1744 delete[] sumFreeEnergy;
1745
1746 if (!consistent) {
1747 vec<Lit> expl;
1748 // Increment the inconsistency counter
1749 nb_ttef_incons++;
1750 if (so.lazy) {
1751 #if CUMUVERB > 0
1752 fprintf(stderr, "Entering TTEF Inconsistent\n");
1753 #endif
1754 list<TaskDur> tasks_tw;
1755 list<TaskDur> tasks_cp;
1756 int en_req1 = 0;
1757 // Retrieve tasks involved
1758 en_req1 = ttef_retrieve_tasks(shift_in, begin, end, -1, tasks_tw, tasks_cp);
1759 assert(en_req1 >= en_req);
1760 // Calculate the lifting TTEF_cal: added breaks
1761 int en_lift = en_req1 - 1 - maxLimit * workingDays;
1762 int breaks = end - begin - workingDays;
1763 assert(en_lift >= 0);
1764 // Explaining the overload
1765 #if CUMUVERB > 0
1766 fprintf(stderr, "Explaining TTEF Overload\n");
1767 #endif
1768 ttef_analyse_limit_and_tasks(begin, end, breaks, tasks_tw, tasks_cp, en_lift, expl);
1769 assert(expl.size() > 0);
1770 }
1771 #if CUMUVERB > 0
1772 fprintf(stderr, "TTEF Submitting Explanation\n");
1773 #endif
1774 // Submitting of the conflict explanation
1775 submit_conflict_explanation(expl);
1776 #if CUMUVERB > 0
1777 fprintf(stderr, "TTEF END Submitting Explanation: %d\n", consistent);
1778 #endif
1779 }
1780 return consistent;
1781 }
1782
1783 // TTEF bounds propagation
1784 //
1785 bool
ttef_bounds_propagation(int shift_in1,int shift_in2)1786 CumulativeCalProp::ttef_bounds_propagation(
1787 int shift_in1,
1788 int shift_in2
1789 ) {
1790 std::queue<TTEFUpdate> update1;
1791 std::queue<TTEFUpdate> update2;
1792 // TODO LB bound on the limit
1793 // LB bounds on the start times
1794 #if CUMUVERB > 0
1795 fprintf(stderr, "Entering TTEF Bounds Propagtion\n");
1796 #endif
1797 if (!ttef_bounds_propagation_lb(shift_in1, update1)) {
1798 // Inconsistency
1799 return false;
1800 }
1801 // UB bounds on the start times
1802 if (!ttef_bounds_propagation_ub(shift_in2, update2)) {
1803 // Inconsistency
1804 return false;
1805 }
1806 #if CUMUVERB > 0
1807 fprintf(stderr, "TTEF Bounds Propagtion\n");
1808 #endif
1809 // Updating the bounds
1810 if (!ttef_update_bounds(shift_in1, update1)) {
1811 return false;
1812 }
1813 if (!ttef_update_bounds(shift_in2, update2)) {
1814 return false;
1815 }
1816 #if CUMUVERB > 0
1817 fprintf(stderr, "Leaving TTEF Bounds Propagtion\n");
1818 #endif
1819 return true;
1820 }
1821
1822 bool
ttef_bounds_propagation_lb(int shift_in,std::queue<TTEFUpdate> & update_queue)1823 CumulativeCalProp::ttef_bounds_propagation_lb(
1824 int shift_in, std::queue<TTEFUpdate> & update_queue
1825 ) {
1826 assert(last_unfixed > 0);
1827 assert(shift_in == 0 || shift_in == 1);
1828 // Begin and end of the time interval [begin, end)
1829
1830 // Some constants
1831 const int maxLimit = max_limit();
1832 const int * rPeriods = workingPeriods[resCalendar - 1];
1833
1834 // Some variables
1835 int begin, end, dur_shift;
1836 int est_idx_last = last_unfixed;
1837 int i, j, en_req, en_avail;
1838 int en_req_free;
1839 int update_en_req_start, update_idx, update_workDays_req_in;
1840 int min_en_avail = -1, min_begin = minTime - 1;
1841 int workingDays = 0;
1842 bool consistent = true;
1843
1844 int maxEnergy = 0, lct_idx_last = -1;
1845 int* sumFreeEnergy = new int[last_unfixed + 1];
1846 for (int ii = 0; ii <= last_unfixed; ii++) {
1847 const int i = task_id_est[ii];
1848 maxEnergy = max(maxEnergy, min_usage(i) * (rho == 1 ? ect_2[i] - est_2[i] : min_dur(i)));
1849 sumFreeEnergy[ii] = (ii == 0 ? 0 : sumFreeEnergy[ii - 1]) + free_energy2[i];
1850 }
1851
1852 end = lct_2[task_id_lct[last_unfixed]] + 1;
1853
1854 // Outer Loop: iterating over lct in non-increasing order
1855 //
1856 for (int ii = last_unfixed; ii >= 0; ii--) {
1857 i = task_id_lct[ii];
1858 if (end == lct_2[i]) continue;
1859
1860 // Dominance rule for skipping time intervals
1861 if (min_en_avail >= 0) {
1862 const int dom_wdays = (rho == 1 ? end - lct_2[i] : rPeriods[lct_2[i]] - rPeriods[end]);
1863 const int dom_en_comp = tt_after_lct[ii] - tt_after_lct[lct_idx_last];
1864 const int dom_en_avail = maxLimit * dom_wdays - dom_en_comp;
1865 if (min_en_avail - dom_en_avail >= maxEnergy)
1866 continue;
1867 }
1868 lct_idx_last = ii;
1869 // Check whether the current latest completion time have to be considered
1870 min_en_avail = maxLimit * (lct_2[task_id_lct[last_unfixed]] - est_2[task_id_est[0]]);
1871 min_begin = minTime - 1;
1872
1873 end = lct_2[i];
1874 while (est_2[task_id_est[est_idx_last]] >= end) est_idx_last--;
1875
1876 // Initialisations for the inner loop
1877 en_req_free = 0;
1878 en_req = 0;
1879 update_idx = -1;
1880 update_en_req_start = -1;
1881 update_workDays_req_in = -1;
1882
1883 // Inner Loop: iterating over est in non-increasing order
1884 //
1885 for (int jj = est_idx_last; jj >= 0; jj--) {
1886 nb_ttef_lb_calls++;
1887 j = task_id_est[jj];
1888
1889 assert(est_2[j] < end);
1890
1891 // Check for TTEEF propagation in the time interval [min_begin, end)
1892 if (minTime <= min_begin && tteef_filt)
1893 tteef_bounds_propagation_ub(min_begin, end, min_en_avail, j, update_queue);
1894
1895 // TTEF Dominance rule for skipping time intervals
1896 // NOTE this rule can cut off TTEEF propagation
1897 if (jj < est_idx_last) {
1898 // Computing an over-estimate of the energy in the time interval [est_2[j], end)
1899 const int dom_wdays = (rho == 1 ? end - est_2[j] : rPeriods[est_2[j]] - rPeriods[end]);
1900 const int dom_en_comp = tt_after_est[0] - tt_after_est[jj + 1];
1901 const int dom_en_free = sumFreeEnergy[jj] + en_req;
1902 const int dom_en_avail = maxLimit * dom_wdays - dom_en_comp - dom_en_free;
1903 if (dom_en_avail >= min_en_avail && dom_en_avail >= maxEnergy)
1904 break;
1905 }
1906
1907 begin = est_2[j];
1908
1909 // Computing the required free energy of task 'j' in the
1910 // time interval [begin, end)
1911 if (lct_2[j] <= end) {
1912 // Task 'j' lies in the considered time interval
1913 en_req_free += free_energy2[j];
1914 } else {
1915 // Task might partially lie in the considered time interval
1916 const int cal_idx = taskCalendar[j] - 1;
1917 const int * wPeriods = workingPeriods[cal_idx];
1918 const int ect_in = min(end, ect_2[j]);
1919 int workDays_req_in = 0;
1920 // Add the compulsory part of 'j' to the required energy in the time interval [begin, end)
1921 if (lst_2[j] < ect_2[j]) {
1922 const int begin_comp = min(end, lst_2[j]);
1923 workDays_req_in += (rho == 1 ? ect_in - begin_comp : wPeriods[begin_comp] - wPeriods[ect_in]);
1924 }
1925
1926 // Computing the required energy in the time interval [begin, end)
1927 // considering the right shift
1928 if (shift_in == 1) {
1929 dur_shift = get_free_dur_right_shift2(begin, end, j);
1930 // Adjusting dur_shift if resource stays engaged
1931 if (rho == 1) {
1932 const int dur_fixed = max(0, ect_2[j] - lst_2[j]);
1933 dur_shift = min(min_energy2[j] / min_usage(j) - dur_fixed, dur_shift);
1934 }
1935 workDays_req_in += dur_shift;
1936 en_req_free += min_usage(j) * dur_shift;
1937 }
1938
1939 // Calculation of the additional required energy for starting at est_2[j]
1940 // in time window [begin, end)
1941 const int workDays_start = (rho == 1 ? ect_in - est_2[j] : wPeriods[est_2[j]] - wPeriods[ect_in]);
1942 const int en_req_start = min_usage(j) * (workDays_start - workDays_req_in);
1943 assert(workDays_start >= workDays_req_in);
1944 if (en_req_start > update_en_req_start) {
1945 update_en_req_start = en_req_start;
1946 update_workDays_req_in = workDays_req_in;
1947 update_idx = jj;
1948 }
1949 }
1950
1951 // Adding the energy from the time table profile (compulsory parts)
1952 en_req = en_req_free + tt_after_est[jj] - tt_after_lct[ii];
1953
1954 // Calculate the available energy in the time window [begin, end)
1955 workingDays = (rho == 1 ? end - begin : rPeriods[begin] - rPeriods[end]);
1956 en_avail = maxLimit * workingDays - en_req;
1957
1958 // Update the time window [., end) with the minimal available energy
1959 // Note is required for the TTEEF propagation
1960 if (min_en_avail > en_avail) {
1961 min_en_avail = en_avail;
1962 min_begin = begin;
1963 }
1964
1965 // Check for resource overload
1966 if (en_avail < 0) {
1967 consistent = false;
1968 ii = -1;
1969 break;
1970 }
1971
1972 // Check for a lower bound update for the start time
1973 if (en_avail < update_en_req_start) {
1974 // Reset 'j' to the task to be updated
1975 j = task_id_est[update_idx];
1976 // Calculation of the possible new lower bound wrt.
1977 // the current time interval [begin, end)
1978 const int en_avail_new = en_avail + update_workDays_req_in * min_usage(j);
1979 const int wdays_avail = en_avail_new / min_usage(j);
1980 const int start_new = ttef_get_new_start_time(begin, end, j, wdays_avail);
1981 // Check whether a new lower bound was found
1982 // - nfnl-rule TODO
1983 if (start_new > new_est[j]) {
1984 // Push possible update into the queue
1985 update_queue.push(TTEFUpdate(j, start_new, begin, end, true));
1986 new_est[j] = start_new;
1987 }
1988 }
1989 }
1990 }
1991
1992 delete[] sumFreeEnergy;
1993
1994 if (!consistent) {
1995 vec<Lit> expl;
1996 // Increment the inconsistency counter
1997 nb_ttef_incons++;
1998 if (so.lazy) {
1999 list<TaskDur> tasks_tw;
2000 list<TaskDur> tasks_cp;
2001 int en_req1 = 0;
2002 // Retrieve tasks involved
2003 en_req1 = ttef_retrieve_tasks(shift_in, begin, end, -1, tasks_tw, tasks_cp);
2004 assert(en_req1 >= en_req);
2005 // Calculate the lifting
2006 int breaks = end - begin - workingDays;
2007 int en_lift = en_req1 - 1 - maxLimit * (end - begin - breaks);
2008 assert(en_lift >= 0);
2009 // Explaining the overload
2010 ttef_analyse_limit_and_tasks(begin, end, breaks, tasks_tw, tasks_cp, en_lift, expl);
2011 assert(expl.size() > 0);
2012 }
2013 // Submitting of the conflict explanation
2014 submit_conflict_explanation(expl);
2015 #if CUMUVERB > 0
2016 fprintf(stderr, "TTEF Inconsistency detected LB");
2017 #endif
2018 }
2019 return consistent;
2020 }
2021
2022 bool
ttef_bounds_propagation_ub(int shift_in,std::queue<TTEFUpdate> & update_queue)2023 CumulativeCalProp::ttef_bounds_propagation_ub(
2024 int shift_in,
2025 std::queue<TTEFUpdate> & update_queue
2026 ) {
2027 assert(last_unfixed > 0);
2028 assert(shift_in == 0 || shift_in == 2);
2029
2030 // Some constants
2031 const int maxLimit = max_limit();
2032 const int * rPeriods = workingPeriods[resCalendar - 1];
2033
2034 // Some variables
2035 // Begin and end of the time interval [begin, end)
2036 int begin, end = -1, dur_shift;
2037 int lct_idx_last = 0;
2038 int i, j, en_req, en_avail;
2039 int en_req_free;
2040 int update_en_req_end, update_idx, update_workDays_req_in;
2041 int min_en_avail = -1, min_end = minTime - 1;
2042 int workingDays = 0;
2043 bool consistent = true;
2044
2045 int maxEnergy = 0, est_idx_last = -1;
2046 int maxLength = 0;
2047 int* sumFreeEnergy = new int[last_unfixed + 2];
2048 sumFreeEnergy[last_unfixed + 1] = 0;
2049 for (int ii = last_unfixed; ii >= 0; ii--) {
2050 const int i = task_id_lct[ii];
2051 maxLength = (rho == 1 ? max(lct_2[i] - lst_2[i], ect_2[i] - est_2[i]) : min_dur(i));
2052 maxEnergy = max(maxEnergy, min_usage(i) * maxLength);
2053 sumFreeEnergy[ii] = sumFreeEnergy[ii + 1] + free_energy2[i];
2054 }
2055
2056 begin = est_2[task_id_est[0]] - 1;
2057
2058 // Outer Loop: iterating over est in non-decreasing order
2059 //
2060 for (int ii = 0; ii <= last_unfixed; ii++) {
2061 i = task_id_est[ii];
2062 if (begin == est_2[i]) continue;
2063
2064 // Dominance rule for skipping time intervals
2065 if (min_en_avail >= 0) {
2066 const int dom_wdays = (rho == 1 ? est_2[i] - begin : rPeriods[begin] - rPeriods[est_2[i]]);
2067 const int dom_en_comp = tt_after_est[est_idx_last] - tt_after_est[ii];
2068 const int dom_en_avail = maxLimit * dom_wdays - dom_en_comp;
2069 if (min_en_avail - dom_en_avail >= maxEnergy)
2070 continue;
2071 }
2072 est_idx_last = ii;
2073
2074 // Intialisation for the minimal avaible energy of a time interval starting
2075 // at begin
2076 min_en_avail = maxLimit * (lct_2[task_id_lct[last_unfixed]] - est_2[task_id_est[0]]);
2077 min_end = minTime - 1;
2078
2079 begin = est_2[i];
2080 while (lct_2[task_id_lct[lct_idx_last]] <= begin) lct_idx_last++;
2081
2082 // Initialisations for the inner loop
2083 en_req = 0;
2084 en_req_free = 0;
2085 en_avail = -1;
2086 update_idx = -1;
2087 update_en_req_end = -1;
2088 update_workDays_req_in = -1;
2089
2090 // Inner Loop: iterating over lct in non-decreasing order
2091 //
2092 for (int jj = lct_idx_last; jj <= last_unfixed; jj++) {
2093 nb_ttef_ub_calls++;
2094 j = task_id_lct[jj];
2095
2096 assert(lct_2[j] > begin);
2097
2098 // Check for TTEEF propagation in the time interval [begin, min_end)
2099 if (minTime <= min_end && tteef_filt)
2100 tteef_bounds_propagation_lb(begin, min_end, min_en_avail, j, update_queue);
2101
2102 // TTEF Dominance rule for skipping time intervals
2103 // NOTE this rule can cut off TTEEF propagation
2104 if (jj > lct_idx_last) {
2105 // Computing an over-estimate of the energy in the time interval [begin, lct_2[j])
2106 const int dom_wdays = (rho == 1 ? lct_2[j] - begin : rPeriods[begin] - rPeriods[lct_2[j]]);
2107 const int dom_en_comp = tt_after_lct[jj - 1];
2108 const int dom_en_free = sumFreeEnergy[jj] + en_req;
2109 const int dom_en_avail = maxLimit * dom_wdays - dom_en_comp - dom_en_free;
2110 if (dom_en_avail >= min_en_avail && dom_en_avail >= maxEnergy)
2111 break;
2112 }
2113
2114 // Update end
2115 end = lct_2[j];
2116
2117 // Computing the required free energy of task 'j' in the
2118 // time interval [begin, end)
2119 if (begin <= est_2[j]) {
2120 // Task lies in the considered time interval [begin, end)
2121 en_req_free += free_energy2[j];
2122 } else {
2123 // Task might partially lie in the considered time interval
2124 const int cal_idx = taskCalendar[j] - 1;
2125 const int * wPeriods = workingPeriods[cal_idx];
2126 const int lst_in = max(begin, lst_2[j]);
2127 int workDays_req_in = 0;
2128 // Add the compulsory part of 'j' to the required energy in the time interval [begin, end)
2129 if (lst_2[j] < ect_2[j]) {
2130 const int end_comp = max(begin, ect_2[j]);
2131 workDays_req_in += (rho == 1 ? end_comp - lst_in : wPeriods[lst_in] - wPeriods[end_comp]);
2132 }
2133
2134 // Computing the required energy in the time interval [begin, end)
2135 // considering the lef shift
2136 if (shift_in == 2) {
2137 dur_shift = get_free_dur_left_shift2(begin, end, j);
2138 // Adjusting dur_shift if resource stays engaged
2139 if (rho == 1) {
2140 const int dur_fixed = max(0, ect_2[j] - lst_2[j]);
2141 dur_shift = min(min_energy2[j] / min_usage(j) - dur_fixed, dur_shift);
2142 }
2143 workDays_req_in += dur_shift;
2144 en_req_free += min_usage(j) * dur_shift;
2145 }
2146
2147 // Calculation of the additional required energy for ending at lct_2[j]
2148 // in time window [begin, end)
2149 const int workDays_end = (rho == 1 ? lct_2[j] - lst_in : wPeriods[lst_in] - wPeriods[lct_2[j]]);
2150 const int en_req_end = min_usage(j) * (workDays_end - workDays_req_in);
2151 assert(workDays_end >= workDays_req_in);
2152 if (en_req_end > update_en_req_end) {
2153 update_en_req_end = en_req_end;
2154 update_workDays_req_in = workDays_req_in;
2155 update_idx = jj;
2156 }
2157 }
2158
2159 // Adding the energy from the time table profile (compulsory parts)
2160 en_req = en_req_free + tt_after_est[ii] - tt_after_lct[jj];
2161
2162 // Calculate the available energy in the time interval [begin, end)
2163 workingDays = (rho == 1 ? end - begin : rPeriods[begin] - rPeriods[end]);
2164 en_avail = maxLimit * workingDays - en_req;
2165
2166 // Update the time window [begin, .) with the minimal available energy
2167 // Note is required for the TTEEF propagation
2168 if (min_en_avail > en_avail) {
2169 min_en_avail = en_avail;
2170 min_end = end;
2171 }
2172
2173 // Check for resource overload
2174 if (en_avail < 0) {
2175 consistent = false;
2176 ii = last_unfixed + 1;
2177 break;
2178 }
2179
2180 // Check for an upper bound update for the start time
2181 if (en_avail < update_en_req_end) {
2182 // Reset 'j' to the task to be updated
2183 j = task_id_lct[update_idx];
2184 // Calculation of the possible upper bound wrt.
2185 // the current time interval [begin , end)
2186 const int en_avail_new = en_avail + update_workDays_req_in * min_usage(j);
2187 const int wdays_avail = en_avail_new / min_usage(j);
2188 const int end_new = ttef_get_new_end_time(begin, end, j, wdays_avail);
2189 // Check whether a new upper bound was found
2190 // - nfnl-rule TODO
2191 if (end_new < new_lct[j]) {
2192 // Push possible update into queue
2193 update_queue.push(TTEFUpdate(j, end_new, begin, end, false));
2194 new_lct[j] = end_new;
2195 }
2196 }
2197 }
2198 }
2199
2200 delete[] sumFreeEnergy;
2201
2202 if (!consistent) {
2203 vec<Lit> expl;
2204 // Increment the inconsistency counter
2205 nb_ttef_incons++;
2206 if (so.lazy) {
2207 list<TaskDur> tasks_tw;
2208 list<TaskDur> tasks_cp;
2209 int en_req1 = 0;
2210 // Retrieve tasks involved
2211 en_req1 = ttef_retrieve_tasks(shift_in, begin, end, -1, tasks_tw, tasks_cp);
2212 assert(en_req1 >= en_req);
2213 // Calculate the lifting
2214 int breaks = end - begin - workingDays;
2215 int en_lift = en_req1 - 1 - maxLimit * (end - begin - breaks);
2216 assert(en_lift >= 0);
2217 // Explaining the overload
2218 ttef_analyse_limit_and_tasks(begin, end, breaks, tasks_tw, tasks_cp, en_lift, expl);
2219 assert(expl.size() > 0);
2220 }
2221 // Submitting of the conflict explanation
2222 submit_conflict_explanation(expl);
2223 #if CUMUVERB > 0
2224 fprintf(stderr, "TTEF Inconsistency detected UB");
2225 #endif
2226 }
2227 return consistent;
2228 }
2229
2230 // Checking for TTEEF propagation on lower bound in the
2231 // time window [begin, end)
2232 void
tteef_bounds_propagation_lb(const int begin,const int end,const int en_avail,const int j,std::queue<TTEFUpdate> & update_queue)2233 CumulativeCalProp::tteef_bounds_propagation_lb(
2234 const int begin, const int end, const int en_avail, const int j,
2235 std::queue<TTEFUpdate> & update_queue
2236 ) {
2237 if (begin <= est_2[j] || ect_2[j] <= begin)
2238 return ;
2239
2240 // Some useful constants
2241 const int * wPeriods = workingPeriods[taskCalendar[j] - 1];
2242 const int est_in = max(begin, est_2[j]);
2243 const int ect_in = min(end, ect_2[j]);
2244 assert(est_in <= ect_in);
2245
2246 // Computing the compulsory part in the time interval [begin, end)
2247 int wdays_in = 0;
2248 if (lst_2[j] < ect_2[j]) {
2249 const int end_comp_in = max(begin, ect_in);
2250 wdays_in += (rho == 1 ? end_comp_in - est_in : wPeriods[est_in] - wPeriods[end_comp_in]);
2251 }
2252
2253 // Computing the working days in the time interval [begin, end) when
2254 // task 'j' is executed to its earliest start time
2255 const int wdays_start_in = (rho == 1 ? ect_in - est_in : wPeriods[est_in] - wPeriods[ect_in]);
2256 assert(wdays_start_in >= wdays_in);
2257
2258 // Checking for lower bound propagation
2259 if (en_avail < min_usage(j) * (wdays_start_in - wdays_in)) {
2260 // Calculate new lower bound
2261 const int wdays_avail = (en_avail / min_usage(j)) + wdays_in;
2262 const int est_new = ttef_get_new_start_time(begin, end, j, wdays_avail);
2263 // Check whether a new lower bound was found
2264 if (est_new > new_est[j]) {
2265 // Push possible update into the queue
2266 update_queue.push(TTEFUpdate(j, est_new, begin, end, true));
2267 new_est[j] = est_new;
2268 }
2269 }
2270 }
2271
2272 // Checking for TTEEF propagation on upper bound in the
2273 // time window [begin, end)
2274 void
tteef_bounds_propagation_ub(const int begin,const int end,const int en_avail,const int j,std::queue<TTEFUpdate> & update_queue)2275 CumulativeCalProp::tteef_bounds_propagation_ub(
2276 const int begin, const int end, const int en_avail, const int j,
2277 std::queue<TTEFUpdate> & update_queue
2278 ) {
2279 if (lst_2[j] >= end || lct_2[j] <= begin || est_2[j] >= begin)
2280 return ;
2281
2282 // Some useful constants
2283 const int * wPeriods = workingPeriods[taskCalendar[j] - 1];
2284 const int lst_in = max(begin, lst_2[j]);
2285 const int lct_in = min(end, lct_2[j]);
2286
2287 // Computing the compulsory part in time interval [begin, end)
2288 int wdays_in = 0;
2289 if (lst_2[j] < ect_2[j]) {
2290 const int end_comp_in = max(begin, lct_in);
2291 wdays_in += (rho == 1 ? end_comp_in - lst_in : wPeriods[lst_in] - wPeriods[end_comp_in]);
2292 }
2293
2294 // Computing the working days in the time interval [begin, end) when
2295 // task 'j' is executed to its latest start time
2296 const int wdays_end_in = (rho == 1 ? lct_in - lst_in : wPeriods[lst_in] - wPeriods[lct_in]);
2297 assert(wdays_end_in >= wdays_in);
2298
2299 // Checking for upper bound propagation
2300 if (en_avail < min_usage(j) * (wdays_end_in - wdays_in)) {
2301 // Calculate new upper bound
2302 const int wdays_avail = (en_avail / min_usage(j)) + wdays_in;
2303 const int lct_new = ttef_get_new_end_time(begin, end, j, wdays_avail);
2304 // Check whether a new upper bound was found
2305 if (lct_new < new_lct[j]) {
2306 // Push possible update into the queue
2307 update_queue.push(TTEFUpdate(j, lct_new, begin, end, false));
2308 new_lct[j] = lct_new;
2309 }
2310 }
2311 }
2312
2313 int
ttef_get_new_start_time(const int begin,const int end,const int task,const int min_wdays_in)2314 CumulativeCalProp::ttef_get_new_start_time(
2315 const int begin, const int end, const int task, const int min_wdays_in
2316 ) {
2317 assert(min_wdays_in >= 0);
2318 if (min_wdays_in == 0) {
2319 const int * cal = calendar[taskCalendar[task] - 1];
2320 int est = end;
2321 while (est <= maxTime && cal[est] == 0)
2322 est++;
2323 return est;
2324 }
2325 if (rho == 0) {
2326 // Resource is released
2327 return getStartTimeForEndTime(task, end, min_wdays_in);
2328 }
2329 // Resource stays engaged
2330 const int * cal = calendar[taskCalendar[task] - 1];
2331 const int begin_in = max(begin, est_2[task]);
2332 const int end_in = min(end, ect_2[task]);
2333 assert(begin_in < end_in);
2334 int wdays_in = end_in - begin_in;
2335 assert(wdays_in > min_wdays_in);
2336 //const int max_est = min(max_start0(task), end - min_wdays_in);
2337 const int max_est = max_start0(task);
2338 int last_est = est_2[task];
2339 int last_wdays_in = wdays_in;
2340 int est = est_2[task] + 1;
2341 int ect = ect_2[task] + 1;
2342
2343 for (; est <= max_est; est++, ect++) {
2344 // Updating the working days
2345 assert(cal[est - 1] == 1);
2346 if (begin <= last_est)
2347 wdays_in--;
2348 // Computing the new start time and updating the working days
2349 while (cal[est] == 0 && est <= max_est) {
2350 if (begin <= est)
2351 wdays_in--;
2352 est++;
2353 }
2354 if (est > max_est)
2355 return last_est;
2356 // Computing the new end time and updating the working days
2357 assert(cal[ect - 2] == 1);
2358 while (cal[ect - 1] == 0) {
2359 if (ect <= end)
2360 wdays_in++;
2361 ect++;
2362 }
2363 // Updating the working days
2364 if (ect <= end)
2365 wdays_in++;
2366 // Checking working days
2367 if (wdays_in == min_wdays_in || (last_wdays_in > min_wdays_in && wdays_in < min_wdays_in))
2368 return est;
2369 else if (wdays_in < min_wdays_in)
2370 return last_est;
2371 // Updating last valid earliest start time
2372 last_est = est;
2373 last_wdays_in = wdays_in;
2374 }
2375
2376 return last_est;
2377 }
2378
2379 int
ttef_get_new_end_time(const int begin,const int end,const int task,const int min_wdays_in)2380 CumulativeCalProp::ttef_get_new_end_time(
2381 const int begin, const int end, const int task, const int min_wdays_in
2382 ) {
2383 assert(min_wdays_in >= 0);
2384 if (min_wdays_in == 0) {
2385 const int * cal = calendar[taskCalendar[task] - 1];
2386 int lct = begin;
2387 while (minTime < lct && cal[lct - 1] == 0)
2388 lct--;
2389 return lct;
2390 }
2391 if (rho == 0) {
2392 // Resource is released
2393 return getEndTimeForStartTime(task, begin, min_wdays_in);
2394 }
2395 // Resource stays engaged
2396 const int * cal = calendar[taskCalendar[task] - 1];
2397 const int begin_in = max(begin, lst_2[task]);
2398 const int end_in = min(end, lct_2[task]);
2399 assert(begin_in < end_in);
2400 int wdays_in = end_in - begin_in;
2401 assert(wdays_in > min_wdays_in);
2402 const int lst0 = min_start0(task);
2403 int last_lct = lct_2[task];
2404 int last_wdays_in = wdays_in;
2405 int lst = lst_2[task] - 1;
2406 int lct = lct_2[task] - 1;
2407
2408 for (; lst <= lst0; lst--, lct--) {
2409 assert(cal[lst + 1] == 1);
2410 // Computing the new start time and updating the working days
2411 while (cal[lst] == 0 && lst0 <= lst) {
2412 if (begin <= lst)
2413 wdays_in++;
2414 lst++;
2415 }
2416 if (lst < lst0)
2417 return last_lct;
2418 // Updating the working days
2419 if (begin <= lst)
2420 wdays_in++;
2421 // Updating the working days
2422 if (lct < end)
2423 wdays_in--;
2424 // Computing the new end time and updating the working days
2425 assert(cal[lct] == 1);
2426 while (cal[lct - 1] == 0) {
2427 if (lct <= end)
2428 wdays_in--;
2429 lct--;
2430 }
2431 // Checking the working days
2432 if (wdays_in == min_wdays_in || (last_wdays_in > min_wdays_in && wdays_in < min_wdays_in)) {
2433 return lct;
2434 } else if (wdays_in < min_wdays_in)
2435 return last_lct;
2436 // Updating the last valid latest completion time
2437 last_lct = lct;
2438 last_wdays_in = wdays_in;
2439 }
2440 return last_lct;
2441 }
2442
2443 void
ttef_explanation_for_update_lb(int shift_in,const int begin,const int end,const int task,int & bound,vec<Lit> & expl)2444 CumulativeCalProp::ttef_explanation_for_update_lb(
2445 int shift_in, const int begin, const int end, const int task, int & bound, vec<Lit> & expl
2446 ) {
2447 // Some constants
2448 const int maxLimit = max_limit();
2449 const int * rPeriods = workingPeriods[resCalendar - 1];
2450 const int * wPeriods = workingPeriods[taskCalendar[task] - 1];
2451
2452 // Some variables
2453 list<TaskDur> tasks_tw;
2454 list<TaskDur> tasks_cp;
2455
2456 // Retrieving tasks involved in the time interval [begin, end) excluding task 'task'
2457 const int en_req = ttef_retrieve_tasks(shift_in, begin, end, task, tasks_tw, tasks_cp);
2458
2459 // Calculating the available energy in the time interval [begin, end)
2460 const int wdays = (rho == 1 ? end - begin : rPeriods[begin] - rPeriods[end]);
2461 const int en_avail = maxLimit * wdays - en_req;
2462 const int breaks = end - begin - wdays;
2463
2464 // Calculating the working days available for the task 'task' in the considered time interval
2465 const int wdays_avail = en_avail / min_usage(task);
2466 const int min_wdays_in = wdays_avail + 1;
2467
2468 // Determining the new lower bound on the start time
2469 const int new_lb = ttef_get_new_start_time(begin, end, task, wdays_avail);
2470
2471 // Some consistency checks
2472 assert(new_lb >= bound);
2473 assert(rho == 0 || en_avail < min_usage(task) * (min(end, ect_2[task]) - max(begin, est_2[task])));
2474 assert(rho == 1 || en_avail < min_usage(task) * (wPeriods[max(begin, est_2[task])] - wPeriods[min(end, ect_2[task])]));
2475
2476 // Calculating the explanation lower bound on the start time
2477 int expl_wdays_in;
2478 int expl_lb;
2479 switch (ttef_expl_deg) {
2480 case ED_NORMAL:
2481 case ED_LIFT:
2482 expl_lb = ttef_analyse_tasks_left_shift(begin, end, min_wdays_in, task, 0, expl_wdays_in);
2483 case ED_NAIVE:
2484 default:
2485 expl_lb = est_2[task];
2486 const int expl_begin = max(begin, expl_lb);
2487 const int expl_end = min(end, ect_2[task]);
2488 expl_wdays_in = (rho == 1 ? expl_end - expl_begin : wPeriods[expl_begin] - wPeriods[expl_end]);
2489 }
2490
2491 // Calculating the lifting energy for the remainder
2492 int en_lift = min_usage(task) - 1 - (en_avail % min_usage(task));
2493 en_lift += min_usage(task) * (expl_wdays_in - wdays_avail - 1);
2494
2495 // More consistency checks
2496 assert(expl_lb <= est_2[task]);
2497 assert(expl_wdays_in >= wdays_avail + 1);
2498 assert(en_lift >= 0);
2499
2500 // Explaining the update for task 'task'
2501 if (expl_lb > min_start0(task)) {
2502 // start[task] >= expl_lb
2503 expl.push(getNegGeqLit(start[task], expl_lb));
2504 }
2505 // Get the negated literal for [[dur[task] >= min_dur(task)]]
2506 if (min_dur0(task) < min_dur(task))
2507 expl.push(getNegGeqLit(dur[task], min_dur(task)));
2508 // Get the negated literal for [[usage[task] >= min_usage(task)]]
2509 if (min_usage0(task) < min_usage(task))
2510 expl.push(getNegGeqLit(usage[task], min_usage(task)));
2511
2512 // Retrieve explanation for the remaining tasks
2513 ttef_analyse_limit_and_tasks(begin, end, breaks, tasks_tw, tasks_cp, en_lift, expl);
2514
2515 // Assigning new lower bound
2516 bound = new_lb;
2517 }
2518
2519 void
ttef_explanation_for_update_ub(int shift_in,const int begin,const int end,const int task,int & bound,vec<Lit> & expl)2520 CumulativeCalProp::ttef_explanation_for_update_ub(
2521 int shift_in, const int begin, const int end, const int task, int & bound, vec<Lit> & expl
2522 ) {
2523 // Some constants
2524 const int maxLimit = max_limit();
2525 const int * rPeriods = workingPeriods[resCalendar - 1];
2526 const int * wPeriods = workingPeriods[taskCalendar[task] - 1];
2527
2528 // Some variables
2529 list<TaskDur> tasks_tw;
2530 list<TaskDur> tasks_cp;
2531
2532 // Retrieving tasks involved in the time interval [begin, end) excluding task 'task'
2533 const int en_req = ttef_retrieve_tasks(shift_in, begin, end, task, tasks_tw, tasks_cp);
2534
2535 // Calculating the available energy in the time interval [begin, end)
2536 const int wdays = (rho == 1 ? end - begin : rPeriods[begin] - rPeriods[end]);
2537 const int en_avail = maxLimit * wdays - en_req;
2538 const int breaks = end - begin - wdays;
2539
2540 // Calculating the working days available for the task 'task' in the considered time interval
2541 const int wdays_avail = en_avail / min_usage(task);
2542 const int min_wdays_in = wdays_avail + 1;
2543
2544 // Determining the new upper bound on the latest completion time
2545 const int new_lct = ttef_get_new_end_time(begin, end, task, wdays_avail);
2546
2547 // Some consistency checks
2548 assert(new_lct <= bound);
2549 assert(rho == 0 || en_avail < min_usage(task) * (min(end, lct_2[task]) - max(begin, lst_2[task])));
2550 assert(rho == 1 || en_avail < min_usage(task) * (wPeriods[max(begin, lst_2[task])] - wPeriods[min(end, lct_2[task])]));
2551
2552 // Calculating the explanation lower bound on the start time
2553 int expl_wdays_in;
2554 int expl_ub;
2555 switch (ttef_expl_deg) {
2556 case ED_NORMAL:
2557 case ED_LIFT:
2558 expl_ub = ttef_analyse_tasks_right_shift(begin, end, min_wdays_in, task, 0, expl_wdays_in);
2559 case ED_NAIVE:
2560 default:
2561 expl_ub = lst_2[task];
2562 const int expl_begin = max(begin, expl_ub);
2563 const int expl_end = min(end, lct_2[task]);
2564 expl_wdays_in = (rho == 1 ? expl_end - expl_begin : wPeriods[expl_begin] - wPeriods[expl_end]);
2565 }
2566
2567 // Calculating the lifting energy for the remainder
2568 int en_lift = min_usage(task) - 1 - (en_avail % min_usage(task));
2569 en_lift += min_usage(task) * (expl_wdays_in - wdays_avail - 1);
2570
2571 // More consistency checks
2572 assert(expl_ub >= lst_2[task]);
2573 assert(expl_wdays_in >= wdays_avail + 1);
2574 assert(en_lift >= 0);
2575
2576 // Explaining the update for task 'task'
2577 if (expl_ub < max_start0(task)) {
2578 // start[task] <= expl_ub
2579 expl.push(getNegLeqLit(start[task], expl_ub));
2580 }
2581 // Get the negated literal for [[dur[task] >= min_dur(task)]]
2582 if (min_dur0(task) < min_dur(task))
2583 expl.push(getNegGeqLit(dur[task], min_dur(task)));
2584 // Get the negated literal for [[usage[task] >= min_usage(task)]]
2585 if (min_usage0(task) < min_usage(task))
2586 expl.push(getNegGeqLit(usage[task], min_usage(task)));
2587
2588 // Retrieve explanation for the remaining tasks
2589 ttef_analyse_limit_and_tasks(begin, end, breaks, tasks_tw, tasks_cp, en_lift, expl);
2590
2591 // Assigning new lower bound
2592 bound = new_lct;
2593 }
2594
2595 bool
ttef_update_bounds(int shift_in,std::queue<TTEFUpdate> & queue_update)2596 CumulativeCalProp::ttef_update_bounds(
2597 int shift_in,
2598 std::queue<TTEFUpdate> & queue_update
2599 ) {
2600 while (!queue_update.empty()) {
2601 const int task = queue_update.front().task;
2602 int bound = queue_update.front().bound_new;
2603 const int begin = queue_update.front().tw_begin;
2604 const int end = queue_update.front().tw_end;
2605 Clause * reason = NULL;
2606 if (queue_update.front().is_lb_update) {
2607 // Lower bound update
2608 if (new_est[task] == bound) {
2609 if (so.lazy) {
2610 vec<Lit> expl;
2611 ttef_explanation_for_update_lb(shift_in, begin, end, task, bound, expl);
2612 reason = get_reason_for_update(expl);
2613 }
2614 nb_ttef_filt++;
2615 // Update the lower bound
2616 if (!start[task]->setMin(bound, reason)) {
2617 // Conflict occurred
2618 return false;
2619 }
2620 // Set bound_update to true
2621 bound_update = true;
2622 #if CUMUVERB > 0
2623 fprintf(stderr, "Bounds Update LB\n");
2624 #endif
2625 }
2626 } else {
2627 // Upper bound update
2628 if (new_lct[task] == bound) {
2629 if (so.lazy) {
2630 vec<Lit> expl;
2631 ttef_explanation_for_update_ub(shift_in, begin, end, task, bound, expl);
2632 reason = get_reason_for_update(expl);
2633 }
2634 // Update the lower bound
2635 const int new_ub = getStartTimeForEndTime(task, bound, min_dur(task));
2636 #if CUMUVERB > 0
2637 fprintf(stderr, "Bounds Update UB: task = %d, old = %d, new = %d \n",task, lst_2[task], new_ub);
2638 #endif
2639 nb_ttef_filt++;
2640 if (!start[task]->setMax(new_ub, reason)) {
2641 // Conflict occurred
2642 return false;
2643 }
2644 // Set bound_update to true
2645 bound_update = true;
2646 }
2647 }
2648 queue_update.pop();
2649 }
2650
2651 return true;
2652 }
2653
2654 int
ttef_retrieve_tasks(const int shift_in,const int begin,const int end,const int fb_id,list<TaskDur> & tasks_tw,list<TaskDur> & tasks_cp)2655 CumulativeCalProp::ttef_retrieve_tasks(
2656 const int shift_in,
2657 const int begin, const int end, const int fb_id, list<TaskDur> & tasks_tw, list<TaskDur> & tasks_cp)
2658 {
2659 int en_req = 0;
2660 int dur_comp, dur_shift, dur_in;
2661 // Getting fixed tasks
2662 for (int ii = 0; ii < task_id.size(); ii++) {
2663 const int i = task_id[ii];
2664 if (i == fb_id || lct_2[i] <= begin || end <= est_2[i])
2665 continue;
2666 if (begin <= est_2[i] && lct_2[i] <= end) {
2667 // Task lies in the time interval [begin, end)
2668 en_req += min_energy2[i];
2669 const int usedDays = min_energy2[i] / min_usage(i);
2670 tasks_tw.push_back(TaskDur(i, usedDays));
2671 continue;
2672 }
2673 if (lst_2[i] < ect_2[i] && is_intersecting(begin, end, lst_2[i], ect_2[i])) {
2674 // Compulsory part partially or fully lies in [begin, end)
2675 const int begin_comp = max(begin, lst_2[i]);
2676 const int end_comp = min(end, ect_2[i]);
2677 dur_comp = end_comp - begin_comp;
2678 if (rho == 0) {
2679 const int cal_idx = taskCalendar[i] - 1;
2680 dur_comp = workingPeriods[cal_idx][begin_comp] - workingPeriods[cal_idx][end_comp];
2681 }
2682 dur_shift = 0;
2683 if (shift_in == 1) {
2684 dur_shift = get_free_dur_right_shift2(begin, end, i);
2685 assert(begin <= est_2[i] || dur_shift == 0);
2686 // Adjusting dur_shift if the resource stays engaged
2687 if (rho == 1) {
2688 const int dur_fixed = max(0, ect_2[i] - lst_2[i]);
2689 dur_shift = min(min_energy2[i] / min_usage(i) - dur_fixed, dur_shift);
2690 }
2691 } else {
2692 assert(shift_in == 2);
2693 dur_shift = get_free_dur_left_shift2(begin, end, i);
2694 // Adjusting dur_shift if the resource stays engaged
2695 if (rho == 1) {
2696 const int dur_fixed = max(0, ect_2[i] - lst_2[i]);
2697 dur_shift = min(min_energy2[i] / min_usage(i) - dur_fixed, dur_shift);
2698 }
2699 }
2700 dur_in = dur_comp + dur_shift;
2701 en_req += min_usage(i) * dur_in;
2702 tasks_cp.push_back(TaskDur(i, dur_in));
2703 continue;
2704 }
2705 // Task 'i' should not have a compulsory part overlapping the time window [begin, end)
2706 dur_in = 0;
2707 if (shift_in == 1) {
2708 dur_in = get_free_dur_right_shift2(begin, end, i);
2709 assert(begin <= est_2[i] || dur_in == 0);
2710 // Adjusting dur_shift if the resource stays engaged
2711 if (rho == 1) {
2712 const int dur_fixed = max(0, ect_2[i] - lst_2[i]);
2713 dur_in = min(min_energy2[i] / min_usage(i) - dur_fixed, dur_in);
2714 }
2715 } else {
2716 assert(shift_in == 2);
2717 dur_in = get_free_dur_left_shift2(begin, end, i);
2718 assert(lct_2[i] <= end || dur_in == 0);
2719 // Adjusting dur_shift if the resource stays engaged
2720 if (rho == 1) {
2721 const int dur_fixed = max(0, ect_2[i] - lst_2[i]);
2722 dur_in = min(min_energy2[i] / min_usage(i) - dur_fixed, dur_in);
2723 }
2724 }
2725 if (0 < dur_in) {
2726 // Task partially lies in [begin, end)
2727 en_req += min_usage(i) * dur_in;
2728 tasks_tw.push_back(TaskDur(i, dur_in));
2729 }
2730 }
2731 return en_req;
2732 }
2733
2734 void
ttef_analyse_limit_and_tasks(const int begin,const int end,const int breaks,list<TaskDur> & tasks_tw,list<TaskDur> & tasks_cp,int & en_lift,vec<Lit> & expl)2735 CumulativeCalProp::ttef_analyse_limit_and_tasks(const int begin, const int end, const int breaks, list<TaskDur> & tasks_tw,
2736 list<TaskDur> & tasks_cp, int & en_lift, vec<Lit> & expl)
2737 {
2738 // Getting explanation for tasks in the time window
2739 ttef_analyse_tasks(begin, end, tasks_tw, en_lift, expl);
2740 // Getting explanation for tasks with compulsory parts
2741 ttef_analyse_tasks(begin, end, tasks_cp, en_lift, expl);
2742 // Getting explanation for the resource capacity
2743 int diff_limit = max_limit0() - max_limit();
2744 if (diff_limit > 0) {
2745 // Calculate possible lifting
2746 int lift_limit = min(en_lift / (end - begin - breaks), diff_limit);
2747 en_lift -= lift_limit * (end - begin - breaks);
2748 assert(en_lift >= 0);
2749 if (lift_limit < diff_limit) {
2750 // limit[%d] <= max_limit() + lift_limit
2751 expl.push(getNegLeqLit(limit, max_limit() + lift_limit));
2752 }
2753 }
2754 }
2755
2756 int
ttef_analyse_tasks_right_shift(const int begin,const int end,const int dur_in,const int task,const int max_dur_lift,int & last_dur)2757 CumulativeCalProp::ttef_analyse_tasks_right_shift(const int begin, const int end, const int dur_in, const int task, const int max_dur_lift, int & last_dur)
2758 {
2759 // Some assumptions
2760 assert(est_2[task] < end && begin < lct_2[task]);
2761
2762 // Defining some constants
2763 const int lst0 = max_start0(task);
2764 if (dur_in <= max_dur_lift) {
2765 last_dur = 0;
2766 return lst0;
2767 }
2768 // Defining more constants
2769 const int cal_idx = taskCalendar[task] - 1;
2770 const int * wPeriods = workingPeriods[cal_idx];
2771 const int * tCal = calendar[cal_idx];
2772 const int min_dur_in = dur_in - max_dur_lift;
2773 const int begin_in = max(begin, min(lst_2[task], end));
2774 const int end_in = min(lct_2[task], end);
2775 // Defining some variables
2776 int workDays = (rho == 1 ? end_in - begin_in : wPeriods[begin_in] - wPeriods[end_in]);
2777 int last_lst = lst_2[task];
2778 last_dur = workDays;
2779 int lst = lst_2[task] + 1;
2780 int lct = lct_2[task] + 1;
2781
2782 assert(workDays >= dur_in);
2783
2784 // Determining the latest possible start time and the number of workDays in the time window [begin, end)
2785 for (; lst <= lst0; lst++, lct++) {
2786 if (last_lst >= begin)
2787 workDays--;
2788 // Determining the new start time
2789 assert(tCal[lst - 1] == 1);
2790 while (tCal[lst] == 0 && lst <= lst0) {
2791 if (rho == 1 && lst >= begin)
2792 workDays--;
2793 lst++;
2794 }
2795 if (lst > lst0) {
2796 return last_lst;
2797 }
2798 // Determining the new end time
2799 assert(tCal[lct - 2] == 1);
2800 while (tCal[lct - 1] == 0) {
2801 if (rho == 1 && lct <= end)
2802 workDays++;
2803 lct++;
2804 }
2805 if (lct <= end)
2806 workDays++;
2807 // Check the number of working days in the time window [begin, end)
2808 if (workDays < min_dur_in) {
2809 return last_lst;
2810 }
2811 // Saving valid shift
2812 last_lst = lst;
2813 last_dur = workDays;
2814
2815 // Some cross checks
2816 assert(min_dur(task) == wPeriods[last_lst] - wPeriods[lct]);
2817 assert(rho == 0 || workDays == min(end, lct) - max(begin, last_lst));
2818 assert(rho == 1 || workDays == wPeriods[max(begin, last_lst)] - wPeriods[min(end, lct)]);
2819 assert(ttef_analyse_tasks_check_expl_ub(begin, end, task, min_dur_in, last_lst));
2820 }
2821 return last_lst;
2822 }
2823
2824 int
ttef_analyse_tasks_left_shift(const int begin,const int end,const int dur_in,const int task,const int max_dur_lift,int & last_dur)2825 CumulativeCalProp::ttef_analyse_tasks_left_shift(const int begin, const int end, const int dur_in, const int task, const int max_dur_lift, int & last_dur)
2826 {
2827 // Determining the earliest start time so that a certain number of work days are within the time window [begin, end)
2828 assert(est_2[task] < end && begin < lct_2[task]);
2829 const int est0 = min_start0(task);
2830 if (dur_in <= max_dur_lift) {
2831 last_dur = 0;
2832 return est0;
2833 }
2834 // Some useful constants
2835 const int cal_idx = taskCalendar[task] - 1;
2836 const int * wPeriods = workingPeriods[cal_idx];
2837 const int * tCal = calendar[cal_idx];
2838 const int min_dur_in = dur_in - max_dur_lift;
2839 const int end_in = min(ect_2[task], end);
2840 const int begin_in = max(est_2[task], begin);
2841 int wdays = (rho == 1 ? end_in - begin_in : wPeriods[begin_in] - wPeriods[end_in]);
2842 int last_est = est_2[task];
2843 last_dur = wdays;
2844 int ect = ect_2[task] - 1;
2845 int est = est_2[task] - 1;
2846 for (; est >= est0; est--, ect--) {
2847 assert(tCal[last_est] == 1);
2848 // Determining the new start time and updating the number of working days
2849 while (tCal[est] == 0 && est >= est0) {
2850 if (rho == 1 && est >= begin)
2851 wdays++;
2852 est--;
2853 }
2854 if (est < est0) {
2855 return last_est;
2856 }
2857 if (est >= begin)
2858 wdays++;
2859 // Determining the new end time and updating the number of working days
2860 assert(tCal[ect] == 1);
2861 if (ect < end)
2862 wdays--;
2863 while (tCal[ect - 1] == 0) {
2864 if (rho == 1 && ect <= end)
2865 wdays--;
2866 ect--;
2867 }
2868 // Check the number of working days in the time window [begin, end)
2869 if (wdays < min_dur_in) {
2870 return last_est;
2871 }
2872 // Saving last valid shift
2873 last_est = est;
2874 last_dur = wdays;
2875 // Some consistency checks
2876 assert(min_dur(task) == wPeriods[last_est] - wPeriods[ect]);
2877 assert(rho == 1 || wdays == wPeriods[max(last_est, begin)] - wPeriods[min(ect, end)]);
2878 assert(rho == 0 || wdays == min(ect, end) - max(last_est, begin));
2879 assert(ttef_analyse_tasks_check_expl_lb(begin, end, task, min_dur_in, last_est));
2880 }
2881 return last_est;
2882 }
2883
2884 bool
ttef_analyse_tasks_check_expl_lb(const int begin,const int end,const int task,const int dur_in,const int expl_lb)2885 CumulativeCalProp::ttef_analyse_tasks_check_expl_lb(const int begin, const int end, const int task, const int dur_in, const int expl_lb) {
2886 const int cal_idx = taskCalendar[task] - 1;
2887 const int ect = getEndTimeForStartTime(task, expl_lb, min_dur(task));
2888 const int begin_expl = max(begin, expl_lb);
2889 const int end_expl = max(begin, min(end, ect));
2890 const int dur_expl_in = (rho == 1 ? end_expl - begin_expl : workingPeriods[cal_idx][begin_expl] - workingPeriods[cal_idx][end_expl]);
2891 if (dur_in > dur_expl_in) {
2892 #if CUMUVERB > 2
2893 printf("xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n");
2894 printf("EXPL LB\n");
2895 printf(" tw [%d, %d); expl_lb %d\n", begin, end, expl_lb);
2896 printf(" task %d: start [%d, %d]; end [%d, %d];\n", task, est_2[task], lst_2[task], ect_2[task], lct_2[task]);
2897 printf(" start0 [%d, %d]\n", min_start0(task), max_start0(task));
2898 printf(" min_dur %d; dur_in %d;\n", min_dur(task), dur_in);
2899 printf(" min_energy2 %d; min_usage %d;\n", min_energy2[task], min_usage(task));
2900 printf(" tw_expl [%d, %d]; dur_expl_in %d, rho %d\n", begin_expl, end_expl, dur_expl_in, rho);
2901 for (int i = max(minTime, begin - 5); i < min(maxTime, end + 5); i++) {
2902 printf("%d ", calendar[cal_idx][i]);
2903 }
2904 printf("\n");
2905 #endif
2906 return false;
2907 }
2908 return true;
2909 }
2910
2911 bool
ttef_analyse_tasks_check_expl_ub(const int begin,const int end,const int task,const int dur_in,const int expl_ub)2912 CumulativeCalProp::ttef_analyse_tasks_check_expl_ub(const int begin, const int end, const int task, const int dur_in, const int expl_ub) {
2913 const int cal_idx = taskCalendar[task] - 1;
2914 const int lct = getEndTimeForStartTime(task, expl_ub, min_dur(task));
2915 const int end_expl = min(lct, end);
2916 const int lst = max(begin, min(end, expl_ub));
2917 const int dur_expl_in = (rho == 1 ? end_expl - lst : workingPeriods[cal_idx][lst] - workingPeriods[cal_idx][end_expl]);
2918 if (dur_in > dur_expl_in) {
2919 #if CUMUVERB > 2
2920 printf("xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\n");
2921 printf("EXPL UB\n");
2922 printf(" tw [%d, %d); expl_ub %d\n", begin, end, expl_ub);
2923 printf(" task %d: start [%d, %d]; end [%d, %d];\n", task, est_2[task], lst_2[task], ect_2[task], lct_2[task]);
2924 printf(" start0 [%d, %d]\n", min_start0(task), max_start0(task));
2925 printf(" min_dur %d; dur_in %d;\n", min_dur(task), dur_in);
2926 printf(" min_energy2 %d; min_usage %d;\n", min_energy2[task], min_usage(task));
2927 printf(" lst [%d, %d]; dur_expl_in %d, rho %d\n", lst, end_expl, dur_expl_in, rho);
2928 for (int i = max(minTime, begin - 5); i < min(maxTime, end + 5); i++) {
2929 printf("%d ", calendar[cal_idx][i]);
2930 }
2931 printf("\n");
2932 #endif
2933 return false;
2934 }
2935 return true;
2936 }
2937
2938 void
ttef_analyse_tasks(const int begin,const int end,list<TaskDur> & tasks,int & en_lift,vec<Lit> & expl)2939 CumulativeCalProp::ttef_analyse_tasks(const int begin, const int end, list<TaskDur> & tasks, int & en_lift, vec<Lit> & expl) {
2940 while (!tasks.empty()) {
2941 const int i = tasks.front().task;
2942 int dur_in = tasks.front().dur_in;
2943 int expl_lb, expl_ub;
2944 int est0 = min_start0(i);
2945 int lst0 = max_start0(i);
2946 // TTEF_cal: running variable for loops t, storages for execution times sto1 and sto2
2947 int t, sto1, sto2;
2948 // Calculate possible lifting
2949 // TTEF_cal: several changes were necessary
2950 switch (ttef_expl_deg) {
2951 case ED_NORMAL:
2952 // XXX Is min_dur correct
2953 if (rho == 1) {
2954 // Resource stays engaged
2955 sto1 = workingPeriods[taskCalendar[i]-1][begin] - workingPeriods[taskCalendar[i]-1][begin + dur_in];
2956 sto2 = min_dur(i) - sto1;
2957 sto1 = 0;
2958 t = begin;
2959 while(sto1 < sto2 && t > 0){
2960 if (calendar[taskCalendar[i]-1][t-1] == 1) sto1++;
2961 t--;
2962 }
2963 expl_lb = min(est_2[i], t);
2964 expl_ub = lst_2[i];//max(lst_2[i], end - dur_in);
2965 } else {
2966 // Resource is released
2967 sto1 = 0;
2968 sto2 = min_dur(i) - dur_in;
2969 t = begin;
2970 while(sto1 < sto2 && t > 0){
2971 if(calendar[taskCalendar[i]-1][t-1]==1) sto1++;
2972 t--;
2973 }
2974 expl_lb = min(est_2[i], t);
2975 sto1 = 0;
2976 sto2 = dur_in;
2977 t = end;
2978 while(sto1 < sto2 && t > 0){
2979 if(calendar[taskCalendar[i]-1][t-1]==1) sto1++;
2980 t--;
2981 }
2982 expl_ub = max(lst_2[i], t);
2983 }
2984 //expl_lb = begin + dur_in - min_dur(i); expl_ub = end - dur_in;
2985 break;
2986 //-----------------------------------------------------------
2987 case ED_LIFT:
2988 {
2989 int dur_in_lb = 0;
2990 int dur_in_ub = 0;
2991 // Computing maximal lift for the work days inside the time window [begin, end)
2992 const int max_lift = en_lift / min_usage(i);
2993 // Computing the lifted lower and upper bound on the start time
2994 expl_lb = ttef_analyse_tasks_left_shift( begin, end, dur_in, i, max_lift, dur_in_lb);
2995 expl_ub = ttef_analyse_tasks_right_shift(begin, end, dur_in, i, max_lift, dur_in_ub);
2996 // Some consistency checks
2997 assert(dur_in - dur_in_lb <= max_lift);
2998 assert(dur_in - dur_in_ub <= max_lift);
2999 assert(ttef_analyse_tasks_check_expl_lb(begin, end, i, min(dur_in_lb, dur_in_ub), expl_lb));
3000 assert(ttef_analyse_tasks_check_expl_ub(begin, end, i, min(dur_in_lb, dur_in_ub), expl_ub));
3001 // Computing the used lift
3002 const int dur_lift = dur_in - min(dur_in_lb, dur_in_ub);
3003 // Updating the remaining energy for lifting
3004 en_lift -= min_usage(i) * dur_lift;
3005 }
3006 break;
3007 //-----------------------------------------------------------
3008 case ED_NAIVE:
3009 default:
3010 expl_lb = est_2[i]; expl_ub = lst_2[i];
3011 }
3012 //printf("%d: dur_in %d/%d; en_in %d; est0 %d; lst0 %d\t", i, dur_in, dur[i], dur_in * min_usage(i), est0, lst0);
3013 if (est0 < expl_lb) {
3014 //printf("s[%d] >= %d; ", i, expl_lb);
3015 expl.push(getNegGeqLit(start[i], expl_lb));
3016 }
3017 if (expl_ub < lst0) {
3018 //printf("s[%d] <= %d; ", i, expl_ub);
3019 expl.push(getNegLeqLit(start[i], expl_ub));
3020 }
3021 // Get the negated literal for [[dur[i] >= min_dur(i)]]
3022 if (min_dur0(i) < min_dur(i))
3023 expl.push(getNegGeqLit(dur[i], min_dur(i)));
3024 // Get the negated literal for [[usage[i] >= min_usage(i)]]
3025 if (min_usage0(i) < min_usage(i))
3026 expl.push(getNegGeqLit(usage[i], min_usage(i)));
3027 //printf("\n");
3028 tasks.pop_front();
3029 }
3030 }
3031
3032 inline bool
is_intersecting(const int begin1,const int end1,const int begin2,const int end2)3033 CumulativeCalProp::is_intersecting(const int begin1, const int end1, const int begin2, const int end2) {
3034 return ((begin1 <= begin2 && begin2 < end1) || (begin2 <= begin1 && begin1 < end2));
3035 }
3036
3037 /*** EOF ***/
3038
3039