1 #ifndef PARTITION_STACK_CDJUCD 2 #define PARTITION_STACK_CDJUCD 3 #include <vector> 4 #include <assert.h> 5 #include <sstream> 6 #include <set> 7 #include <map> 8 #include <limits> 9 10 #include "library/optional.hpp" 11 #include "library/algorithms.hpp" 12 #include "library/vec1.hpp" 13 #include "library/sorter.hpp" 14 #include "queue/abstract_queue.hpp" 15 #include "memory_backtrack.hpp" 16 17 /// A store of all the information we need 18 /// to efficently backtrack the state. 19 struct PartitionSplit 20 { 21 int cell; 22 int splitpos; 23 PartitionSplitPartitionSplit24 PartitionSplit(int _c, int _s) : 25 cell(_c), splitpos(_s) 26 { } 27 PartitionSplitPartitionSplit28 PartitionSplit() {} 29 }; 30 31 class MarkStore 32 { 33 /// maintain data structures for cellOfVal and cellOfPos 34 bool enable_cellOfFunctions; 35 36 vec1<int> marks_m; 37 38 public: 39 has_cellOf() const40 bool has_cellOf() const 41 { return enable_cellOfFunctions; } 42 MarkStore(int n)43 MarkStore(int n) 44 : enable_cellOfFunctions(false), marks_m(n+1,0) 45 { 46 marks_m[1] = 1; 47 marks_m[n+1] = std::numeric_limits<int>::max(); 48 enable_cellOf(); 49 } 50 51 // TODO : Make this O(cell) instead of O(n) cellOfPos(int pos)52 int cellOfPos(int pos) 53 { 54 D_ASSERT(enable_cellOfFunctions); 55 return std::abs(marks_m[pos]); 56 } 57 marks(int pos) const58 int marks(int pos) const 59 { return marks_m[pos]; } 60 add_cell_marker(int val,int pos,int length)61 void add_cell_marker(int val, int pos, int length) 62 { 63 marks_m[pos] = val; 64 clean_marks_array(pos, pos + length); 65 } 66 remove_cell_marker(int val,int pos,int length)67 void remove_cell_marker(int val, int pos, int length) 68 { 69 val = -val; 70 D_ASSERT(marks_m[pos] > 0); 71 for(int i = pos; i < pos + length; ++i) 72 { 73 D_ASSERT(i == pos || marks_m[i] < 0); 74 marks_m[i] = val; 75 } 76 } 77 clean_marks_array(int startpos,int endpos)78 void clean_marks_array(int startpos, int endpos) 79 { 80 if(!enable_cellOfFunctions) 81 return; 82 int cell = -marks_m[startpos]; 83 for(int i = startpos + 1; i < endpos; ++i) 84 { 85 D_ASSERT(marks_m[i] <= 0); 86 marks_m[i] = cell; 87 } 88 } 89 enable_cellOf()90 void enable_cellOf() 91 { 92 if(enable_cellOfFunctions) 93 return; 94 95 enable_cellOfFunctions = true; 96 int cell = 1; 97 for(int i : range1(marks_m.size())) 98 { 99 if(marks_m[i] > 0) 100 cell = marks_m[i]; 101 else 102 marks_m[i] = -cell; 103 } 104 } 105 }; 106 107 class PartitionStack : public BacktrackableType 108 { 109 AbstractQueue* aq; 110 vec1<PartitionSplit> backtrack_stack; 111 112 vec1<int> backtrack_depths; 113 114 MarkStore markstore; 115 116 /// Maximum domain value 117 int n; 118 119 // The partition, and it's inverse 120 // NOTE: To help the gap<->C++ integration, 121 // these are 1-based arrays (ignore value 0) 122 vec1<int> vals; 123 vec1<int> invvals; 124 125 // Store explicit list of fixed cells 126 vec1<int> fixed; 127 128 // Store explicit list of the values in fixed cells 129 vec1<int> fixed_vals; 130 131 132 /// Starts of cells 133 vec1<int> cellstart; 134 /// Sizes of cells 135 vec1<int> cellsize; 136 137 /// Number of cells at push events 138 vec1<int> pushes; 139 140 public: 141 cellStarts()142 const vec1<int>& cellStarts() 143 { return cellstart; } 144 cellSizes()145 const vec1<int>& cellSizes() 146 { return cellsize; } 147 setAbstractQueue(AbstractQueue * new_aq)148 void setAbstractQueue(AbstractQueue* new_aq) 149 { aq = new_aq; } 150 getAbstractQueue()151 AbstractQueue* getAbstractQueue() 152 { return aq; } 153 154 // This is a safety mechanism -- in general 155 // copying a PartitionStack is a bad idea, but in some 156 // situations we want to. clone()157 PartitionStack* clone() 158 { 159 PartitionStack* ps = new PartitionStack(n, NULL, NULL); 160 ps->vals = vals; 161 ps->invvals = invvals; 162 ps->fixed = fixed; 163 ps->fixed_vals = fixed_vals; 164 ps->markstore = markstore; 165 ps->cellstart = cellstart; 166 ps->cellsize = cellsize; 167 ps->pushes = pushes; 168 169 return ps; 170 } 171 addTrigger(AbstractConstraint * ac,TriggerType tt)172 void addTrigger(AbstractConstraint* ac, TriggerType tt) 173 { aq->addTrigger(ac, tt); } 174 175 typedef vec1<int>::iterator cellit; 176 PartitionStack(int _n,AbstractQueue * _aq,MemoryBacktracker * mb)177 PartitionStack(int _n, AbstractQueue* _aq, MemoryBacktracker* mb) : 178 BacktrackableType(mb), aq(_aq), markstore(_n), 179 n(_n), vals(n), invvals(n) 180 { 181 backtrack_depths.push_back(1); 182 183 for(int i : range1(n)) 184 { 185 vals[i] = i; 186 invvals[i] = i; 187 } 188 cellstart.push_back(1); 189 cellsize.push_back(n); 190 191 D_SLOW_ASSERT(sanity_check()); 192 } 193 194 /// Get number of points in partition domainSize() const195 int domainSize() const 196 { return n; } 197 cellCount() const198 int cellCount() const 199 { return cellstart.size(); } 200 cellSize(int i) const201 int cellSize(int i) const 202 { 203 return cellsize[i]; 204 } 205 cellStartPos(int i) const206 int cellStartPos(int i) const 207 { 208 return cellstart[i]; 209 } 210 cellStartPtr(int i)211 cellit cellStartPtr(int i) 212 { return valPtr(cellStartPos(i)); } 213 cellEndPos(int i) const214 int cellEndPos(int i) const 215 { 216 D_ASSERT(i > 0 && i <= cellCount()); 217 return cellstart[i] + cellsize[i]; 218 } 219 cellEndPtr(int i)220 cellit cellEndPtr(int i) 221 { return valPtr(cellEndPos(i)); } 222 cellRange(int i)223 Range<cellit> cellRange(int i) 224 { return rangeWrap(cellStartPtr(i), cellEndPtr(i)); } 225 val(int pos)226 int val(int pos) 227 { return *valPtr(pos); } 228 invval(int pos)229 int invval(int pos) 230 { return *invvalPtr(pos); } 231 val_ref() const232 const vec1<int>& val_ref() const 233 { return vals; } 234 invval_ref() const235 const vec1<int>& invval_ref() const 236 { return invvals; } 237 cellAsVec(int cell)238 vec1<int> cellAsVec(int cell) 239 { 240 return vec1<int>(cellStartPtr(cell), cellEndPtr(cell)); 241 } 242 cellOfVal(int val)243 int cellOfVal(int val) 244 { 245 return cellOfPos(invvals[val]); 246 } 247 248 // TODO : Make this O(cell) instead of O(n) cellOfPos(int pos)249 int cellOfPos(int pos) 250 { 251 return markstore.cellOfPos(pos); 252 } 253 valPtr(int pos)254 cellit valPtr(int pos) 255 { return vals.begin() + (pos - 1); } 256 invvalPtr(int pos)257 cellit invvalPtr(int pos) 258 { return invvals.begin() + (pos - 1); } 259 valStart()260 cellit valStart() 261 { return vals.begin(); } 262 invvalStart()263 cellit invvalStart() 264 { return invvals.begin(); } 265 fixed_cells() const266 const vec1<int>& fixed_cells() const 267 { return fixed; } 268 fixed_values() const269 const vec1<int>& fixed_values() const 270 { return fixed_vals; } 271 272 /// Sanity checks all internal state of partition stack 273 /// Warning: May be expensive! sanity_check()274 bool sanity_check() 275 { 276 assert(vals.size() == n); 277 assert(invvals.size() == n); 278 279 for(int i : range1(n)) 280 { 281 assert(invvals[vals[i]] == i); 282 assert(vals[invvals[i]] == i); 283 } 284 285 assert(contains_no_repeats(fixed)); 286 assert(fixed.size() == fixed_vals.size()); 287 for(int i : range1(fixed.size())) 288 { 289 assert(cellsize[fixed[i]] == 1); 290 assert(*(cellStartPtr(fixed[i])) == fixed_vals[i]); 291 } 292 293 294 assert(contains_no_repeats(cellstart)); 295 assert(cellstart.size() == cellsize.size()); 296 assert(cellstart[1] == 1); 297 assert(cellstart[1]+cellsize[1] != 0); 298 299 int fixed_count = 0; 300 301 for(int i : range1(cellCount())) 302 { 303 assert(cellsize[i] > 0); 304 if(cellsize[i] == 1) 305 fixed_count++; 306 assert(markstore.marks(cellstart[i]) == i); 307 assert(cellOfPos(cellstart[i]) == i); 308 assert(cellOfVal(val(cellstart[i])) == i); 309 for(int j = 1; j < cellsize[i]; ++j) 310 { 311 int expected_value = markstore.has_cellOf()?-i:0; 312 assert(markstore.marks(cellstart[i] + j) == expected_value); 313 // Re-enable these when cellOfPos gets a non-trivial 314 // implementation 315 if(markstore.has_cellOf()) 316 { 317 assert(cellOfPos(cellstart[i] + j) == i); 318 assert(cellOfVal(val(cellstart[i]+j)) == i); 319 } 320 } 321 } 322 assert(fixed.size() == fixed_count); 323 324 if(markstore.has_cellOf()) 325 { 326 int cell = 99999; // random number 327 for(int i : range1(n)) 328 { 329 assert(markstore.marks(i) != 0); 330 331 if(markstore.marks(i) > 0) 332 { 333 cell = markstore.marks(i); 334 assert(cellstart[markstore.marks(i)] == i); 335 } 336 else 337 { 338 assert(markstore.marks(i) == -cell); 339 } 340 } 341 } 342 else 343 { 344 for(int i : range1(n)) 345 { 346 if(markstore.marks(i) != 0) 347 assert(cellstart[markstore.marks(i)] == i); 348 } 349 } 350 return true; 351 } 352 353 split(int cell,int pos)354 SplitState split(int cell, int pos) 355 { 356 D_ASSERT(pos > cellStartPos(cell)); 357 D_ASSERT(pos < cellEndPos(cell)); 358 359 360 // We allow attempts to split an empty 361 // piece off a cell, and just ignore it 362 // if(pos == cellStartPos(cell) || 363 // pos == cellEndPos(cell)) 364 // return SplitState(true); 365 366 367 // Should always be true, just sanity check 368 D_ASSERT(cellsize[cell] > 1); 369 370 int original_first_cell_length = cellsize[cell]; 371 int new_first_cell_length = pos - cellStartPos(cell); 372 int new_second_cell_length = original_first_cell_length - new_first_cell_length; 373 374 int new_cell_num = cellstart.size() + 1; 375 376 SplitState ss = aq->triggerSplit(cell, new_cell_num, new_first_cell_length, new_second_cell_length); 377 378 if(ss.hasFailed()) 379 return ss; 380 381 cellsize[cell] = new_first_cell_length; 382 cellstart.push_back(pos); 383 cellsize.push_back(new_second_cell_length); 384 markstore.add_cell_marker(cellCount(), pos, new_second_cell_length); 385 386 if(cellsize[cell] == 1) 387 { 388 fixed.push_back(cell); 389 fixed_vals.push_back(*cellStartPtr(cell)); 390 } 391 392 if(cellsize[new_cell_num] == 1) 393 { 394 fixed.push_back(new_cell_num); 395 fixed_vals.push_back(*cellStartPtr(new_cell_num)); 396 } 397 398 backtrack_stack.push_back(PartitionSplit(cell, pos)); 399 D_SLOW_ASSERT(sanity_check()); 400 return ss; 401 } 402 event_pushWorld()403 void event_pushWorld() 404 { 405 backtrack_depths.push_back(backtrack_stack.size()); 406 } 407 event_popWorld()408 void event_popWorld() 409 { 410 int depth = backtrack_depths.back(); 411 backtrack_depths.pop_back(); 412 while(backtrack_stack.size() > depth) 413 { 414 PartitionSplit ps = backtrack_stack.back(); 415 backtrack_stack.pop_back(); 416 417 if(cellSize(cellCount()) == 1) 418 { 419 D_ASSERT(fixed.back() == cellCount()); 420 fixed.pop_back(); 421 fixed_vals.pop_back(); 422 } 423 424 if(cellSize(ps.cell) == 1) 425 { 426 D_ASSERT(fixed.back() == ps.cell); 427 fixed.pop_back(); 428 fixed_vals.pop_back(); 429 } 430 431 D_ASSERT(markstore.marks(ps.splitpos) == cellCount()); 432 markstore.remove_cell_marker(ps.cell, ps.splitpos, cellsize[cellCount()]); 433 D_ASSERT(cellStartPos(cellCount()) == ps.splitpos); 434 cellsize[ps.cell] += cellsize[cellCount()]; 435 cellstart.pop_back(); 436 cellsize.pop_back(); 437 D_SLOW_ASSERT(sanity_check()); 438 } 439 } 440 swapPositions(int pos1,int pos2)441 void swapPositions(int pos1, int pos2) 442 { 443 D_ASSERT(cellOfPos(pos1) == cellOfPos(pos2)); 444 int temp = vals[pos1]; 445 vals[pos1] = vals[pos2]; 446 vals[pos2] = temp; 447 invvals[vals[pos1]] = pos1; 448 invvals[vals[pos2]] = pos2; 449 } 450 451 /// Fix the inverses of a cell fixCellInverses(int cell)452 void fixCellInverses(int cell) 453 { 454 int start = cellStartPos(cell); 455 int end = cellEndPos(cell); 456 for(int i = start; i < end; ++i) 457 { 458 invvals[vals[i]] = i; 459 } 460 } 461 462 dumpCurrentPartition()463 vec1<vec1<int> > dumpCurrentPartition() 464 { 465 vec1<vec1<int> > partition; 466 for(int i : range1(cellCount())) 467 { 468 vec1<int> v; 469 for(cellit it = cellStartPtr(i); it != cellEndPtr(i); ++it) 470 v.push_back(*it); 471 std::sort(v.begin(), v.end()); 472 partition.push_back(v); 473 } 474 return partition; 475 } 476 printCurrentPartition()477 std::string printCurrentPartition() 478 { 479 vec1<vec1<int> > v = dumpCurrentPartition(); 480 std::ostringstream oss; 481 oss << "[" << markstore.marks(1) << ": "; 482 for(int i : range1(n)) 483 { 484 oss << vals[i]; 485 if(markstore.marks(i+1) > 0) 486 oss << "|" << markstore.marks(i+1) << ": "; 487 else 488 oss << " "; 489 } 490 oss << "]"; 491 return oss.str(); 492 } 493 }; 494 495 496 #endif 497