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 // Time Decomposition of the cumulative constraint
timed_cumulative(vec<IntVar * > & s,vec<int> & d,vec<int> & r,int b)10 void timed_cumulative(vec<IntVar*>& s, vec<int>& d, vec<int>& r, int b) {
11 assert(s.size() == d.size() && s.size() == r.size());
12 int min = INT_MAX;
13 int max = INT_MIN;
14 // bool in[s.size()];
15 bool* in = new bool[s.size()];
16 vec<int> a;
17 for (int i = 0; i < s.size(); i++) {
18 in[i] = (d[i] > 0 && r[i] > 0);
19 if (!in[i]) continue;
20 if (s[i]->getMin() < min) min = s[i]->getMin();
21 if (s[i]->getMax() + d[i] > max) max = s[i]->getMax() + d[i];
22 s[i]->specialiseToEL();
23 a.push(r[i]);
24 }
25 for (int t = min; t <= max; t++) {
26 vec<IntVar*> x;
27 for (int i = 0; i < s.size(); i++) {
28 if (!in[i]) continue;
29 BoolView b1(s[i]->getLit(t,3));
30 BoolView b2(s[i]->getLit(t-d[i]+1,2));
31 BoolView b3 = newBoolVar();
32 IntVar* v = newIntVar(0,1);
33 bool_rel(b1, BRT_AND, b2, b3);
34 bool2int(b3, v);
35 x.push(v);
36 }
37 int_linear(a, x, IRT_LE, b);
38 }
39 delete[] in;
40
41 }
42
43 #define CUMUVERB 0
44
45 // Data types for the Chuffed solver
46 #define CUMU_ARR_INTVAR vec<IntVar*>
47 #define CUMU_ARR_INT vec<int>
48 #define CUMU_INTVAR IntVar*
49 #define CUMU_INT int
50 #define CUMU_BOOL bool
51 #define CUMU_GETMIN(x) x.getMin()
52 #define CUMU_GETMAX(x) x.getMax()
53 #define CUMU_GETMAX0(x) x.getMax()
54 #define CUMU_PT_GETMIN(x) x->getMin()
55 #define CUMU_PT_GETMAX(x) x->getMax()
56 #define CUMU_PT_GETMIN0(x) x->getMin0()
57 #define CUMU_PT_GETMAX0(x) x->getMax0()
58 #define CUMU_PT_ISFIXED(x) x->isFixed()
59
60 class CumulativeProp : public Propagator {
61 enum ExplDeg {
62 ED_NAIVE,
63 ED_NORMAL,
64 ED_LIFT
65 };
66 // Task-Duration tuple
67 struct TaskDur {
68 int task;
69 int dur_in;
TaskDurCumulativeProp::TaskDur70 TaskDur(int _task, int _dur_in) : task(_task), dur_in(_dur_in) {}
71 };
72 // TTEF Update Structure
73 struct TTEFUpdate {
74 int task;
75 int bound_new;
76 int tw_begin;
77 int tw_end;
78 bool is_lb_update;
TTEFUpdateCumulativeProp::TTEFUpdate79 TTEFUpdate(int _t, int _n, int _b, int _e, int _l) : task(_t), bound_new(_n),
80 tw_begin(_b), tw_end(_e), is_lb_update(_l) {}
81 };
82 // Compulsory Part of a Task
83 struct CompPart {
84 CUMU_INT begin;
85 CUMU_INT end;
86 CUMU_INT level;
87 CUMU_INT task;
CompPartCumulativeProp::CompPart88 CompPart(CUMU_INT b, CUMU_INT e, CUMU_INT l, CUMU_INT t)
89 : begin(b), end(e), level(l), task(t) {}
90 };
91
92 // Resource profile of the resource
93 struct ProfilePart {
94 CUMU_INT begin;
95 CUMU_INT end;
96 CUMU_INT level;
97 set<CUMU_INT> tasks;
ProfilePartCumulativeProp::ProfilePart98 ProfilePart(CUMU_INT b, CUMU_INT e, CUMU_INT l, CUMU_INT t)
99 : begin(b), end(e), level(l) { tasks.insert(t); };
ProfilePartCumulativeProp::ProfilePart100 ProfilePart() : begin(0), end(0), level(0) {}
101 };
102
103 enum ProfileChange { PROFINC, PROFDEC };
104 struct ProfileChangePt {
105 CUMU_INT time;
106 ProfileChange change;
ProfileChangePtCumulativeProp::ProfileChangePt107 ProfileChangePt(CUMU_INT t, ProfileChange c) : time(t), change(c) {}
108 };
109
110 Tint last_unfixed;
111
112 public:
113 string name; // Name of the cumulative constraint for printing statistics
114
115 // Constant Data
116 CUMU_ARR_INTVAR start; // Start time variables of the tasks
117 CUMU_ARR_INTVAR dur; // Durations of the tasks
118 CUMU_ARR_INTVAR usage; // Resource usage of the tasks
119 CUMU_INTVAR limit; // Resource capacity of the resource
120
121 // Options
122 CUMU_BOOL idem; // Whether the cumulative propagator should be idempotent
123 CUMU_BOOL tt_check;
124 CUMU_BOOL tt_filt;
125 CUMU_BOOL ttef_check;
126 CUMU_BOOL ttef_filt;
127
128 ExplDeg ttef_expl_deg;
129
130 // Counters
131 long nb_tt_incons; // Number of timetabling inconsistencies
132 long nb_tt_filt; // Number of timetabling propagations
133 long nb_ttef_incons; // Number of timetabling-edge-finding inconsistencies
134 long nb_ttef_filt; // Number of timetabling-edge-finding propagations
135
136 // Parameters
137 CUMU_BOOL bound_update;
138
139 // Structures
140 CUMU_ARR_INT task_id; // Unfixed tasks on the left-hand side and fixed tasks on the right-hand size
141 int * task_id_est;
142 int * task_id_lct;
143 int * tt_after_est;
144 int * tt_after_lct;
145 int * new_est;
146 int * new_lct;
147 int tt_profile_size;
148 struct ProfilePart * tt_profile;
149
150 // Inline functions
151 struct SortEstAsc {
152 CumulativeProp *p;
operator ()CumulativeProp::SortEstAsc153 bool operator() (int i, int j) { return p->est(i) < p->est(j); }
SortEstAscCumulativeProp::SortEstAsc154 SortEstAsc(CumulativeProp *_p) : p(_p) {}
155 } sort_est_asc;
156
157 struct SortLctAsc {
158 CumulativeProp *p;
operator ()CumulativeProp::SortLctAsc159 bool operator() (int i, int j) { return p->lct(i) < p->lct(j); }
SortLctAscCumulativeProp::SortLctAsc160 SortLctAsc(CumulativeProp *_p) : p(_p) {}
161 } sort_lct_asc;
162
163 // Constructor
164 //
CumulativeProp(CUMU_ARR_INTVAR & _start,CUMU_ARR_INTVAR & _dur,CUMU_ARR_INTVAR & _usage,CUMU_INTVAR _limit,list<string> opt)165 CumulativeProp(CUMU_ARR_INTVAR & _start, CUMU_ARR_INTVAR & _dur, CUMU_ARR_INTVAR & _usage,
166 CUMU_INTVAR _limit, list<string> opt)
167 : name(""), start(_start), dur(_dur), usage(_usage), limit(_limit),
168 idem(false), tt_check(true), tt_filt(true), ttef_check(false), ttef_filt(false),
169 nb_tt_incons(0), nb_tt_filt(0), nb_ttef_incons(0), nb_ttef_filt(0),
170 bound_update(false),
171 sort_est_asc(this), sort_lct_asc(this)
172 {
173 // Overriding option defaults
174 for (list<string>::iterator it = opt.begin(); it != opt.end(); it++) {
175 if (!(*it).compare("tt_filt_on"))
176 tt_filt = true;
177 else if (!(*it).compare("tt_filt_off"))
178 tt_filt = false;
179 if (!(*it).compare("ttef_check_on"))
180 ttef_check = true;
181 else if (!(*it).compare("ttef_check_off"))
182 ttef_check = false;
183 if (!(*it).compare("ttef_filt_on"))
184 ttef_filt = true;
185 else if (!(*it).compare("ttef_filt_off"))
186 ttef_filt = false;
187 else if ((*it).find("__name__") == 0)
188 name = (*it).substr(8);
189 }
190 //ttef_expl_deg = ED_NAIVE;
191 //ttef_expl_deg = ED_NORMAL;
192 ttef_expl_deg = ED_LIFT;
193 // Allocation of the memory
194 tt_profile = new ProfilePart[2 * start.size()];
195 tt_profile_size = 0;
196 // XXX Check for successful memory allocation
197 if (ttef_check || ttef_filt) {
198 task_id_est = (int *) malloc(start.size() * sizeof(int));
199 task_id_lct = (int *) malloc(start.size() * sizeof(int));
200 tt_after_est = (int *) malloc(start.size() * sizeof(int));
201 tt_after_lct = (int *) malloc(start.size() * sizeof(int));
202 if (ttef_filt) {
203 new_est = (int *) malloc(start.size() * sizeof(int));
204 new_lct = (int *) malloc(start.size() * sizeof(int));
205 } else {
206 new_est = NULL;
207 new_lct = NULL;
208 }
209 // XXX Check for successful memory allocation
210 } else {
211 task_id_est = NULL;
212 task_id_lct = NULL;
213 tt_after_est = NULL;
214 }
215
216 // Priority of the propagator
217 priority = 3;
218 #if CUMUVERB>0
219 fprintf(stderr, "\tCumulative with n = %d\n", start.size());
220 #endif
221 // Attach to var events
222 for (int i = 0; i < start.size(); i++) {
223 #if CUMUVERB>1
224 fprintf(stderr, "\t%d: %p\n", i, start[i]);
225 #endif
226 start[i]->attach(this, i, EVENT_LU);
227 if (min_dur(i) < max_dur(i)) dur[i]->attach(this, i, EVENT_LF);
228 if (min_usage(i) < max_usage(i)) usage[i]->attach(this, i, EVENT_LF);
229 }
230 limit->attach(this, start.size(), EVENT_UF);
231
232 for (int i = 0; i < start.size(); i++) {
233 task_id.push(i);
234 }
235 last_unfixed = start.size() - 1;
236 }
237
238 // Statistics
printStats()239 void printStats() {
240 fprintf(stderr, "%% Cumulative propagator statistics");
241 if (name != "")
242 cerr << " for " << name;
243 fprintf(stderr, ":\n");
244 fprintf(stderr, "%%\t#TT incons.: %ld\n", nb_tt_incons);
245 if (tt_filt)
246 fprintf(stderr, "%%\t#TT prop.: %ld\n", nb_tt_filt);
247 if (ttef_check || ttef_filt)
248 fprintf(stderr, "%%\t#TTEF incons.: %ld\n", nb_ttef_incons);
249 if (ttef_filt) {
250 fprintf(stderr, "%%\t#TTEF prop.: %ld\n", nb_ttef_filt);
251 }
252 }
253
254 /**
255 * Inline function for parameters of tasks
256 **/
257 // Earliest start time of task i
258 inline CUMU_INT
est(CUMU_INT i)259 est(CUMU_INT i) { return CUMU_PT_GETMIN(start[i]); }
260 // Latest start time of task i
261 inline CUMU_INT
lst(CUMU_INT i)262 lst(CUMU_INT i) { return CUMU_PT_GETMAX(start[i]); }
263 // Earliest completion time of task i
264 inline CUMU_INT
ect(CUMU_INT i)265 ect(CUMU_INT i) { return CUMU_PT_GETMIN(start[i]) + CUMU_PT_GETMIN(dur[i]); }
266 // Latest completion time of task i
267 inline CUMU_INT
lct(CUMU_INT i)268 lct(CUMU_INT i) { return CUMU_PT_GETMAX(start[i]) + CUMU_PT_GETMIN(dur[i]); }
269 // Minimal resource usage of task i
270 inline CUMU_INT
min_usage(CUMU_INT i)271 min_usage(CUMU_INT i) { return CUMU_PT_GETMIN(usage[i]); }
272 // Minimal energy of task i
273 inline CUMU_INT
min_energy(CUMU_INT i)274 min_energy(CUMU_INT i) { return min_usage(i) * min_dur(i); }
275 // Free Energy
276 inline CUMU_INT
free_energy(CUMU_INT i)277 free_energy(CUMU_INT i) {
278 return min_energy(i) - min_usage(i) * max(0, ect(i) - lst(i));
279 }
280
281 /**
282 * Inline functions for receiving the minimum and maximum of integer
283 * variables
284 **/
285 inline CUMU_INT
min_start0(CUMU_INT i)286 min_start0(CUMU_INT i) { return CUMU_PT_GETMIN0(start[i]); }
287 inline CUMU_INT
max_start0(CUMU_INT i)288 max_start0(CUMU_INT i) { return CUMU_PT_GETMAX0(start[i]); }
289 inline CUMU_INT
min_dur(CUMU_INT i)290 min_dur(CUMU_INT i) { return CUMU_PT_GETMIN(dur[i]); }
291 inline CUMU_INT
max_dur(CUMU_INT i)292 max_dur(CUMU_INT i) { return CUMU_PT_GETMAX(dur[i]); }
293 inline CUMU_INT
min_dur0(CUMU_INT i)294 min_dur0(CUMU_INT i) { return CUMU_PT_GETMIN0(dur[i]); }
295 inline CUMU_INT
max_usage(CUMU_INT i)296 max_usage(CUMU_INT i) { return CUMU_PT_GETMAX(usage[i]); }
297 inline CUMU_INT
min_usage0(CUMU_INT i)298 min_usage0(CUMU_INT i) { return CUMU_PT_GETMIN0(usage[i]); }
299
300 inline CUMU_INT
min_limit()301 min_limit() { return CUMU_PT_GETMIN(limit); }
302 inline CUMU_INT
max_limit()303 max_limit() { return CUMU_PT_GETMAX(limit); }
304 inline CUMU_INT
max_limit0()305 max_limit0() { return CUMU_PT_GETMAX0(limit); }
306
307 // Cumulative Propagator
308 CUMU_BOOL
propagate()309 propagate() {
310 #if CUMUVERB>0
311 fprintf(stderr, "Entering cumulative propagation\n");
312 #endif
313 int new_unfixed = last_unfixed;
314 for (int ii = new_unfixed; ii >= 0; ii--) {
315 int i = task_id[ii];
316 if ((CUMU_PT_ISFIXED(start[i]) && CUMU_PT_ISFIXED(dur[i]) && CUMU_PT_ISFIXED(usage[i])) || max_dur(i) <= 0 || max_usage(i) <= 0) {
317 // Swaping the id's
318 task_id[ii] = task_id[new_unfixed];
319 task_id[new_unfixed] = i;
320 new_unfixed--;
321 }
322 }
323 // Trailing the index of the last unfixed task
324 last_unfixed = new_unfixed;
325 #if CUMUVERB>0
326 fprintf(stderr, "\tEntering cumulative propagation loop\n");
327 #endif
328 // idempotent
329 do {
330 bound_update = false;
331 // Reseting the profile size
332 tt_profile_size = 0;
333 // Time-table propagators
334 if (tt_check || tt_filt) {
335 // Time-table propagation
336 if (! time_table_propagation(task_id) ) {
337 // Inconsistency was detected
338 #if CUMUVERB > 10
339 fprintf(stderr, "Leaving cumulative propagation with failure\n");
340 #endif
341 return false;
342 }
343 }
344 // TODO Time-table-edge-finding propagation
345 if (!bound_update && last_unfixed > 0 && (ttef_check || ttef_filt)) {
346 // Initialisation of necessary structures
347 // - Unfixed tasks sorted according earliest start time
348 // - Unfixed tasks sorted according latest completion time
349 // - Energy of the compulsory parts after the latest completion
350 // time of unfixed tasks
351 // - Energy of the compulsory parts after the earliest start
352 // time of unfixed tasks
353 ttef_initialise_parameters();
354 // TTEF consistency check
355 //if (!ttef_consistency_check(get_free_dur_right_shift)) {
356 // // Inconsistency was detected
357 // return false;
358 //}
359 // TODO TTEF start time filtering algorithm
360 if (ttef_filt) {
361 if (!ttef_bounds_propagation(get_free_dur_right_shift, get_free_dur_left_shift)) {
362 // Inconsistency was detected
363 return false;
364 }
365 } else {
366 if (!ttef_consistency_check(get_free_dur_right_shift)) {
367 // Inconsistency was detected
368 return false;
369 }
370 }
371 }
372 // TODO Optional task propagation
373 if (!bound_update) {
374 if (tt_filt && tt_profile_size > 0) {
375 if (!tt_optional_task_propagation()) {
376 // Inconsistency was detected
377 return false;
378 }
379 }
380 }
381 } while (idem && bound_update);
382 #if CUMUVERB > 0
383 fprintf(stderr, "\tLeaving cumulative propagation loop\n");
384 fprintf(stderr, "Leaving cumulative propagation without failure\n");
385 #endif
386 return true;
387 }
388
389 // Comparison between two compulsory parts
390 static bool
compare_CompParts(CompPart cp1,CompPart cp2)391 compare_CompParts(CompPart cp1, CompPart cp2) {
392 if (cp1.begin < cp2.begin) return true;
393 if (cp1.begin > cp2.begin) return false;
394 // ASSUMPTION
395 // - cp1.begin == cp2.begin
396 if (cp1.end < cp2.end) return true;
397 if (cp1.end > cp2.end) return false;
398 // ASSUMPTION
399 // - cp1.end == cp2.end
400 if (cp1.task < cp2.task) return true;
401 return false;
402 }
403
404
405 // Creation of the resource profile for the time-table consistency check
406 // and propagator
407 CUMU_BOOL
time_table_propagation(CUMU_ARR_INT & task)408 time_table_propagation(CUMU_ARR_INT & task) {
409 list<ProfileChangePt> changes;
410 list<CUMU_INT> comp_task;
411 //int size_profile = 0;
412
413 #if CUMUVERB>10
414 fprintf(stderr, "\tCompulsory Parts ...\n");
415 #endif
416 get_compulsory_parts2(changes, comp_task, task, 0, task.size());
417 // Proceed if there are compulsory parts
418 if (!changes.empty()) {
419 #if CUMUVERB>1
420 fprintf(stderr, "\tSorting (size %d)...\n", (int) changes.size());
421 #endif
422 // Sorting the start and end points of all the profile
423 changes.sort(compare_ProfileChangePt);
424 #if CUMUVERB>1
425 fprintf(stderr, "\tSorting (size %d)...\n", (int) changes.size());
426 #endif
427 // Counting the number of different profiles
428 tt_profile_size = count_profile(changes);
429 #if CUMUVERB>1
430 fprintf(stderr, "\t#profile parts = %d\n", tt_profile_size);
431 #endif
432 #if CUMUVERB>1
433 fprintf(stderr, "\tProfile Parts ...\n");
434 #endif
435 // Creating the different profile parts
436 create_profile(changes);
437 int i_max_usage = 0;
438 #if CUMUVERB>1
439 fprintf(stderr, "\tFilling of Profile Parts ...\n");
440 #endif
441 // Filling the profile parts with tasks
442 if (!fill_in_profile_parts(tt_profile, tt_profile_size, comp_task, i_max_usage)) {
443 return false;
444 }
445 #if CUMUVERB>10
446 fprintf(stderr, "\tFiltering Resource Limit ...\n");
447 #endif
448 // Filtering of resource limit variable
449 if (!filter_limit(tt_profile, i_max_usage)) {
450 return false;
451 }
452 if (tt_filt) {
453 #if CUMUVERB>10
454 fprintf(stderr, "\tFiltering Start Times ...\n");
455 #endif
456 // Time-table filtering
457 if (!time_table_filtering(tt_profile, tt_profile_size, task, 0, last_unfixed, tt_profile[i_max_usage].level)) {
458 return false;
459 }
460 }
461 }
462 #if CUMUVERB>10
463 fprintf(stderr, "\tEnd of time-table propagation ...\n");
464 #endif
465 return true;
466 }
467
468 void
469 get_compulsory_parts2(
470 list<ProfileChangePt> &changes, list<CUMU_INT> &comp_task, CUMU_ARR_INT & task,
471 CUMU_INT i_start, CUMU_INT i_end
472 );
473
474 // Sets for each profile part its begin and end time in chronological order
475 // Runtime complexity: O(n)
476 //
477 void
create_profile(list<ProfileChangePt> & changes)478 create_profile(list<ProfileChangePt> &changes) {
479 list<ProfileChangePt>::iterator iter = changes.begin();
480 int cur_profile = 0;
481 int cur_time = iter->time;
482 ProfileChange cur_change = iter->change;
483 int no_starts = 1;
484 for (; iter != changes.end(); iter++) {
485 if (iter->time > cur_time && no_starts > 1) {
486 #if CUMUVERB>20
487 fprintf(stderr, "Set times for profile part %d = [%d, %d)\n", cur_profile, cur_time, iter->time);
488 fprintf(stderr, "\t%p; %p; %d\n", tt_profile, this, start.size());
489 #endif
490 set_times_for_profile(cur_profile, cur_time, iter->time);
491 cur_profile++;
492 }
493 no_starts += (iter->change == PROFINC ? 1 : -1);
494 cur_change = iter->change;
495 cur_time = iter->time;
496 }
497 }
498
499 inline void
set_times_for_profile(int i,CUMU_INT begin,CUMU_INT end)500 set_times_for_profile(int i, CUMU_INT begin, CUMU_INT end) {
501 tt_profile[i].begin = begin;
502 tt_profile[i].end = end;
503 tt_profile[i].level = 0;
504 //fprintf(stderr, "blxxx %d\n", (int) tt_profile[i].tasks.size());
505 tt_profile[i].tasks.clear();
506 }
507
508 // Filling the profile parts with compulsory parts and checking for a resource
509 // overload
510 CUMU_BOOL
fill_in_profile_parts(ProfilePart * profile,int size,list<CUMU_INT> comp_task,int & i_max_usage)511 fill_in_profile_parts(ProfilePart * profile, int size, list<CUMU_INT> comp_task, int & i_max_usage) {
512 list<CUMU_INT>::iterator iter;
513 int i = 0;
514 CUMU_INT lst_i, ect_i;
515
516 #if CUMUVERB>2
517 fprintf(stderr, "\t\tstart filling profiles (size %d)\n", size);
518 #endif
519 for (iter = comp_task.begin(); iter != comp_task.end(); iter++) {
520 #if CUMUVERB>2
521 fprintf(stderr, "\t\tcomp part = %d\n", *iter);
522 #endif
523 lst_i = lst(*iter);
524 ect_i = ect(*iter);
525 #if CUMUVERB>2
526 fprintf(stderr, "\t\tFinding first profile part\n");
527 #endif
528 // Find first profile
529 i = find_first_profile(profile, 0, size - 1, lst_i);
530 #if CUMUVERB>2
531 fprintf(stderr, "\t\tAdding comp parts of level %d\n", min_usage(*iter));
532 #endif
533 // Add compulsory part to the profile
534 while (i < size && profile[i].begin < ect_i) {
535 #if CUMUVERB>2
536 fprintf(stderr, "\t\t\tAdding comp parts in profile part %d\n", i);
537 #endif
538 profile[i].level += min_usage(*iter);
539 profile[i].tasks.insert(*iter);
540 // Checking if the profile part i is the part with the maximal level
541 //
542 if (profile[i].level > profile[i_max_usage].level) {
543 i_max_usage = i;
544 }
545 // Time-table consistency check
546 //
547 if (profile[i].level > max_limit()) {
548 #if CUMUVERB > 20
549 fprintf(stderr, "\t\t\tResource overload (%d > %d) in profile part %d\n", profile[i].level, max_limit(), i);
550 #endif
551 // Increment the inconsistency counter
552 nb_tt_incons++;
553
554 // The resource is overloaded in this part
555 vec<Lit> expl;
556 if (so.lazy) {
557 CUMU_INT lift_usage = profile[i].level - max_limit() - 1;
558 CUMU_INT begin1, end1;
559 // TODO Different choices to pick the interval
560 // Pointwise explanation
561 begin1 = profile[i].begin + ((profile[i].end - profile[i].begin) / 2);
562 end1 = begin1 + 1;
563 // Generation of the explanation
564 analyse_limit_and_tasks(
565 expl, profile[i].tasks, lift_usage, begin1, end1
566 );
567 }
568 // Submitting of the conflict explanation
569 submit_conflict_explanation(expl);
570 #if CUMUVERB > 20
571 fprintf(stderr, "\t\tend filling (conflict)\n");
572 #endif
573 return false;
574 }
575 i++;
576 }
577 }
578 #if CUMUVERB>2
579 fprintf(stderr, "\t\tend filling (successful)\n");
580 #endif
581 return true;
582 }
583
584 // Finds the profile part that begins at the time unit "lst"
585 // Complexity: O(log(high - low + 1))
586 //
587 int
find_first_profile(ProfilePart * profile,int low,int high,CUMU_INT lst)588 find_first_profile(ProfilePart * profile, int low, int high, CUMU_INT lst) {
589 int median = 0;
590 while (profile[low].begin != lst) {
591 median = low + (high - low + 1) / 2;
592 if (profile[median].begin > lst) {
593 high = median;
594 } else {
595 low = median;
596 }
597 }
598 return low;
599 }
600
601 // Counting the number of profiles
602 //
603 int
count_profile(list<ProfileChangePt> & changes)604 count_profile(list<ProfileChangePt> &changes) {
605 list<ProfileChangePt>::iterator iter = changes.begin();
606 int cur_time = iter->time;
607 int next_time;
608 ProfileChange cur_change = iter->change;
609 int no_starts = ( iter->change == PROFINC ? 1 : 0 );
610 int no_profile = no_starts;
611 iter++;
612
613 #if CUMUVERB>2
614 fprintf( stderr, "\t\t\ttime = %d; change = %d; no_starts = %d; no_profile = %d;\n", cur_time, cur_change, no_starts, no_profile);
615 #endif
616 for (; iter != changes.end(); iter++) {
617 if (iter->change == PROFINC) {
618 if (cur_time < iter->time || cur_change == PROFDEC) {
619 no_profile++;
620 }
621 no_starts++;
622 } else {
623 // ASSUMPTION
624 // - iter->change = PROFDEC
625 no_starts--;
626 next_time = iter->time;
627 iter++;
628 if (iter != changes.end() && no_starts > 0 && iter->time > next_time) {
629 no_profile++;
630 }
631 iter--;
632 }
633 cur_time = iter->time;
634 cur_change = iter->change;
635 #if CUMUVERB>2
636 fprintf( stderr, "\t\t\ttime = %d; change = %d; no_starts = %d; no_profile = %d;\n", cur_time, cur_change, no_starts, no_profile);
637 #endif
638 }
639 return no_profile;
640 }
641
642 static bool
compare_ProfileChangePt(ProfileChangePt & pt1,ProfileChangePt & pt2)643 compare_ProfileChangePt(ProfileChangePt & pt1, ProfileChangePt & pt2) {
644 if (pt1.time == pt2.time && pt1.change == PROFDEC && pt2.change == PROFINC) return true;
645 return pt1.time < pt2.time;
646 }
647
648 // Time-table filtering on the lower bound of the resource limit variable
649 // Complexity:
650 CUMU_BOOL
651 filter_limit(ProfilePart * profile, int & i_max_usage);
652
653 // Time-table filtering on the start time variables
654 // Complexity:
655 CUMU_BOOL
656 time_table_filtering(ProfilePart profile[], int size, CUMU_ARR_INT & task, int start, int end, CUMU_INT max_usage);
657 CUMU_BOOL
658 time_table_filtering_lb(ProfilePart profile[], int low, int high, int task);
659 CUMU_BOOL
660 time_table_filtering_ub(ProfilePart profile[], int low, int high, int task);
661
662 int
663 find_first_profile_for_lb(ProfilePart profile[], int low, int high, CUMU_INT t);
664 int
665 find_first_profile_for_ub(ProfilePart profile[], int low, int high, CUMU_INT t);
666
667 // Time-table filtering for optional tasks
668 CUMU_BOOL
669 tt_optional_task_propagation();
670
671 // Analysing the conflict and generation of the explanations
672 // NOTE: Fixed durations and resource usages are assumed!!!
673 //
674 // Explanation is created for the time interval [begin, end), i.e., exluding end.
675 //
676 void
677 analyse_limit_and_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end);
678 void
679 analyse_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end);
680 void
681 submit_conflict_explanation(vec<Lit> & expl);
682 Clause *
683 get_reason_for_update(vec<Lit> & expl);
684
685 // TODO Disentailment check
686 //CUMU_INT
687 //checkSatisfied() {
688 // // XXX Until no cumulative propagator is implemented the constraint
689 // // is always ?satisfied?
690 // return 1;
691 //}
692
693 // Wrapper to get the negated literal -[[v <= val]] = [[v >= val + 1]]
694 inline Lit
getNegLeqLit(CUMU_INTVAR v,CUMU_INT val)695 getNegLeqLit(CUMU_INTVAR v, CUMU_INT val) {
696 //return v->getLit(val + 1, 2);
697 return (INT_VAR_LL == v->getType() ? v->getMaxLit() : v->getLit(val + 1, 2));
698 }
699 // Wrapper to get the negated literal -[[v >= val]] = [[ v <= val - 1]]
700 inline Lit
getNegGeqLit(CUMU_INTVAR v,CUMU_INT val)701 getNegGeqLit(CUMU_INTVAR v, CUMU_INT val) {
702 //return v->getLit(val - 1, 3);
703 return (INT_VAR_LL == v->getType() ? v->getMinLit() : v->getLit(val - 1, 3));
704 }
705
706 // TTEF Propagator
707 //
708 void ttef_initialise_parameters();
709 bool ttef_consistency_check(int shift_in(const int, const int, const int, const int, const int, const int, const int));
710 bool ttef_bounds_propagation(int shift_in1(const int, const int, const int, const int, const int, const int, const int),
711 int shift_in2(const int, const int, const int, const int, const int, const int, const int));
712 bool ttef_bounds_propagation_lb(int shift_in(const int, const int, const int, const int, const int, const int, const int),
713 std::queue<TTEFUpdate> & update_queue);
714 bool ttef_bounds_propagation_ub(int shift_in(const int, const int, const int, const int, const int, const int, const int),
715 std::queue<TTEFUpdate> & update_queue);
716 bool ttef_update_bounds(int shift_in(const int, const int, const int, const int, const int, const int, const int),
717 std::queue<TTEFUpdate> & queue_update);
718
719 int
720 ttef_retrieve_tasks(int shift_in(const int, const int, const int, const int, const int, const int, const int),
721 int begin, int end, int fb_id, list<TaskDur> & tasks_tw, list<TaskDur> & tasks_cp);
722
723 // TTEF Generation of explanations
724 //
725 void
726 ttef_analyse_limit_and_tasks(const int begin, const int end, list<TaskDur> & tasks_tw,
727 list<TaskDur> & tasks_cp, int & en_lift, vec<Lit> & expl);
728 void
729 ttef_analyse_tasks(const int begin, const int end, list<TaskDur> & tasks, int & en_lift, vec<Lit> & expl);
730
731 inline bool
732 is_intersecting(const int begin1, const int end1, const int begin2, const int end2);
733
734 // Shift functions
735 //
736 static inline int
get_free_dur_right_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)737 get_free_dur_right_shift(const int tw_begin, const int tw_end, const int est, const int ect,
738 const int lst, const int lct, const int dur_fixed_in)
739 {
740 return (tw_begin <= est ? max(0, tw_end - lst - dur_fixed_in) : 0);
741 }
742
743 static inline int
get_free_dur_left_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)744 get_free_dur_left_shift(const int tw_begin, const int tw_end, const int est, const int ect,
745 const int lst, const int lct, const int dur_fixed_in)
746 {
747 return (tw_end >= lct ? max(0, ect - tw_begin - dur_fixed_in) : 0);
748 }
749
750 static 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)751 get_no_shift(const int tw_begin, const int tw_end, const int est, const int ect,
752 const int lst, const int lct, const int dur_fixed_in)
753 {
754 return 0;
755 }
756 };
757
758 /****
759 * Functions related to the Time-Table Consistency Check and Propagation
760 ****/
761
762 void
get_compulsory_parts2(list<ProfileChangePt> & changes,list<CUMU_INT> & comp_task,CUMU_ARR_INT & task,CUMU_INT i_start,CUMU_INT i_end)763 CumulativeProp::get_compulsory_parts2(
764 list<ProfileChangePt> &changes, list<CUMU_INT> &comp_task, CUMU_ARR_INT & task, CUMU_INT i_start, CUMU_INT i_end
765 ) {
766 CUMU_INT i;
767 #if CUMUVERB>2
768 fprintf(stderr, "\tstart get_compulsory_part from %d to %d\n", i_start, i_end);
769 #endif
770 for (i = i_start; i < i_end; i++) {
771 #if CUMUVERB>2
772 fprintf(stderr, "\t\ti = %d; task[i] = %d\n", i, task[i]);
773 #endif
774 // Check whether the task creates a compulsory part
775 if (min_dur(task[i]) > 0 && min_usage(task[i]) > 0 && lst(task[i]) < ect(task[i])) {
776 #if CUMUVERB>2
777 fprintf(stderr, "\t\ttask[i] = %d, comp part [%d, %d)\n", task[i], lst(task[i]), ect(task[i]));
778 #endif
779 // Add task to the list
780 comp_task.push_back(task[i]);
781 // Add time points to change lists
782 changes.push_back( ProfileChangePt(lst(task[i]), PROFINC) );
783 changes.push_back( ProfileChangePt(ect(task[i]), PROFDEC) );
784 }
785 }
786 #if CUMUVERB>2
787 fprintf(stderr, "\tend get_compulsory_part\n");
788 #endif
789 }
790
791
792 /***************************************************************************************
793 * Function for time-table filtering on the lower bound of the resource limit variable *
794 ***************************************************************************************/
795
796 CUMU_BOOL
filter_limit(ProfilePart * profile,int & i)797 CumulativeProp::filter_limit(ProfilePart * profile, int & i) {
798 if (min_limit() < profile[i].level) {
799 Clause * reason = NULL;
800 nb_tt_filt++;
801 if (so.lazy) {
802 // Lower bound can be updated
803 // XXX Determining what time period is the best
804 int expl_begin = profile[i].begin + ((profile[i].end - profile[i].begin - 1)/2);
805 int expl_end = expl_begin + 1;
806 vec<Lit> expl;
807 // Get the negated literals for the tasks in the profile
808 analyse_tasks(expl, profile[i].tasks, 0, expl_begin, expl_end);
809 // Transform literals to a clause
810 reason = get_reason_for_update(expl);
811 }
812 if (! limit->setMin(profile[i].level, reason)) {
813 // Conflict occurred
814 return false;
815 }
816 // Set bound_update to true
817 bound_update = true;
818 }
819 return true;
820 }
821
822 /******************************************************************
823 * Functions for Time-Table Filtering on the start time variables *
824 ******************************************************************/
825
826 CUMU_BOOL
time_table_filtering(ProfilePart profile[],int size,CUMU_ARR_INT & task,int i_start,int i_end,CUMU_INT max_usage)827 CumulativeProp::time_table_filtering(ProfilePart profile[], int size, CUMU_ARR_INT & task, int i_start, int i_end, CUMU_INT max_usage) {
828 for (int i = i_start; i <= i_end; i++) {
829 // Skipping tasks with zero duration or usage
830 if (min_dur(task[i]) <= 0 || min_usage(task[i]) <= 0)
831 continue;
832 #if CUMUVERB>0
833 fprintf(stderr, "TT Filtering of task %d\n", task[i]);
834 #endif
835 // Check if the sum of max_usage and the task's usage are greater then the upper bound
836 // on the resource limit
837 if (min_usage(task[i]) + max_usage > max_limit()) {
838 int index;
839 #if CUMUVERB>0
840 fprintf(stderr, "Finding the first index for LB ...\n");
841 #endif
842 // Find initial profile part for lower bound propagation
843 //
844 index = find_first_profile_for_lb(profile, 0, size - 1, est(task[i]));
845 #if CUMUVERB>0
846 fprintf(stderr, "Lower bound starting from index %d till index %d\n", index, size - 1);
847 #endif
848 // Update the lower bound if possible
849 if (! time_table_filtering_lb(profile, index, size - 1, task[i])) {
850 return false;
851 }
852 #if CUMUVERB>0
853 fprintf(stderr, "Finding the first index for UB ...\n");
854 #endif
855 // Find initial profile part for upper bound propagation
856 index = find_first_profile_for_ub(profile, 0, size - 1, lct(task[i]));
857 #if CUMUVERB>0
858 fprintf(stderr, "Upper bound starting from index %d till index 0\n", index);
859 #endif
860 // Update the upper bound if possible
861 if (! time_table_filtering_ub(profile, 0, index, task[i])) {
862 return false;
863 }
864 }
865 }
866 return true;
867 }
868
869 // Time-Table Filtering on the Lower Bound of Start Times Variables
870 //
871 CUMU_BOOL
time_table_filtering_lb(ProfilePart profile[],int low,int high,int task)872 CumulativeProp::time_table_filtering_lb(ProfilePart profile[], int low, int high, int task) {
873 int i;
874 #if CUMUVERB>5
875 fprintf(stderr, "task %d: start [%d, %d], end [%d, %d], min usage %d\n", task, est(task), lst(task), ect(task), lct(task), min_usage(task));
876 #endif
877 for (i = low; i <= high; i++) {
878 #if CUMUVERB>5
879 fprintf(stderr, "\tprofile[%d]: begin %d; end %d; level %d;\n", i, profile[i].begin, profile[i].end, profile[i].level);
880 #endif
881 if (ect(task) <= profile[i].begin) {
882 // No lower bound update possible
883 break;
884 }
885 // ASSUMPTION
886 // - ect(task) > profile[i].begin
887 if (est(task) < profile[i].end && profile[i].level + min_usage(task) > max_limit()) {
888 // Possibly a lower bound update if "task" as no compulsory part in the profile
889 if (lst(task) < ect(task) && lst(task) <= profile[i].begin && profile[i].end <= ect(task)) {
890 // No lower bound update possible for this profile part, because
891 // "task" has a compulsory part in it
892 continue ;
893 }
894 #if CUMUVERB>1
895 fprintf(stderr, "\n----\n");
896 fprintf(stderr, "setMin of task %d in profile part [%d, %d)\n", task, profile[i].begin, profile[i].end);
897 fprintf(stderr, "task %d: lst = %d; ect = %d; dur = %d;\n", task, lst(task), ect(task), min_dur(task));
898 #endif
899 int expl_end = profile[i].end;
900 Clause * reason = NULL;
901 if (so.lazy) {
902 // XXX Assumption for the remaining if-statement
903 // No compulsory part of task in profile[i]!
904 int lift_usage = profile[i].level + min_usage(task) - max_limit() - 1;
905 // TODO Choices of different explanation
906 // Pointwise explanation
907 expl_end = min(ect(task), profile[i].end);
908 int expl_begin = expl_end - 1;
909 vec<Lit> expl;
910 // Get the negated literal for [[start[task] >= ex_end - min_dur(task)]]
911 #if CUMUVERB>1
912 fprintf(stderr, "start[%d] => %d ", task, expl_end - min_dur(task));
913 #endif
914 expl.push(getNegGeqLit(start[task], expl_end - min_dur(task)));
915 // Get the negated literal for [[dur[task] >= min_dur(task)]]
916 if (min_dur0(task) < min_dur(task))
917 expl.push(getNegGeqLit(dur[task], min_dur(task)));
918 // Get the negated literal for [[usage[task] >= min_usage(task)]]
919 if (min_usage0(task) < min_usage(task))
920 expl.push(getNegGeqLit(usage[task], min_usage(task)));
921 // Get the negated literals for the tasks in the profile and the resource limit
922 analyse_limit_and_tasks(expl, profile[i].tasks, lift_usage, expl_begin, expl_end);
923 #if CUMUVERB>1
924 fprintf(stderr, " -> start[%d] => %d\n", task, expl_end);
925 #endif
926 // Transform literals to a clause
927 reason = get_reason_for_update(expl);
928 }
929 nb_tt_filt++;
930 // Impose the new lower bound on start[task]
931 if (! start[task]->setMin(expl_end, reason)) {
932 // Conflict occurred
933 return false;
934 }
935 // Set bound_update to true
936 bound_update = true;
937 // Check for the next profile
938 if (expl_end < profile[i].end) {
939 i--;
940 }
941 }
942 }
943 return true;
944 }
945
946 // Time-table filtering on the upper bound of start times variables
947 //
948 CUMU_BOOL
time_table_filtering_ub(ProfilePart profile[],int low,int high,int task)949 CumulativeProp::time_table_filtering_ub(ProfilePart profile[], int low, int high, int task) {
950 int i;
951 #if CUMUVERB>5
952 fprintf(stderr, "task %d: start [%d, %d], end [%d, %d], min usage %d\n", task, est(task), lst(task), ect(task), lct(task), min_usage(task));
953 #endif
954 for (i = high; i >= low; i--) {
955 #if CUMUVERB>5
956 fprintf(stderr, "\tprofile[%d]: begin %d; end %d; level %d;\n", i, profile[i].begin, profile[i].end, profile[i].level);
957 #endif
958 if (profile[i].end <= lst(task)) {
959 // No upper bound update possible
960 break;
961 }
962 // ASSUMPTION for the remaining for-loop
963 // - profile[i].end > lst(task)
964 if (profile[i].begin < lct(task) && profile[i].level + min_usage(task) > max_limit()) {
965 // Possibly a upper bound update possible if "task" has no compulsory part
966 // in this profile part
967 if (lst(task) < ect(task) && lst(task) <= profile[i].begin && profile[i].end <= ect(task)) {
968 // No lower bound update possible for this profile part, because
969 // "task" has a compulsory part in it
970 continue ;
971 }
972 int expl_begin = profile[i].begin;
973 Clause * reason = NULL;
974 if (so.lazy) {
975 // ASSUMPTION for the remaining if-statement
976 // - No compulsory part of task in profile[i]
977 int lift_usage = profile[i].level + min_usage(task) - max_limit() - 1;
978 // TODO Choices of different explanations
979 // Pointwise explanation
980 expl_begin = max(profile[i].begin, lst(task));
981 int expl_end = expl_begin + 1;
982 vec<Lit> expl;
983 // Get the negated literal for [[start[task] <= expl_begin]]
984 expl.push(getNegLeqLit(start[task], expl_begin));
985 // Get the negated literal for [[dur[task] >= min_dur(task)]]
986 if (min_dur0(task) < min_dur(task))
987 expl.push(getNegGeqLit(dur[task], min_dur(task)));
988 // Get the negated literal for [[usage[task] >= min_usage(task)]]
989 if (min_usage0(task) < min_usage(task))
990 expl.push(getNegGeqLit(usage[task], min_usage(task)));
991 // Get the negated literals for the tasks in the profile and the resource limit
992 analyse_limit_and_tasks(expl, profile[i].tasks, lift_usage, expl_begin, expl_end);
993 // Transform literals to a clause
994 reason = get_reason_for_update(expl);
995 }
996 nb_tt_filt++;
997 // Impose the new lower bound on start[task]
998 if (! start[task]->setMax(expl_begin - min_dur(task), reason)) {
999 // Conflict occurred
1000 return false;
1001 }
1002 // Set bound_update to true
1003 bound_update = true;
1004 // Check for the next profile
1005 if (profile[i].begin < expl_begin) {
1006 i++;
1007 }
1008 }
1009 }
1010 return true;
1011 }
1012
1013 CUMU_BOOL
tt_optional_task_propagation()1014 CumulativeProp::tt_optional_task_propagation() {
1015 for (int ii = 0; ii <= last_unfixed; ii++) {
1016 const int i = task_id[ii];
1017 assert(max_dur(i) > 0 && max_usage(i) > 0);
1018 if (min_dur(i) <= 0 || min_usage(i) <= 0) {
1019 //fprintf(stderr, "task %d: start [%d, %d], dur %d, usage %d\n", i, est(i), lst(i), min_dur(i), min_usage(i));
1020 // Getting the smallest non-zero value for the duration
1021 const int dur_smallest = max(1, min_dur(i));
1022 // Getting the smallest non-zero value for the usage
1023 const int usage_smallest = max(1, min_usage(i));
1024 // XXX Only for the moment to make the propagation easier
1025 if (est(i) < lst(i))
1026 continue;
1027 // Getting the starting profile index
1028 const int index = find_first_profile_for_lb(tt_profile, 0, tt_profile_size - 1, est(i));
1029 // TODO Check whether a task with a duration 'dur_smallest' and a usage 'usage_smallest'
1030 // can be scheduled
1031 //fprintf(stderr, "%d: start %d; profile (%d, %d, %d)\n", i, est(i), tt_profile[index].begin, tt_profile[index].end, tt_profile[index].level);
1032 if (est(i) < tt_profile[index].end && tt_profile[index].begin < est(i) + dur_smallest
1033 && tt_profile[index].level + usage_smallest > max_limit()) {
1034 // Tasks cannot be performed on this resource
1035
1036 Clause * reason = NULL;
1037 if (so.lazy) {
1038 // Explanation for the propagation required
1039 vec<Lit> expl;
1040
1041 // Lifting the usage
1042 int lift_usage = tt_profile[index].level + usage_smallest - max_limit() - 1;
1043 // Defining explanation time interval
1044 const int overlap_begin = max(tt_profile[index].begin, est(i));
1045 const int overlap_end = min(tt_profile[index].end, est(i) + dur_smallest);
1046 const int expl_begin = overlap_begin + ((overlap_end - overlap_begin - 1)/2);
1047 const int expl_end = expl_begin + 1;
1048
1049 // Explanation parts for task 'i'
1050 // Get the negated literal for [[start[i] >= expl_end - dur_smallest]]
1051 expl.push(getNegGeqLit(start[i], expl_end - dur_smallest));
1052 // Get the negated literal for [[start[task] <= expl_begin]]
1053 expl.push(getNegLeqLit(start[i], expl_begin));
1054 // Get the negated literal for [[dur[i] >= min_dur(i)]]
1055 if (min_dur0(i) < min_dur(i) && 0 < min_dur(i))
1056 expl.push(getNegGeqLit(dur[i], min_dur(i)));
1057 // Get the negated literal for [[usage[i] >= min_usage(i)]]
1058 if (min_usage0(i) < min_usage(i) && 0 < min_usage(i))
1059 expl.push(getNegGeqLit(usage[i], min_usage(i)));
1060
1061 // Get the negated literals for the tasks in the profile and the resource limit
1062 analyse_limit_and_tasks(expl, tt_profile[index].tasks, lift_usage, expl_begin, expl_end);
1063 // Transform literals to a clause
1064 reason = get_reason_for_update(expl);
1065 }
1066 // Increment filtering counter
1067 nb_tt_filt++;
1068 if (min_usage(i) <= 0) {
1069 // Impose the new upper bound on usage[i]
1070 if (! usage[i]->setMax(0, reason)) {
1071 // Conflict occurred
1072 return false;
1073 }
1074 }
1075 else {
1076 // Impose the new upper bound on usage[i]
1077 if (! dur[i]->setMax(0, reason)) {
1078 // Conflict occurred
1079 return false;
1080 }
1081 }
1082 }
1083 }
1084 }
1085 return true;
1086 }
1087
1088 int
find_first_profile_for_lb(ProfilePart profile[],int low,int high,CUMU_INT t)1089 CumulativeProp::find_first_profile_for_lb(ProfilePart profile[], int low, int high, CUMU_INT t) {
1090 int median;
1091 if (profile[low].end > t || low == high) {
1092 return low;
1093 }
1094 if (profile[high].begin <= t) {
1095 return high;
1096 }
1097 #if CUMUVERB>0
1098 fprintf(stderr, "time = %d\n", t);
1099 fprintf(stderr, "profile[low = %d] = [%d, %d); ", low, profile[low].begin, profile[low].end);
1100 fprintf(stderr, "profile[high = %d] = [%d, %d);\n", high, profile[high].begin, profile[high].end);
1101 #endif
1102 // ASSUMPTIONS:
1103 // - profile[low].end <= t
1104 // - profile[high].begin > t
1105 // - low < high
1106 //
1107 while (!(profile[low].end <= t && t <= profile[low + 1].end)) {
1108 median = low + (high - low + 1) / 2;
1109 #if CUMUVERB>0
1110 fprintf(stderr, "profile[lo = %d] = [%d, %d); ", low, profile[low].begin, profile[low].end);
1111 fprintf(stderr, "profile[me = %d] = [%d, %d); ", median, profile[median].begin, profile[median].end);
1112 fprintf(stderr, "profile[hi = %d] = [%d, %d);\n", high, profile[high].begin, profile[high].end);
1113 #endif
1114 if (t < profile[median].end) {
1115 high = median;
1116 //high = median - 1;
1117 low++;
1118 } else {
1119 low = median;
1120 }
1121 }
1122 return low;
1123 }
1124
1125 int
find_first_profile_for_ub(ProfilePart profile[],int low,int high,CUMU_INT t)1126 CumulativeProp::find_first_profile_for_ub(ProfilePart profile[], int low, int high, CUMU_INT t) {
1127 int median;
1128 if (profile[high].begin <= t || low == high) {
1129 return high;
1130 }
1131 if (t < profile[low].end) {
1132 return low;
1133 }
1134 // ASSUMPTIONS:
1135 // - profile[high].begin > t
1136 // - profile[low].end <= t
1137 // - low < high
1138 //
1139 while (!(profile[high - 1].begin <= t && t < profile[high].begin)) {
1140 median = low + (high - low + 1) / 2;
1141 if (t < profile[median].begin) {
1142 high = median;
1143 } else {
1144 low = median;
1145 high--;
1146 }
1147 }
1148 return high;
1149 }
1150
1151
1152 /************************************************************************
1153 * Functions for Analysing Conflicts or Bound Updates and Generation of *
1154 * their explanations *
1155 ************************************************************************/
1156
1157 void
analyse_limit_and_tasks(vec<Lit> & expl,set<CUMU_INT> & tasks,CUMU_INT lift_usage,CUMU_INT begin,CUMU_INT end)1158 CumulativeProp::analyse_limit_and_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end) {
1159 CUMU_INT diff_limit = max_limit0() - max_limit();
1160 if (diff_limit > 0) {
1161 // Lifting of limit variable if possible
1162 if (diff_limit <= lift_usage) {
1163 // No explanation literal is needed
1164 lift_usage -= diff_limit;
1165 } else {
1166 lift_usage = 0;
1167 // Get explanation for [[limit <= max_limit() + lift_usage]]
1168 #if CUMUVERB > 10
1169 fprintf(stderr, "/\\ limit <= %d ", max_limit() + lift_usage);
1170 #endif
1171 expl.push(getNegLeqLit(limit, max_limit() + lift_usage));
1172 }
1173 }
1174 analyse_tasks(expl, tasks, lift_usage, begin, end);
1175 }
1176
1177 void
analyse_tasks(vec<Lit> & expl,set<CUMU_INT> & tasks,CUMU_INT lift_usage,CUMU_INT begin,CUMU_INT end)1178 CumulativeProp::analyse_tasks(vec<Lit> & expl, set<CUMU_INT> & tasks, CUMU_INT lift_usage, CUMU_INT begin, CUMU_INT end) {
1179 set<CUMU_INT>::iterator iter;
1180 for (iter = tasks.begin(); iter != tasks.end(); iter++) {
1181 #if CUMUVERB > 10
1182 fprintf(stderr, "\ns[%d] in [%d..%d]\n", *iter, start[*iter]->getMin(), start[*iter]->getMax());
1183 #endif
1184 if (min_usage(*iter) <= lift_usage) {
1185 // Task is not relevant for the resource overload
1186 lift_usage -= min_usage(*iter);
1187 } else {
1188 // Task is relevant for the resource overload
1189 if (min_start0(*iter) + min_dur(*iter) <= end) {
1190 // Lower bound of the start time variable matters
1191 // Get explanation for [[start[*iter] >= end - min_dur(*iter)]]
1192 #if CUMUVERB > 10
1193 fprintf(stderr, "/\\ start[%d] => %d ", *iter, end - min_dur(*iter));
1194 #endif
1195 expl.push(getNegGeqLit(start[*iter], end - min_dur(*iter)));
1196 }
1197 if (begin < max_start0(*iter)) {
1198 // Upper bound of the start time variable matters
1199 // Get explanation for [[start[*iter] <= begin]]
1200 #if CUMUVERB > 10
1201 fprintf(stderr, "/\\ start[%d] <= %d ", *iter, begin);
1202 #endif
1203 expl.push(getNegLeqLit(start[*iter], begin));
1204 }
1205 // Get the negated literal for [[dur[*iter] >= min_dur(*iter)]]
1206 if (min_dur0(*iter) < min_dur(*iter))
1207 expl.push(getNegGeqLit(dur[*iter], min_dur(*iter)));
1208 // Get the negated literal for [[usage[*iter] >= min_usage(*iter)]]
1209 const CUMU_INT usage_diff = min_usage(*iter) - min_usage0(*iter);
1210 if (usage_diff > 0) {
1211 if (usage_diff <= lift_usage)
1212 lift_usage -= usage_diff;
1213 else
1214 expl.push(getNegGeqLit(usage[*iter], min_usage(*iter)));
1215 }
1216 }
1217 }
1218 }
1219
1220 void
submit_conflict_explanation(vec<Lit> & expl)1221 CumulativeProp::submit_conflict_explanation(vec<Lit> & expl) {
1222 Clause * reason = NULL;
1223 if (so.lazy) {
1224 reason = Reason_new(expl.size());
1225 int i = 0;
1226 for (; i < expl.size(); i++) { (*reason)[i] = expl[i]; }
1227 }
1228 sat.confl = reason;
1229 }
1230
1231 Clause *
get_reason_for_update(vec<Lit> & expl)1232 CumulativeProp::get_reason_for_update(vec<Lit> & expl) {
1233 Clause* reason = Reason_new(expl.size() + 1);
1234 for (int i = 1; i <= expl.size(); i++) {
1235 (*reason)[i] = expl[i-1];
1236 }
1237 return reason;
1238 }
1239
1240
1241 // XXX Which version of the cumulative constraint should be used?
1242 // Lifting the limit parameter to an integer variable
1243 //
cumulative(vec<IntVar * > & s,vec<int> & d,vec<int> & r,int limit)1244 void cumulative(vec<IntVar*>& s, vec<int>& d, vec<int>& r, int limit) {
1245 std::list<string> opt;
1246 cumulative(s, d, r, limit, opt);
1247 }
1248
cumulative(vec<IntVar * > & s,vec<int> & d,vec<int> & r,int limit,std::list<string> opt)1249 void cumulative(vec<IntVar*>& s, vec<int>& d, vec<int>& r, int limit, std::list<string> opt) {
1250 rassert(s.size() == d.size() && s.size() == r.size());
1251 // ASSUMPTION
1252 // - s, d, and r contain the same number of elements
1253
1254 // Option switch
1255 if (so.cumu_global) {
1256 vec<IntVar*> s_new, d_new, r_new;
1257 IntVar * vlimit = newIntVar(limit, limit);
1258 int r_sum = 0;
1259
1260 for (int i = 0; i < s.size(); i++) {
1261 if (r[i] > 0 && d[i] > 0) {
1262 s_new.push(s[i]);
1263 d_new.push(newIntVar(d[i], d[i]));
1264 r_new.push(newIntVar(r[i], r[i]));
1265 r_sum += r[i];
1266 }
1267 }
1268
1269 if (r_sum <= limit) return;
1270
1271 // Global cumulative constraint
1272 new CumulativeProp(s_new, d_new, r_new, vlimit, opt);
1273 } else {
1274 vec<IntVar*> s_new;
1275 vec<int> d_new, r_new;
1276 int r_sum = 0;
1277 for (int i = 0; i < s.size(); i++) {
1278 if (r[i] > 0 && d[i] > 0) {
1279 s_new.push(s[i]);
1280 d_new.push(d[i]);
1281 r_new.push(r[i]);
1282 r_sum += r[i];
1283 }
1284 }
1285
1286 if (r_sum <= limit) return;
1287
1288 // Time-indexed decomposition
1289 timed_cumulative(s_new, d_new, r_new, limit);
1290 }
1291 }
1292
cumulative2(vec<IntVar * > & s,vec<IntVar * > & d,vec<IntVar * > & r,IntVar * limit)1293 void cumulative2(vec<IntVar*>& s, vec<IntVar*>& d, vec<IntVar*>& r, IntVar* limit) {
1294 std:list<string> opt;
1295 cumulative2(s, d, r, limit, opt);
1296 }
1297
cumulative2(vec<IntVar * > & s,vec<IntVar * > & d,vec<IntVar * > & r,IntVar * limit,std::list<string> opt)1298 void cumulative2(vec<IntVar*>& s, vec<IntVar*>& d, vec<IntVar*>& r, IntVar* limit, std::list<string> opt) {
1299 rassert(s.size() == d.size() && s.size() == r.size());
1300 // ASSUMPTION
1301 // - s, d, and r contain the same number of elements
1302
1303 vec<IntVar*> s_new, d_new, r_new;
1304 int r_sum = 0;
1305
1306 for (int i = 0; i < s.size(); i++) {
1307 if (r[i]->getMax() > 0 && d[i]->getMax() > 0) {
1308 s_new.push(s[i]);
1309 d_new.push(d[i]);
1310 r_new.push(r[i]);
1311 r_sum += r[i]->getMax();
1312 }
1313 }
1314
1315 if (r_sum <= limit->getMin()) return;
1316
1317 // Global cumulative constraint
1318 new CumulativeProp(s_new, d_new, r_new, limit, opt);
1319 }
1320
1321 /********************************************
1322 * Functions related to the TTEF propagator
1323 *******************************************/
1324
1325 // Initialisation of various parameters
1326 //
1327 void
ttef_initialise_parameters()1328 CumulativeProp::ttef_initialise_parameters() {
1329 int energy = 0;
1330 int p_idx = tt_profile_size - 1;
1331
1332 // Initialisation of the task id's arrays
1333 //
1334 for (int ii = 0; ii <= last_unfixed; ii++) {
1335 task_id_est[ii] = task_id[ii];
1336 task_id_lct[ii] = task_id[ii];
1337 }
1338 if (ttef_filt) {
1339 for (int ii = 0; ii <= last_unfixed; ii++) {
1340 new_est[task_id[ii]] = est(task_id[ii]);
1341 new_lct[task_id[ii]] = lct(task_id[ii]);
1342 }
1343 }
1344 // Sorting of the task id's arrays
1345 //
1346 sort(task_id_est, task_id_est + last_unfixed + 1, sort_est_asc);
1347 sort(task_id_lct, task_id_lct + last_unfixed + 1, sort_lct_asc);
1348 // Calculation of 'tt_after_est'
1349 //
1350 for (int ii = last_unfixed; ii >= 0; ii--) {
1351 int i = task_id_est[ii];
1352 if (p_idx < 0 || tt_profile[p_idx].end <= est(i)) {
1353 tt_after_est[ii] = energy;
1354 } else if (tt_profile[p_idx].begin <= est(i)) {
1355 tt_after_est[ii] = energy + tt_profile[p_idx].level * (tt_profile[p_idx].end - est(i));
1356 } else {
1357 assert(tt_profile[p_idx].begin > est(i));
1358 energy += tt_profile[p_idx].level * (tt_profile[p_idx].end - tt_profile[p_idx].begin);
1359 p_idx--;
1360 ii++;
1361 }
1362 }
1363 // Calculation of 'tt_after_lct'
1364 //
1365 p_idx = tt_profile_size - 1;
1366 energy = 0;
1367 for (int ii = last_unfixed; ii >= 0; ii--) {
1368 unsigned i = task_id_lct[ii];
1369 if (p_idx < 0 || tt_profile[p_idx].end <= lct(i)) {
1370 tt_after_lct[ii] = energy;
1371 } else if (tt_profile[p_idx].begin <= lct(i)) {
1372 tt_after_lct[ii] = energy + tt_profile[p_idx].level * (tt_profile[p_idx].end - lct(i));
1373 } else {
1374 assert(tt_profile[p_idx].begin > lct(i));
1375 energy += tt_profile[p_idx].level * (tt_profile[p_idx].end - tt_profile[p_idx].begin);
1376 p_idx--;
1377 ii++;
1378 }
1379 }
1380 }
1381
1382 // TTEF Consistency Check
1383 // Assumptions:
1384 // - task_id_est sorted in non-decreasing order of est's
1385 // - task_id_lct sorted in non-decreasing order of lct's
1386 bool
ttef_consistency_check(int shift_in (const int,const int,const int,const int,const int,const int,const int))1387 CumulativeProp::ttef_consistency_check(
1388 int shift_in(const int, const int, const int, const int, const int, const int, const int)
1389 ) {
1390 assert(last_unfixed > 0);
1391 int begin, end; // Begin and end of the time interval [begin, end)
1392 int est_idx_last = last_unfixed;
1393 int i, j, en_req, en_avail;
1394 int en_req_free;
1395 int min_en_avail = -1, lct_idx_last = last_unfixed, i_last = task_id_lct[lct_idx_last];
1396 bool consistent = true;
1397
1398 end = lct(task_id_lct[last_unfixed]) + 1;
1399
1400 // Outer Loop: iterating over lct in non-increasing order
1401 //
1402 for (int ii = last_unfixed; ii >= 0; ii--) {
1403 i = task_id_lct[ii];
1404 if (end == lct(i) || min_energy(i) == 0) continue;
1405
1406 // Check whether the current latest completion time have to be considered
1407 int free = max_limit() * (lct(i_last) - lct(i)) - (tt_after_lct[ii] - tt_after_lct[lct_idx_last]);
1408 if (min_en_avail >= free) continue;
1409 lct_idx_last = ii;
1410 i_last = i;
1411 min_en_avail = max_limit() * (lct(task_id_lct[last_unfixed]) - est(task_id_est[0]));
1412
1413 end = lct(i);
1414 while (est(task_id_est[est_idx_last]) >= end) est_idx_last--;
1415 en_req_free = 0;
1416
1417 // Inner Loop: iterating over est in non-increasing order
1418 //
1419 for (int jj = est_idx_last; jj >= 0; jj--) {
1420 j = task_id_est[jj];
1421 if (min_energy(j) == 0) continue;
1422 assert(est(j) < end);
1423 begin = est(j);
1424 if (lct(j) <= end) {
1425 // Task lies in the considered time interval
1426 en_req_free += free_energy(j);
1427 } else {
1428 // Task might partially lie in the considered time interval
1429 int dur_fixed = max(0, ect(j) - lst(j));
1430 int dur_shift = shift_in(begin, end, est(j), ect(j), lst(j), lct(j), dur_fixed);
1431 en_req_free += min_usage(j) * dur_shift;
1432 }
1433 en_req = en_req_free + tt_after_est[jj] - tt_after_lct[ii];
1434 en_avail = max_limit() * (end - begin) - en_req;
1435
1436 min_en_avail = min(min_en_avail, en_avail);
1437
1438 // Check for resource overload
1439 //
1440 if (en_avail < 0) {
1441 consistent = false;
1442 ii = -1;
1443 break;
1444 }
1445 }
1446 }
1447
1448 if (!consistent) {
1449 vec<Lit> expl;
1450 // Increment the inconsistency counter
1451 nb_ttef_incons++;
1452 if (so.lazy) {
1453 list<TaskDur> tasks_tw;
1454 list<TaskDur> tasks_cp;
1455 int en_req1 = 0;
1456 // Retrieve tasks involved
1457 en_req1 = ttef_retrieve_tasks(shift_in, begin, end, -1, tasks_tw, tasks_cp);
1458 assert(en_req1 >= en_req);
1459 // Calculate the lifting
1460 int en_lift = en_req1 - 1 - max_limit() * (end - begin);
1461 assert(en_lift >= 0);
1462 // Explaining the overload
1463 ttef_analyse_limit_and_tasks(begin, end, tasks_tw, tasks_cp, en_lift, expl);
1464 }
1465 assert(expl.size() > 0);
1466 // Submitting of the conflict explanation
1467 submit_conflict_explanation(expl);
1468 }
1469 return consistent;
1470 }
1471
1472 // TTEF bounds propagation
1473 //
1474 bool
ttef_bounds_propagation(int shift_in1 (const int,const int,const int,const int,const int,const int,const int),int shift_in2 (const int,const int,const int,const int,const int,const int,const int))1475 CumulativeProp::ttef_bounds_propagation(
1476 int shift_in1(const int, const int, const int, const int, const int, const int, const int),
1477 int shift_in2(const int, const int, const int, const int, const int, const int, const int)
1478 ) {
1479 std::queue<TTEFUpdate> update1;
1480 std::queue<TTEFUpdate> update2;
1481 // TODO LB bound on the limit
1482 // LB bounds on the start times
1483 if (!ttef_bounds_propagation_lb(shift_in1, update1)) {
1484 // Inconsistency
1485 return false;
1486 }
1487 // TODO UB bounds on the start times
1488 if (!ttef_bounds_propagation_ub(shift_in2, update2)) {
1489 // Inconsistency
1490 return false;
1491 }
1492 // TODO Updating the bounds
1493 //printf("zzz %d\n", (int) update1.size());
1494 if (!ttef_update_bounds(shift_in1, update1)) {
1495 return false;
1496 }
1497 if (!ttef_update_bounds(shift_in2, update2)) {
1498 return false;
1499 }
1500 return true;
1501 }
1502
1503 bool
ttef_bounds_propagation_lb(int shift_in (const int,const int,const int,const int,const int,const int,const int),std::queue<TTEFUpdate> & update_queue)1504 CumulativeProp::ttef_bounds_propagation_lb(
1505 int shift_in(const int, const int, const int, const int, const int, const int, const int),
1506 std::queue<TTEFUpdate> & update_queue
1507 ) {
1508 assert(last_unfixed > 0);
1509 int begin, end; // Begin and end of the time interval [begin, end)
1510 int est_idx_last = last_unfixed;
1511 int i, j, en_req, en_avail;
1512 int en_req_free;
1513 int update_en_req_start, update_idx;
1514 //int min_en_avail = -1, lct_idx_last = last_unfixed, i_last = task_id_lct[lct_idx_last];
1515 int min_en_avail = -1, min_begin = -1;
1516 bool consistent = true;
1517
1518 end = lct(task_id_lct[last_unfixed]) + 1;
1519
1520 // Outer Loop: iterating over lct in non-increasing order
1521 //
1522 for (int ii = last_unfixed; ii >= 0; ii--) {
1523 i = task_id_lct[ii];
1524 if (end == lct(i) || min_energy(i) == 0) continue;
1525
1526 // Check whether the current latest completion time have to be considered
1527 //int free = max_limit() * (lct(i_last) - lct(i)) - (tt_after_lct[ii] - tt_after_lct[lct_idx_last]);
1528 //if (min_en_avail >= free) continue;
1529 //lct_idx_last = ii;
1530 //i_last = i;
1531 min_en_avail = max_limit() * (lct(task_id_lct[last_unfixed]) - est(task_id_est[0]));
1532 min_begin = -1;
1533
1534 end = lct(i);
1535 while (est(task_id_est[est_idx_last]) >= end) est_idx_last--;
1536 // Initialisations for the inner loop
1537 en_req_free = 0;
1538 update_idx = -1;
1539 update_en_req_start = -1;
1540
1541 // Inner Loop: iterating over est in non-increasing order
1542 //
1543 for (int jj = est_idx_last; jj >= 0; jj--) {
1544 j = task_id_est[jj];
1545 assert(est(j) < end);
1546 if (min_energy(j) == 0) continue;
1547 begin = est(j);
1548
1549 // Checking for TTEEF propagation on upper bound
1550 //
1551 int min_en_in = min_usage(j) * max(0, min(end, ect(j)) - max(min_begin, lst(j)));
1552 if (min_begin >= 0 && min_en_avail + min_en_in < min_usage(j) * (min(end, lct(j)) - max(min_begin, lst(j)))) {
1553 // Calculate new upper bound
1554 // XXX Is min_usage correct?
1555 int dur_avail = (min_en_avail + min_en_in) / min_usage(j);
1556 int lct_new = min_begin + dur_avail;
1557 // Check whether a new upper bound was found
1558 if (lct_new < new_lct[j]) {
1559 // Push possible update into the queue
1560 update_queue.push(TTEFUpdate(j, lct_new, min_begin, end, false));
1561 new_lct[j] = lct_new;
1562 //int blah = max_limit() * (end - min_begin) - (min_en_avail + min_en_in);
1563 //printf("%d: lct_new %d; dur_avail %d; en_req %d; [%d, %d)\n", j, lct_new, dur_avail, blah, min_begin, end);
1564 //printf("XXXXXX\n");
1565 }
1566 }
1567
1568 if (lct(j) <= end) {
1569 // Task lies in the considered time interval
1570 en_req_free += free_energy(j);
1571 } else {
1572 // Task might partially lie in the considered time interval
1573
1574 // Calculation of the energy part inside the time interavl
1575 int dur_fixed = max(0, ect(j) - lst(j));
1576 int dur_shift = shift_in(begin, end, est(j), ect(j), lst(j), lct(j), dur_fixed);
1577 en_req_free += min_usage(j) * dur_shift;
1578 // Calculation of the required energy for starting at est(j)
1579 int en_req_start = min(free_energy(j), min_usage(j) * (end - est(j))) - min_usage(j) * dur_shift;
1580 if (en_req_start > update_en_req_start) {
1581 update_en_req_start = en_req_start;
1582 update_idx = jj;
1583 }
1584 }
1585 en_req = en_req_free + tt_after_est[jj] - tt_after_lct[ii];
1586 en_avail = max_limit() * (end - begin) - en_req;
1587
1588 if (min_en_avail > en_avail) {
1589 min_en_avail = en_avail;
1590 min_begin = begin;
1591 }
1592
1593 // Check for resource overload
1594 //
1595 if (en_avail < 0) {
1596 consistent = false;
1597 ii = -1;
1598 break;
1599 }
1600
1601 // Check for a start time update
1602 //
1603 if (en_avail < update_en_req_start) {
1604 // Reset 'j' to the task to be updated
1605 j = task_id_est[update_idx];
1606 // Calculation of the possible new lower bound wrt.
1607 // the current time interval
1608 int dur_mand = max(0, min(end, ect(j)) - lst(j));
1609 int dur_shift = shift_in(begin, end, est(j), ect(j), lst(j), lct(j), dur_mand);
1610 int en_in = min_usage(j) * (dur_mand + dur_shift);
1611 int en_avail_new = en_avail + en_in;
1612 // XXX Is min_usage correct?
1613 int dur_avail = en_avail_new / min_usage(j);
1614 int start_new = end - dur_avail;
1615 // TODO Check whether a new lower bound was found
1616 // - nfnl-rule TODO
1617 if (start_new > new_est[j]) {
1618 // Push possible update into the queue
1619 update_queue.push(TTEFUpdate(j, start_new, begin, end, true));
1620 new_est[j] = start_new;
1621 //printf("XXXXXX\n");
1622 }
1623 }
1624 }
1625 }
1626
1627 if (!consistent) {
1628 vec<Lit> expl;
1629 // Increment the inconsistency counter
1630 nb_ttef_incons++;
1631 if (so.lazy) {
1632 list<TaskDur> tasks_tw;
1633 list<TaskDur> tasks_cp;
1634 int en_req1 = 0;
1635 // Retrieve tasks involved
1636 en_req1 = ttef_retrieve_tasks(shift_in, begin, end, -1, tasks_tw, tasks_cp);
1637 assert(en_req1 >= en_req);
1638 // Calculate the lifting
1639 int en_lift = en_req1 - 1 - max_limit() * (end - begin);
1640 assert(en_lift >= 0);
1641 // Explaining the overload
1642 ttef_analyse_limit_and_tasks(begin, end, tasks_tw, tasks_cp, en_lift, expl);
1643 assert(expl.size() > 0);
1644 }
1645 // Submitting of the conflict explanation
1646 submit_conflict_explanation(expl);
1647 }
1648 return consistent;
1649 }
1650
1651 bool
ttef_bounds_propagation_ub(int shift_in (const int,const int,const int,const int,const int,const int,const int),std::queue<TTEFUpdate> & update_queue)1652 CumulativeProp::ttef_bounds_propagation_ub(
1653 int shift_in(const int, const int, const int, const int, const int, const int, const int),
1654 std::queue<TTEFUpdate> & update_queue
1655 ) {
1656 assert(last_unfixed > 0);
1657 int begin, end; // Begin and end of the time interval [begin, end)
1658 int lct_idx_last = 0;
1659 int i, j, en_req, en_avail;
1660 int en_req_free;
1661 int update_en_req_end, update_idx;
1662 //int min_en_avail = -1, lct_idx_last = last_unfixed, i_last = task_id_lct[lct_idx_last];
1663 int min_en_avail = -1, min_end = -1;
1664 bool consistent = true;
1665
1666 begin = est(task_id_est[0]) - 1;
1667
1668 // Outer Loop: iterating over est in non-decreasing order
1669 //
1670 for (int ii = 0; ii <= last_unfixed; ii++) {
1671 i = task_id_est[ii];
1672 if (begin == est(i) || min_energy(i) == 0) continue;
1673
1674 // Intialisation for the minimal avaible energy of a time interval starting
1675 // at begin
1676 // TODO dominance rule for skipping time intervals
1677 min_en_avail = max_limit() * (lct(task_id_lct[last_unfixed]) - est(task_id_est[0]));
1678 min_end = -1;
1679
1680 begin = est(i);
1681 while (lct(task_id_lct[lct_idx_last]) <= begin) lct_idx_last++;
1682 // Initialisations for the inner loop
1683 en_req_free = 0;
1684 update_idx = -1;
1685 update_en_req_end = -1;
1686
1687 // Inner Loop: iterating over lct in non-decreasing order
1688 //
1689 for (int jj = lct_idx_last; jj <= last_unfixed; jj++) {
1690 j = task_id_lct[jj];
1691 assert(lct(j) > begin);
1692 if (min_energy(j) == 0) continue;
1693 end = lct(j);
1694
1695 // Checking for TTEEF propagation on lower bounds
1696 //
1697 int min_en_in = min_usage(j) * max(0, min(min_end, ect(j)) - max(begin, lst(j)));
1698 if (min_end >= 0 && min_en_avail + min_en_in < min_usage(j) * (min(min_end, ect(j)) - max(begin, est(j)))) {
1699 // Calculate new upper bound
1700 // XXX Is min_usage correct?
1701 int dur_avail = (min_en_avail + min_en_in) / min_usage(j);
1702 int est_new = min_end - dur_avail;
1703 // Check whether a new lower bound was found
1704 if (est_new > new_est[j]) {
1705 // Push possible update into the queue
1706 update_queue.push(TTEFUpdate(j, est_new, begin, min_end, true));
1707 new_est[j] = est_new;
1708 //int blah = max_limit() * (end - min_begin) - (min_en_avail + min_en_in);
1709 //printf("%d: lct_new %d; dur_avail %d; en_req %d; [%d, %d)\n", j, lct_new, dur_avail, blah, min_begin, end);
1710 //printf("XXXXXX\n");
1711 }
1712 }
1713
1714 if (begin <= est(j)) {
1715 // Task lies in the considered time interval [begin, end)
1716 en_req_free += free_energy(j);
1717 } else {
1718 // Task might partially lie in the considered time interval
1719
1720 // Calculation of the energy part inside the time interval
1721 int dur_fixed = max(0, ect(j) - lst(j));
1722 int dur_shift = shift_in(begin, end, est(j), ect(j), lst(j), lct(j), dur_fixed);
1723 en_req_free += min_usage(j) * dur_shift;
1724 // Calculation of the required energy for finishing at 'lct(j)'
1725 int en_req_end = min(free_energy(j), min_usage(j) * (lct(j) - begin)) - min_usage(j) * dur_shift;
1726 if (en_req_end > update_en_req_end) {
1727 update_en_req_end = en_req_end;
1728 update_idx = jj;
1729 }
1730 }
1731 en_req = en_req_free + tt_after_est[ii] - tt_after_lct[jj];
1732 en_avail = max_limit() * (end - begin) - en_req;
1733
1734 if (min_en_avail > en_avail) {
1735 min_en_avail = en_avail;
1736 min_end = end;
1737 }
1738
1739 // Check for resource overload
1740 //
1741 if (en_avail < 0) {
1742 consistent = false;
1743 ii = last_unfixed + 1;
1744 break;
1745 }
1746
1747 // Check for a start time update
1748 //
1749 if (en_avail < update_en_req_end) {
1750 // Reset 'j' to the task to be updated
1751 j = task_id_lct[update_idx];
1752 // Calculation of the possible upper bound wrt.
1753 // the current time interval
1754 int dur_mand = max(0, ect(j) - max(begin, lst(j)));
1755 int dur_shift = shift_in(begin, end, est(j), ect(j), lst(j), lct(j), dur_mand);
1756 int en_in = min_usage(j) * (dur_mand + dur_shift);
1757 int en_avail_new = en_avail + en_in;
1758 // XXX Is min_usage correct?
1759 int dur_avail = en_avail_new / min_usage(j);
1760 int end_new = begin + dur_avail;
1761 // TODO Check whether a new uppder bound was found
1762 // - nfnl-rule TODO
1763 if (end_new < new_lct[j]) {
1764 // Push possible update into queue
1765 update_queue.push(TTEFUpdate(j, end_new, begin, end, false));
1766 new_lct[j] = end_new;
1767 }
1768 }
1769 }
1770 }
1771
1772 if (!consistent) {
1773 vec<Lit> expl;
1774 // Increment the inconsistency counter
1775 nb_ttef_incons++;
1776 if (so.lazy) {
1777 list<TaskDur> tasks_tw;
1778 list<TaskDur> tasks_cp;
1779 int en_req1 = 0;
1780 // Retrieve tasks involved
1781 en_req1 = ttef_retrieve_tasks(shift_in, begin, end, -1, tasks_tw, tasks_cp);
1782 assert(en_req1 >= en_req);
1783 // Calculate the lifting
1784 int en_lift = en_req1 - 1 - max_limit() * (end - begin);
1785 assert(en_lift >= 0);
1786 // Explaining the overload
1787 ttef_analyse_limit_and_tasks(begin, end, tasks_tw, tasks_cp, en_lift, expl);
1788 assert(expl.size() > 0);
1789 }
1790 // Submitting of the conflict explanation
1791 submit_conflict_explanation(expl);
1792 }
1793 return consistent;
1794 }
1795
1796 bool
ttef_update_bounds(int shift_in (const int,const int,const int,const int,const int,const int,const int),std::queue<TTEFUpdate> & queue_update)1797 CumulativeProp::ttef_update_bounds(
1798 int shift_in(const int, const int, const int, const int, const int, const int, const int),
1799 std::queue<TTEFUpdate> & queue_update
1800 ) {
1801 while (!queue_update.empty()) {
1802 int task = queue_update.front().task;
1803 int bound = queue_update.front().bound_new;
1804 int begin = queue_update.front().tw_begin;
1805 int end = queue_update.front().tw_end;
1806 Clause * reason = NULL;
1807 if (queue_update.front().is_lb_update) {
1808 // Lower bound update
1809 if (new_est[task] == bound) {
1810 if (so.lazy) {
1811 vec<Lit> expl;
1812 list<TaskDur> tasks_tw;
1813 list<TaskDur> tasks_cp;
1814 // Retrieving tasks involved
1815 int en_req = ttef_retrieve_tasks(shift_in, begin, end, task, tasks_tw, tasks_cp);
1816
1817 // Lifting for the lower bound of 'task'
1818 //
1819 int en_avail = max_limit() * (end - begin) - en_req;
1820 // XXX Is min_usage correct?
1821 int dur_avail = en_avail / min_usage(task);
1822 assert(end - dur_avail >= bound);
1823 // XXX Is min_usage correct?
1824 assert(en_avail < min_usage(task) * (min(end, ect(task)) - max(begin, est(task))));
1825 bound = end - dur_avail;
1826 int expl_lb;
1827
1828 switch (ttef_expl_deg) {
1829 case ED_NORMAL:
1830 case ED_LIFT:
1831 // XXX Is min_dur correct?
1832 expl_lb = max(min_start0(task), begin + dur_avail + 1 - min_dur(task));
1833 break;
1834 case ED_NAIVE:
1835 default:
1836 expl_lb = est(task);
1837 }
1838 // Lifting from the remainder
1839 int en_lift = min_usage(task) - 1 - (en_avail % min_usage(task));
1840 // Lifting from 'expl_lb'
1841 en_lift += min_usage(task) * (expl_lb + min_dur(task) - (begin + dur_avail + 1));
1842 assert(expl_lb + min_dur(task) - (begin + dur_avail + 1) >= 0);
1843 assert(en_lift >= 0);
1844
1845 // Explaining the update
1846 //
1847 if (expl_lb > min_start0(task)) {
1848 // start[task] >= expl_lb
1849 expl.push(getNegGeqLit(start[task], expl_lb));
1850 }
1851 // Get the negated literal for [[dur[task] >= min_dur(task)]]
1852 if (min_dur0(task) < min_dur(task))
1853 expl.push(getNegGeqLit(dur[task], min_dur(task)));
1854 // Get the negated literal for [[usage[task] >= min_usage(task)]]
1855 if (min_usage0(task) < min_usage(task))
1856 expl.push(getNegGeqLit(usage[task], min_usage(task)));
1857 ttef_analyse_limit_and_tasks(begin, end, tasks_tw, tasks_cp, en_lift, expl);
1858 reason = get_reason_for_update(expl);
1859 }
1860 // Increment the filtering counter
1861 nb_ttef_filt++;
1862 // Update the lower bound
1863 if (!start[task]->setMin(bound, reason)) {
1864 // Conflict occurred
1865 return false;
1866 }
1867 // Set bound_update to true
1868 bound_update = true;
1869 }
1870 } else {
1871 // Upper bound update
1872 if (new_lct[task] == bound) {
1873 if (so.lazy) {
1874 vec<Lit> expl;
1875 list<TaskDur> tasks_tw;
1876 list<TaskDur> tasks_cp;
1877 // Retrieving tasks involved
1878 int en_req = ttef_retrieve_tasks(shift_in, begin, end, task, tasks_tw, tasks_cp);
1879
1880 // Lifting for the upper bound of 'task'
1881 //
1882 int en_avail = max_limit() * (end - begin) - en_req;
1883 // XXX Is min_usage correct?
1884 int dur_avail = en_avail / min_usage(task);
1885 //printf("%d: bound %d; dur_avail %d; en_req %d; [%d, %d)\n", task, bound, dur_avail, en_req, begin, end);
1886 assert(begin + dur_avail <= bound);
1887 // assert(en_avail < usage[task] * (min(end, lct(task)) - max(begin, lst(task))));
1888 bound = begin + dur_avail;
1889 int expl_ub;
1890
1891 switch (ttef_expl_deg) {
1892 case ED_NORMAL:
1893 case ED_LIFT:
1894 expl_ub = min(max_start0(task), end - dur_avail - 1);
1895 break;
1896 case ED_NAIVE:
1897 default:
1898 expl_ub = lst(task);
1899 }
1900 // Lifting from the remainder
1901 // XXX Is min_usage correct
1902 int en_lift = min_usage(task) - 1 - (en_avail % min_usage(task));
1903 // Lifting from 'expl_ub'
1904 en_lift += min_usage(task) * (end - dur_avail - 1 - expl_ub);
1905 assert(end - dur_avail - 1 - expl_ub >= 0);
1906 assert(en_lift >= 0);
1907
1908 // Explaining the update
1909 //
1910 if (expl_ub < max_start0(task)) {
1911 // start[task] <= expl_ub
1912 expl.push(getNegLeqLit(start[task], expl_ub));
1913 }
1914 // Get the negated literal for [[dur[task] >= min_dur(task)]]
1915 if (min_dur0(task) < min_dur(task))
1916 expl.push(getNegGeqLit(dur[task], min_dur(task)));
1917 // Get the negated literal for [[usage[task] >= min_usage(task)]]
1918 if (min_usage0(task) < min_usage(task))
1919 expl.push(getNegGeqLit(usage[task], min_usage(task)));
1920 ttef_analyse_limit_and_tasks(begin, end, tasks_tw, tasks_cp, en_lift, expl);
1921 reason = get_reason_for_update(expl);
1922
1923 }
1924 // Increment the filtering counter
1925 nb_ttef_filt++;
1926 // Update the lower bound
1927 // XXX Is min_dur correct?
1928 if (!start[task]->setMax(bound - min_dur(task), reason)) {
1929 // Conflict occurred
1930 return false;
1931 }
1932 // Set bound_update to true
1933 bound_update = true;
1934 }
1935 }
1936 queue_update.pop();
1937 }
1938
1939 return true;
1940 }
1941
1942 int
ttef_retrieve_tasks(int shift_in (const int,const int,const int,const int,const int,const int,const int),int begin,int end,int fb_id,list<TaskDur> & tasks_tw,list<TaskDur> & tasks_cp)1943 CumulativeProp::ttef_retrieve_tasks(
1944 int shift_in(const int, const int, const int, const int, const int, const int, const int),
1945 int begin, int end, int fb_id, list<TaskDur> & tasks_tw, list<TaskDur> & tasks_cp)
1946 {
1947 int en_req = 0;
1948 //printf("* [%d, %d): #tasks %d; fixed %d\n", begin, end, task_id.size(), (int) last_unfixed);
1949 // Getting fixed tasks
1950 for (int ii = 0; ii < task_id.size(); ii++) {
1951 int i = task_id[ii];
1952 if (i == fb_id || min_energy(i) == 0) continue;
1953 //printf("\t%d: est %d; ect %d; lst %d; lct %d (dur: %d; rr: %d; en: %d)\n", i, est(i), ect(i), lst(i), lct(i),
1954 // min_dur(i), min_usage(i), min_energy(i));
1955 if (begin <= est(i) && lct(i) <= end) {
1956 // Task lies in the time interval [begin, end)
1957 en_req += min_energy(i);
1958 tasks_tw.push_back(TaskDur(i, min_dur(i)));
1959 //printf("\tFull %d: %d in [%d, %d)\n", i, min_energy(i), begin, end);
1960 //printf("\t\t%d: est %d; ect %d; lst %d; lct %d (dur: %d; rr: %d; en: %d)\n", i, est(i), ect(i), lst(i), lct(i),
1961 // min_dur(i), min_usage(i), min_energy(i));
1962 } else if (lst(i) < ect(i) && is_intersecting(begin, end, lst(i), ect(i))) {
1963 // Compulsory part partially or fully lies in [begin, end)
1964 int dur_comp = min(end, ect(i)) - max(begin, lst(i));
1965 int dur_shift = shift_in(begin, end, est(i), ect(i), lst(i), lct(i), dur_comp);
1966 int dur_in = dur_comp + dur_shift;
1967 en_req += min_usage(i) * dur_in;
1968 tasks_cp.push_back(TaskDur(i, dur_in));
1969 //printf("\tComp %d: %d in [%d, %d)\n", i, min_usage(i) * dur_in, begin, end);
1970 //printf("\t\t%d: est %d; ect %d; lst %d; lct %d (dur: %d; rr: %d; en: %d)\n", i, est(i), ect(i), lst(i), lct(i),
1971 // min_dur(i), min_usage(i), min_energy(i));
1972 } else if (0 < shift_in(begin, end, est(i), ect(i), lst(i), lct(i), 0)) {
1973 // Task partially lies in [begin, end)
1974 int dur_in = shift_in(begin, end, est(i), ect(i), lst(i), lct(i), 0);
1975 en_req += min_usage(i) * dur_in;
1976 tasks_tw.push_back(TaskDur(i, dur_in));
1977 //printf("Shift %d: %d in [%d, %d)\n", i, min_usage(i) * dur_in, begin, end);
1978 }
1979 }
1980 return en_req;
1981 }
1982
1983 void
ttef_analyse_limit_and_tasks(const int begin,const int end,list<TaskDur> & tasks_tw,list<TaskDur> & tasks_cp,int & en_lift,vec<Lit> & expl)1984 CumulativeProp::ttef_analyse_limit_and_tasks(const int begin, const int end, list<TaskDur> & tasks_tw,
1985 list<TaskDur> & tasks_cp, int & en_lift, vec<Lit> & expl)
1986 {
1987 // Getting explanation for tasks in the time window
1988 ttef_analyse_tasks(begin, end, tasks_tw, en_lift, expl);
1989 // Getting explanation for tasks with compulsory parts
1990 ttef_analyse_tasks(begin, end, tasks_cp, en_lift, expl);
1991 // Getting explanation for the resource capacity
1992 int diff_limit = max_limit0() - max_limit();
1993 if (diff_limit > 0) {
1994 // Calculate possible lifting
1995 int lift_limit = min(en_lift / (end - begin), diff_limit);
1996 en_lift -= lift_limit * (end - begin);
1997 assert(en_lift >= 0);
1998 if (lift_limit < diff_limit) {
1999 // limit[%d] <= max_limit() + lift_limit
2000 expl.push(getNegLeqLit(limit, max_limit() + lift_limit));
2001 }
2002 }
2003 }
2004
2005 void
ttef_analyse_tasks(const int begin,const int end,list<TaskDur> & tasks,int & en_lift,vec<Lit> & expl)2006 CumulativeProp::ttef_analyse_tasks(const int begin, const int end, list<TaskDur> & tasks, int & en_lift, vec<Lit> & expl) {
2007 while (!tasks.empty()) {
2008 int i = tasks.front().task;
2009 int dur_in = tasks.front().dur_in;
2010 int expl_lb, expl_ub;
2011 int est0 = min_start0(i);
2012 int lst0 = max_start0(i);
2013 // Calculate possible lifting
2014 switch (ttef_expl_deg) {
2015 case ED_NORMAL:
2016 // XXX Is min_dur correct
2017 expl_lb = begin + dur_in - min_dur(i); expl_ub = end - dur_in;
2018 break;
2019 case ED_LIFT: {
2020 int dur_max_out0 = max(0, max(lst0 + min_dur(i) - end, begin - est0));
2021 int dur_max_out = min(dur_max_out0, dur_in);
2022 // XXX Is min_usage correct?
2023 int dur_lift = min(en_lift / min_usage(i), dur_max_out);
2024 //printf("\t%d: dur_in %d, dur_lift %d; max_out0 %d; max_out %d; %d\n", i, dur_in, dur_lift, dur_max_out0, dur_max_out, en_lift /dur[i]);
2025 //printf("\t\t est0 %d, lst0 %d\n", est0, lst0);
2026 en_lift -= min_usage(i) * dur_lift;
2027 assert(en_lift >= 0);
2028 if (dur_lift < dur_in) {
2029 // XXX Is min_dur correct?
2030 expl_lb = begin + dur_in - dur_lift - min_dur(i);
2031 expl_ub = end - dur_in + dur_lift;
2032 } else {
2033 expl_lb = est0;
2034 expl_ub = lst0;
2035 }}
2036 break;
2037 case ED_NAIVE:
2038 default:
2039 expl_lb = est(i); expl_ub = lst(i);
2040 }
2041 //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);
2042 if (est0 < expl_lb) {
2043 //printf("s[%d] >= %d; ", i, expl_lb);
2044 expl.push(getNegGeqLit(start[i], expl_lb));
2045 }
2046 if (expl_ub < lst0) {
2047 //printf("s[%d] <= %d; ", i, expl_ub);
2048 expl.push(getNegLeqLit(start[i], expl_ub));
2049 }
2050 // Get the negated literal for [[dur[i] >= min_dur(i)]]
2051 if (min_dur0(i) < min_dur(i))
2052 expl.push(getNegGeqLit(dur[i], min_dur(i)));
2053 // Get the negated literal for [[usage[i] >= min_usage(i)]]
2054 if (min_usage0(i) < min_usage(i))
2055 expl.push(getNegGeqLit(usage[i], min_usage(i)));
2056 //printf("\n");
2057 tasks.pop_front();
2058 }
2059 }
2060
2061 inline bool
is_intersecting(const int begin1,const int end1,const int begin2,const int end2)2062 CumulativeProp::is_intersecting(const int begin1, const int end1, const int begin2, const int end2) {
2063 return ((begin1 <= begin2 && begin2 < end1) || (begin2 <= begin1 && begin1 < end2));
2064 }
2065
2066 /*** EOF ***/
2067
2068