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