this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Linnea Ingmar <linnea.ingmar@hotmail.com>
5 * Christian Schulte <schulte@gecode.org>
6 *
7 * Copyright:
8 * Linnea Ingmar, 2017
9 * Christian Schulte, 2017
10 *
11 * This file is part of Gecode, the generic constraint
12 * development environment:
13 * http://www.gecode.org
14 *
15 * Permission is hereby granted, free of charge, to any person obtaining
16 * a copy of this software and associated documentation files (the
17 * "Software"), to deal in the Software without restriction, including
18 * without limitation the rights to use, copy, modify, merge, publish,
19 * distribute, sublicense, and/or sell copies of the Software, and to
20 * permit persons to whom the Software is furnished to do so, subject to
21 * the following conditions:
22 *
23 * The above copyright notice and this permission notice shall be
24 * included in all copies or substantial portions of the Software.
25 *
26 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
27 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
28 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
29 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
30 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
31 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
32 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
33 *
34 */
35
36#include <algorithm>
37#include <type_traits>
38
39namespace Gecode { namespace Int { namespace Extensional {
40
41 /*
42 * Advisor
43 *
44 */
45 template<class View, bool pos>
46 forceinline void
47 Compact<View,pos>::CTAdvisor::adjust(void) {
48 if (pos) {
49 {
50 int n = view().min();
51 assert((_fst->min <= n) && (n <= _lst->max));
52 while (n > _fst->max)
53 _fst++;
54 assert((_fst->min <= n) && (n <= _lst->max));
55 }
56 {
57 int n = view().max();
58 assert((_fst->min <= n) && (n <= _lst->max));
59 while (n < _lst->min)
60 _lst--;
61 assert((_fst->min <= n) && (n <= _lst->max));
62 }
63 } else {
64 {
65 int n = view().min();
66 while ((_fst <= _lst) && (n > _fst->max))
67 _fst++;
68 }
69 {
70 int n = view().max();
71 while ((_fst <= _lst) && (n < _lst->min))
72 _lst--;
73 }
74 }
75 }
76
77 template<class View, bool pos>
78 forceinline
79 Compact<View,pos>::CTAdvisor::CTAdvisor
80 (Space& home, Propagator& p,
81 Council<CTAdvisor>& c, const TupleSet& ts, View x0, int i)
82 : ViewAdvisor<View>(home,p,c,x0), _fst(ts.fst(i)), _lst(ts.lst(i)) {
83 adjust();
84 }
85
86 template<class View, bool pos>
87 forceinline
88 Compact<View,pos>::CTAdvisor::CTAdvisor(Space& home, CTAdvisor& a)
89 : ViewAdvisor<View>(home,a), _fst(a._fst), _lst(a._lst) {}
90
91 template<class View, bool pos>
92 forceinline const typename Compact<View,pos>::Range*
93 Compact<View,pos>::CTAdvisor::fst(void) const {
94 return _fst;
95 }
96
97 template<class View, bool pos>
98 forceinline const typename Compact<View,pos>::Range*
99 Compact<View,pos>::CTAdvisor::lst(void) const {
100 return _lst;
101 }
102
103 template<class View, bool pos>
104 forceinline void
105 Compact<View,pos>::CTAdvisor::dispose(Space& home, Council<CTAdvisor>& c) {
106 (void) ViewAdvisor<View>::dispose(home,c);
107 }
108
109
110 /*
111 * The propagator base class
112 *
113 */
114 template<class View, bool pos>
115 const typename Compact<View,pos>::Range*
116 Compact<View,pos>::range(CTAdvisor& a, int n) {
117 assert((n > a.fst()->max) && (n < a.lst()->min));
118
119 const Range* f=a.fst()+1;
120 const Range* l=a.lst()-1;
121
122 assert(!pos || (f<=l));
123
124 while (f < l) {
125 const Range* m = f + ((l-f) >> 1);
126 if (n < m->min) {
127 l=m-1;
128 } else if (n > m->max) {
129 f=m+1;
130 } else {
131 f=m; break;
132 }
133 }
134
135 if (pos) {
136 assert((f->min <= n) && (n <= f->max));
137 return f;
138 } else {
139 if ((f <= l) && (f->min <= n) && (n <= f->max))
140 return f;
141 else
142 return nullptr;
143 }
144 }
145
146 template<class View, bool pos>
147 forceinline const BitSetData*
148 Compact<View,pos>::supports(CTAdvisor& a, int n) {
149 const Range* fnd;
150 const Range* fst=a.fst();
151 const Range* lst=a.lst();
152 if (pos) {
153 if (n <= fst->max) {
154 fnd=fst;
155 } else if (n >= lst->min) {
156 fnd=lst;
157 } else {
158 fnd=range(a,n);
159 }
160 } else {
161 if ((n < fst->min) || (n > lst->max))
162 return nullptr;
163 if (n <= fst->max) {
164 fnd=fst;
165 } else if (n >= lst->min) {
166 fnd=lst;
167 } else {
168 fnd=range(a,n);
169 if (!fnd)
170 return nullptr;
171 }
172 }
173 assert((fnd->min <= n) && (n <= fnd->max));
174 return fnd->supports(n_words,n);
175 }
176
177 template<class View, bool pos>
178 forceinline void
179 Compact<View,pos>::ValidSupports::find(void) {
180 assert(!pos);
181 assert(n <= max);
182 while (true) {
183 while (xr() && (n > xr.max()))
184 ++xr;
185 if (!xr()) {
186 n = max+1; return;
187 }
188 assert(n <= xr.max());
189 n = std::max(n,xr.min());
190
191 while ((sr <= lst) && (n > sr->max))
192 sr++;
193 if (sr > lst) {
194 n = max+1; return;
195 }
196 assert(n <= sr->max);
197 n = std::max(n,sr->min);
198
199 if ((xr.min() <= n) && (n <= xr.max())) {
200 s = sr->supports(n_words,n);
201 return;
202 }
203 }
204 GECODE_NEVER;
205 }
206
207 template<class View, bool pos>
208 forceinline
209 Compact<View,pos>::ValidSupports::ValidSupports(const Compact<View,pos>& p,
210 CTAdvisor& a)
211 : n_words(p.n_words), max(a.view().max()),
212 xr(a.view()), sr(a.fst()), lst(a.lst()), n(xr.min()) {
213 if (pos) {
214 while (n > sr->max)
215 sr++;
216 s = sr->supports(n_words,n);
217 } else {
218 s = nullptr; // To avoid warnings
219 find();
220 }
221 }
222 template<class View, bool pos>
223 forceinline
224 Compact<View,pos>::ValidSupports::ValidSupports(const TupleSet& ts,
225 int i, View x)
226 : n_words(ts.words()), max(x.max()),
227 xr(x), sr(ts.fst(i)), lst(ts.lst(i)), n(xr.min()) {
228 if (pos) {
229 while (n > sr->max)
230 sr++;
231 s = sr->supports(n_words,n);
232 } else {
233 s = nullptr; // To avoid warnings
234 find();
235 }
236 }
237 template<class View, bool pos>
238 forceinline void
239 Compact<View,pos>::ValidSupports::operator ++(void) {
240 n++;
241 if (pos) {
242 if (n <= xr.max()) {
243 assert(n <= sr->max);
244 s += n_words;
245 } else if (n <= max) {
246 while (n > xr.max())
247 ++xr;
248 n = xr.min();
249 while (n > sr->max)
250 sr++;
251 s = sr->supports(n_words,n);
252 assert((xr.min() <= n) && (n <= xr.max()));
253 assert((sr->min <= n) && (n <= sr->max));
254 assert(sr->min <= xr.min());
255 }
256 } else {
257 if ((n <= sr->max) && (n <= xr.max())) {
258 s += n_words;
259 } else if (n <= max) {
260 find();
261 }
262 }
263 }
264 template<class View, bool pos>
265 forceinline bool
266 Compact<View,pos>::ValidSupports::operator ()(void) const {
267 return n <= max;
268 }
269 template<class View, bool pos>
270 forceinline const BitSetData*
271 Compact<View,pos>::ValidSupports::supports(void) const {
272 assert(s == sr->supports(n_words,n));
273 return s;
274 }
275 template<class View, bool pos>
276 forceinline int
277 Compact<View,pos>::ValidSupports::val(void) const {
278 return n;
279 }
280
281 /*
282 * Lost supports iterator
283 *
284 */
285 template<class View, bool pos>
286 forceinline
287 Compact<View,pos>::LostSupports::LostSupports
288 (const Compact<View,pos>& p, CTAdvisor& a, int l0, int h0)
289 : n_words(p.n_words), r(a.fst()), l(l0), h(h0) {
290 assert(pos);
291 // Move to first value for which there is support
292 while (l > r->max)
293 r++;
294 l = std::max(l,r->min);
295 s = r->supports(n_words,l);
296 }
297 template<class View, bool pos>
298 forceinline void
299 Compact<View,pos>::LostSupports::operator ++(void) {
300 l++; s += n_words;
301 while ((l <= h) && (l > r->max)) {
302 r++; l=r->min; s=r->s;
303 }
304 }
305 template<class View, bool pos>
306 forceinline bool
307 Compact<View,pos>::LostSupports::operator ()(void) const {
308 return l<=h;
309 }
310 template<class View, bool pos>
311 forceinline const TupleSet::BitSetData*
312 Compact<View,pos>::LostSupports::supports(void) const {
313 assert((l >= r->min) && (l <= r->max));
314 assert(s == r->supports(n_words,l));
315 return s;
316 }
317
318 template<class View, bool pos>
319 forceinline bool
320 Compact<View,pos>::all(void) const {
321 Advisors<CTAdvisor> as(c);
322 return !as();
323 }
324 template<class View, bool pos>
325 forceinline bool
326 Compact<View,pos>::atmostone(void) const {
327 Advisors<CTAdvisor> as(c);
328 if (!as()) return true;
329 ++as;
330 return !as();
331 }
332
333 template<class View, bool pos>
334 forceinline
335 Compact<View,pos>::Compact(Space& home, Compact& p)
336 : Propagator(home,p), n_words(p.n_words), ts(p.ts) {
337 c.update(home,p.c);
338 }
339
340 template<class View, bool pos>
341 forceinline
342 Compact<View,pos>::Compact(Home home, const TupleSet& ts0)
343 : Propagator(home), n_words(ts0.words()), ts(ts0), c(home) {
344 home.notice(*this, AP_DISPOSE);
345 }
346
347 template<class View, bool pos>
348 template<class Table>
349 void
350 Compact<View,pos>::setup(Space& home, Table& table, ViewArray<View>& x) {
351 // For scheduling the propagator
352 ModEvent me = ME_INT_BND;
353 Region r;
354 BitSetData* mask = r.alloc<BitSetData>(table.size());
355 // Invalidate tuples
356 for (int i=0; i<x.size(); i++) {
357 table.clear_mask(mask);
358 for (ValidSupports vs(ts,i,x[i]); vs(); ++vs)
359 table.add_to_mask(vs.supports(),mask);
360 table.template intersect_with_mask<false>(mask);
361 // The propagator must be scheduled for subsumption
362 if (table.empty())
363 goto schedule;
364 }
365 // Post advisors
366 for (int i=0; i<x.size(); i++)
367 if (!x[i].assigned())
368 (void) new (home) CTAdvisor(home,*this,c,ts,x[i],i);
369 else
370 me = ME_INT_VAL;
371 // Schedule propagator
372 schedule:
373 View::schedule(home,*this,me);
374 }
375
376 template<class View, bool pos>
377 template<class Table>
378 forceinline bool
379 Compact<View,pos>::full(const Table& table) const {
380 unsigned long long int s = 1U;
381 for (Advisors<CTAdvisor> as(c); as(); ++as) {
382 s *= static_cast<unsigned long long int>(as.advisor().view().size());
383 if (s > table.bits())
384 return false;
385 }
386 return s == table.ones();
387 }
388
389 template<class View, bool pos>
390 PropCost
391 Compact<View,pos>::cost(const Space&, const ModEventDelta&) const {
392 // Computing this is crucial in case there are many propagators!
393 int n = 0;
394 // The value of 3 is cheating from the Gecode kernel...
395 for (Advisors<CTAdvisor> as(c); as() && (n <= 3); ++as)
396 n++;
397 return PropCost::quadratic(PropCost::HI,n);
398 }
399
400 template<class View, bool pos>
401 forceinline size_t
402 Compact<View,pos>::dispose(Space& home) {
403 home.ignore(*this,AP_DISPOSE);
404 c.dispose(home);
405 ts.~TupleSet();
406 (void) Propagator::dispose(home);
407 return sizeof(*this);
408 }
409
410
411 /*
412 * Status for the positive propagator
413 *
414 */
415 template<class View, class Table>
416 forceinline
417 PosCompact<View,Table>::Status::Status(StatusType t)
418 : s(t) {}
419 template<class View, class Table>
420 forceinline
421 PosCompact<View,Table>::Status::Status(const Status& s)
422 : s(s.s) {}
423 template<class View, class Table>
424 forceinline typename PosCompact<View,Table>::StatusType
425 PosCompact<View,Table>::Status::type(void) const {
426 return static_cast<StatusType>(s & 3);
427 }
428 template<class View, class Table>
429 forceinline bool
430 PosCompact<View,Table>::Status::single(CTAdvisor& a) const {
431 if (type() != SINGLE)
432 return false;
433 assert(type() == 0);
434 return reinterpret_cast<CTAdvisor*>(s) == &a;
435 }
436 template<class View, class Table>
437 forceinline void
438 PosCompact<View,Table>::Status::touched(CTAdvisor& a) {
439 if (!single(a))
440 s = MULTIPLE;
441 }
442 template<class View, class Table>
443 forceinline void
444 PosCompact<View,Table>::Status::none(void) {
445 s = NONE;
446 }
447 template<class View, class Table>
448 forceinline void
449 PosCompact<View,Table>::Status::propagating(void) {
450 s = PROPAGATING;
451 }
452
453 /*
454 * The propagator proper
455 *
456 */
457 template<class View, class Table>
458 template<class TableProp>
459 forceinline
460 PosCompact<View,Table>::PosCompact(Space& home, TableProp& p)
461 : Compact<View,true>(home,p), status(NONE), table(home,p.table) {
462 assert(!table.empty());
463 }
464
465 template<class View, class Table>
466 Actor*
467 PosCompact<View,Table>::copy(Space& home) {
468 assert((table.words() > 0U) && (table.width() >= table.words()));
469 if (table.words() <= 4U) {
470 switch (table.width()) {
471 case 0U:
472 GECODE_NEVER; break;
473 case 1U:
474 return new (home) PosCompact<View,TinyBitSet<1U>>(home,*this);
475 case 2U:
476 return new (home) PosCompact<View,TinyBitSet<2U>>(home,*this);
477 case 3U:
478 return new (home) PosCompact<View,TinyBitSet<3U>>(home,*this);
479 case 4U:
480 return new (home) PosCompact<View,TinyBitSet<4U>>(home,*this);
481 default:
482 break;
483 }
484 }
485 if (std::is_same<Table,BitSet<unsigned char>>::value) {
486 goto copy_char;
487 } else if (std::is_same<Table,BitSet<unsigned short int>>::value) {
488 switch (Gecode::Support::u_type(table.width())) {
489 case Gecode::Support::IT_CHAR: goto copy_char;
490 case Gecode::Support::IT_SHRT: goto copy_short;
491 case Gecode::Support::IT_INT: GECODE_NEVER;
492 default: GECODE_NEVER;
493 }
494 } else {
495 switch (Gecode::Support::u_type(table.width())) {
496 case Gecode::Support::IT_CHAR: goto copy_char;
497 case Gecode::Support::IT_SHRT: goto copy_short;
498 case Gecode::Support::IT_INT: goto copy_int;
499 default: GECODE_NEVER;
500 }
501 GECODE_NEVER;
502 return nullptr;
503 }
504 copy_char:
505 return new (home) PosCompact<View,BitSet<unsigned char>>(home,*this);
506 copy_short:
507 return new (home) PosCompact<View,BitSet<unsigned short int>>(home,*this);
508 copy_int:
509 return new (home) PosCompact<View,BitSet<unsigned int>>(home,*this);
510 }
511
512 template<class View, class Table>
513 forceinline
514 PosCompact<View,Table>::PosCompact(Home home, ViewArray<View>& x,
515 const TupleSet& ts)
516 : Compact<View,true>(home,ts), status(MULTIPLE), table(home,ts.words()) {
517 setup(home,table,x);
518 }
519
520 template<class View, class Table>
521 forceinline ExecStatus
522 PosCompact<View,Table>::post(Home home, ViewArray<View>& x,
523 const TupleSet& ts) {
524 auto ct = new (home) PosCompact(home,x,ts);
525 assert((x.size() > 1) && (ts.tuples() > 1));
526 return ct->table.empty() ? ES_FAILED : ES_OK;
527 }
528
529 template<class View, class Table>
530 forceinline size_t
531 PosCompact<View,Table>::dispose(Space& home) {
532 (void) Compact<View,true>::dispose(home);
533 return sizeof(*this);
534 }
535
536 template<class View, class Table>
537 void
538 PosCompact<View,Table>::reschedule(Space& home) {
539 // Modified variable, subsumption, or failure
540 if ((status.type() != StatusType::NONE) ||
541 all() || table.empty())
542 View::schedule(home,*this,ME_INT_DOM);
543 }
544
545 template<class View, class Table>
546 ExecStatus
547 PosCompact<View,Table>::propagate(Space& home, const ModEventDelta&) {
548 if (table.empty())
549 return ES_FAILED;
550 if (all())
551 return home.ES_SUBSUMED(*this);
552
553 Status touched(status);
554 // Mark as performing propagation
555 status.propagating();
556
557 Region r;
558 // Scan all values of all unassigned variables to see if they
559 // are still supported.
560 for (Advisors<CTAdvisor> as(c); as(); ++as) {
561 CTAdvisor& a = as.advisor();
562 View x = a.view();
563
564 // No point filtering variable if it was the only modified variable
565 if (touched.single(a) || x.assigned())
566 continue;
567
568 if (x.size() == 2) { // Consider min and max values only
569 if (!table.intersects(supports(a,x.min())))
570 GECODE_ME_CHECK(x.eq(home,x.max()));
571 else if (!table.intersects(supports(a,x.max())))
572 GECODE_ME_CHECK(x.eq(home,x.min()));
573 if (!x.assigned())
574 a.adjust();
575 } else { // x.size() > 2
576 // How many values to remove
577 int* nq = r.alloc<int>(x.size());
578 unsigned int n_nq = 0;
579 // The initialization is here just to avoid warnings...
580 int last_support = 0;
581 for (ValidSupports vs(*this,a); vs(); ++vs)
582 if (!table.intersects(vs.supports()))
583 nq[n_nq++] = vs.val();
584 else
585 last_support = vs.val();
586 // Remove collected values
587 if (n_nq > 0U) {
588 if (n_nq == 1U) {
589 GECODE_ME_CHECK(x.nq(home,nq[0]));
590 } else if (n_nq == x.size() - 1U) {
591 GECODE_ME_CHECK(x.eq(home,last_support));
592 goto noadjust;
593 } else {
594 Iter::Values::Array rnq(nq,n_nq);
595 GECODE_ASSUME(n_nq >= 2U);
596 GECODE_ME_CHECK(x.minus_v(home,rnq,false));
597 }
598 a.adjust();
599 noadjust: ;
600 }
601 r.free();
602 }
603 }
604
605 // Mark as no touched variable
606 status.none();
607 // Should not be in a failed state
608 assert(!table.empty());
609 // Subsume if there is at most one non-assigned variable
610 return atmostone() ? home.ES_SUBSUMED(*this) : ES_FIX;
611 }
612
613 template<class View, class Table>
614 ExecStatus
615 PosCompact<View,Table>::advise(Space& home, Advisor& a0, const Delta& d) {
616 CTAdvisor& a = static_cast<CTAdvisor&>(a0);
617
618 // Do not fail a disabled propagator
619 if (table.empty())
620 return Compact<View,true>::disabled() ?
621 home.ES_NOFIX_DISPOSE(c,a) : ES_FAILED;
622
623 View x = a.view();
624
625 /*
626 * Do not schedule if propagator is performing propagation,
627 * and dispose if assigned.
628 */
629 if (status.type() == StatusType::PROPAGATING)
630 return x.assigned() ? home.ES_FIX_DISPOSE(c,a) : ES_FIX;
631
632 // Update status
633 status.touched(a);
634
635 if (x.assigned()) {
636 // Variable is assigned -- intersect with its value
637 table.template intersect_with_mask<true>(supports(a,x.val()));
638 return home.ES_NOFIX_DISPOSE(c,a);
639 }
640
641 if (!x.any(d) && (x.min(d) == x.max(d))) {
642 table.nand_with_mask(supports(a,x.min(d)));
643 a.adjust();
644 } else if (!x.any(d) && (x.width(d) <= x.size())) {
645 // Incremental update, using the removed values
646 for (LostSupports ls(*this,a,x.min(d),x.max(d)); ls(); ++ls) {
647 table.nand_with_mask(ls.supports());
648 if (table.empty())
649 return Compact<View,true>::disabled() ?
650 home.ES_NOFIX_DISPOSE(c,a) : ES_FAILED;
651 }
652 a.adjust();
653 } else {
654 a.adjust();
655 // Reset-based update, using the values that are left
656 if (x.size() == 2) {
657 table.intersect_with_masks(supports(a,x.min()),
658 supports(a,x.max()));
659 } else {
660 Region r;
661 BitSetData* mask = r.alloc<BitSetData>(table.size());
662 // Collect all tuples to be kept in a temporary mask
663 table.clear_mask(mask);
664 for (ValidSupports vs(*this,a); vs(); ++vs)
665 table.add_to_mask(vs.supports(),mask);
666 table.template intersect_with_mask<false>(mask);
667 }
668 }
669
670 // Do not fail a disabled propagator
671 if (table.empty())
672 return Compact<View,true>::disabled() ?
673 home.ES_NOFIX_DISPOSE(c,a) : ES_FAILED;
674
675 // Schedule propagator
676 return ES_NOFIX;
677 }
678
679
680 /*
681 * Post function
682 */
683 template<class View>
684 ExecStatus
685 postposcompact(Home home, ViewArray<View>& x, const TupleSet& ts) {
686 if (ts.tuples() == 0)
687 return (x.size() == 0) ? ES_OK : ES_FAILED;
688
689 // All variables pruned to correct domain
690 for (int i=0; i<x.size(); i++) {
691 TupleSet::Ranges r(ts,i);
692 GECODE_ME_CHECK(x[i].inter_r(home, r, false));
693 }
694
695 if ((x.size() <= 1) || (ts.tuples() <= 1))
696 return ES_OK;
697
698 // Choose the right bit set implementation
699 switch (ts.words()) {
700 case 0U:
701 GECODE_NEVER; return ES_OK;
702 case 1U:
703 return PosCompact<View,TinyBitSet<1U>>::post(home,x,ts);
704 case 2U:
705 return PosCompact<View,TinyBitSet<2U>>::post(home,x,ts);
706 case 3U:
707 return PosCompact<View,TinyBitSet<3U>>::post(home,x,ts);
708 case 4U:
709 return PosCompact<View,TinyBitSet<4U>>::post(home,x,ts);
710 default:
711 switch (Gecode::Support::u_type(ts.words())) {
712 case Gecode::Support::IT_CHAR:
713 return PosCompact<View,BitSet<unsigned char>>
714 ::post(home,x,ts);
715 case Gecode::Support::IT_SHRT:
716 return PosCompact<View,BitSet<unsigned short int>>
717 ::post(home,x,ts);
718 case Gecode::Support::IT_INT:
719 return PosCompact<View,BitSet<unsigned int>>
720 ::post(home,x,ts);
721 default: GECODE_NEVER;
722 }
723 }
724 GECODE_NEVER;
725 return ES_OK;
726 }
727
728
729 /*
730 * The negative propagator
731 *
732 */
733 template<class View, class Table>
734 template<class TableProp>
735 forceinline
736 NegCompact<View,Table>::NegCompact(Space& home, TableProp& p)
737 : Compact<View,false>(home,p), table(home,p.table) {
738 assert(!table.empty());
739 }
740
741 template<class View, class Table>
742 Actor*
743 NegCompact<View,Table>::copy(Space& home) {
744 assert((table.words() > 0U) && (table.width() >= table.words()));
745 if (table.words() <= 4U) {
746 switch (table.width()) {
747 case 0U:
748 GECODE_NEVER; break;
749 case 1U:
750 return new (home) NegCompact<View,TinyBitSet<1U>>(home,*this);
751 case 2U:
752 return new (home) NegCompact<View,TinyBitSet<2U>>(home,*this);
753 case 3U:
754 return new (home) NegCompact<View,TinyBitSet<3U>>(home,*this);
755 case 4U:
756 return new (home) NegCompact<View,TinyBitSet<4U>>(home,*this);
757 default:
758 break;
759 }
760 }
761 if (std::is_same<Table,BitSet<unsigned char>>::value) {
762 goto copy_char;
763 } else if (std::is_same<Table,BitSet<unsigned short int>>::value) {
764 switch (Gecode::Support::u_type(table.width())) {
765 case Gecode::Support::IT_CHAR: goto copy_char;
766 case Gecode::Support::IT_SHRT: goto copy_short;
767 case Gecode::Support::IT_INT: GECODE_NEVER;
768 default: GECODE_NEVER;
769 }
770 } else {
771 switch (Gecode::Support::u_type(table.width())) {
772 case Gecode::Support::IT_CHAR: goto copy_char;
773 case Gecode::Support::IT_SHRT: goto copy_short;
774 case Gecode::Support::IT_INT: goto copy_int;
775 default: GECODE_NEVER;
776 }
777 GECODE_NEVER;
778 return nullptr;
779 }
780 copy_char:
781 return new (home) NegCompact<View,BitSet<unsigned char>>(home,*this);
782 copy_short:
783 return new (home) NegCompact<View,BitSet<unsigned short int>>(home,*this);
784 copy_int:
785 return new (home) NegCompact<View,BitSet<unsigned int>>(home,*this);
786 }
787
788 template<class View, class Table>
789 forceinline
790 NegCompact<View,Table>::NegCompact(Home home, ViewArray<View>& x,
791 const TupleSet& ts)
792 : Compact<View,false>(home,ts), table(home,ts.words()) {
793 setup(home,table,x);
794 }
795
796 template<class View, class Table>
797 forceinline ExecStatus
798 NegCompact<View,Table>::post(Home home, ViewArray<View>& x,
799 const TupleSet& ts) {
800 auto ct = new (home) NegCompact(home,x,ts);
801 return ct->full(ct->table) ? ES_FAILED : ES_OK;
802 }
803
804 template<class View, class Table>
805 forceinline size_t
806 NegCompact<View,Table>::dispose(Space& home) {
807 (void) Compact<View,false>::dispose(home);
808 return sizeof(*this);
809 }
810
811 template<class View, class Table>
812 void
813 NegCompact<View,Table>::reschedule(Space& home) {
814 View::schedule(home,*this,ME_INT_DOM);
815 }
816
817 template<class View, class Table>
818 ExecStatus
819 NegCompact<View,Table>::propagate(Space& home, const ModEventDelta&) {
820#ifndef NDEBUG
821 if (!table.empty()) {
822 // Check that all views have at least one value with support
823 for (Advisors<CTAdvisor> as(c); as(); ++as) {
824 ValidSupports vs(*this,as.advisor());
825 assert(vs());
826 }
827 }
828#endif
829
830 if (table.empty())
831 return home.ES_SUBSUMED(*this);
832
833 // Estimate whether any pruning will be possible
834 unsigned long long int x_size = 1U;
835 unsigned long long int x_max = 1U;
836 /* The size of the Cartesian product will be x_size times x_max,
837 * where x_max is the size of the largest variable domain.
838 */
839 for (Advisors<CTAdvisor> as(c); as(); ++as) {
840 unsigned long long int n = as.advisor().view().size();
841 if (n > x_max) {
842 x_size *= x_max; x_max = n;
843 } else {
844 x_size *= n;
845 }
846 if (x_size > table.bits())
847 return ES_FIX;
848 }
849 if (x_size > table.ones())
850 return ES_FIX;
851
852 {
853 // Adjust to size of the Cartesian product
854 x_size *= x_max;
855
856 Region r;
857
858 for (Advisors<CTAdvisor> as(c); as(); ++as) {
859 assert(!table.empty());
860 CTAdvisor& a = as.advisor();
861 View x = a.view();
862
863 // Adjust for the current variable domain
864 x_size /= static_cast<unsigned long long int>(x.size());
865
866 if ((x_size <= table.bits()) && (x_size <= table.ones())) {
867 // How many values to remove
868 int* nq = r.alloc<int>(x.size());
869 unsigned int n_nq = 0U;
870
871 for (ValidSupports vs(*this,a); vs(); ++vs)
872 if (x_size == table.ones(vs.supports()))
873 nq[n_nq++] = vs.val();
874
875 // Remove collected values
876 if (n_nq > 0U) {
877 if (n_nq == 1U) {
878 GECODE_ME_CHECK(x.nq(home,nq[0]));
879 } else {
880 Iter::Values::Array rnq(nq,n_nq);
881 GECODE_ASSUME(n_nq >= 2U);
882 GECODE_ME_CHECK(x.minus_v(home,rnq,false));
883 }
884 if (table.empty())
885 return home.ES_SUBSUMED(*this);
886 a.adjust();
887 }
888 r.free();
889 }
890 // Re-adjust size
891 x_size *= static_cast<unsigned long long int>(x.size());
892 }
893 }
894
895 if (table.ones() == x_size)
896 return ES_FAILED;
897 if (table.empty() || atmostone())
898 return home.ES_SUBSUMED(*this);
899 return ES_FIX;
900 }
901
902 template<class View, class Table>
903 ExecStatus
904 NegCompact<View,Table>::advise(Space& home, Advisor& a0, const Delta&) {
905 CTAdvisor& a = static_cast<CTAdvisor&>(a0);
906
907 // We are subsumed
908 if (table.empty())
909 return home.ES_NOFIX_DISPOSE(c,a);
910
911 View x = a.view();
912
913 a.adjust();
914
915 if (x.assigned()) {
916 // Variable is assigned -- intersect with its value
917 if (const BitSetData* s = supports(a,x.val()))
918 table.template intersect_with_mask<true>(s);
919 else
920 table.flush(); // Mark as subsumed
921 return home.ES_NOFIX_DISPOSE(c,a);
922 }
923
924 {
925 ValidSupports vs(*this,a);
926 if (!vs()) {
927 table.flush(); // Mark as subsumed
928 return home.ES_NOFIX_DISPOSE(c,a);
929 }
930
931 Region r;
932 BitSetData* mask = r.alloc<BitSetData>(table.size());
933 // Collect all tuples to be kept in a temporary mask
934 table.clear_mask(mask);
935 do {
936 table.add_to_mask(vs.supports(),mask);
937 ++vs;
938 } while (vs());
939 table.template intersect_with_mask<false>(mask);
940 }
941
942 if (table.empty())
943 return home.ES_NOFIX_DISPOSE(c,a);
944
945 // Schedule propagator
946 return ES_NOFIX;
947 }
948
949
950 /*
951 * Post function
952 */
953 template<class View>
954 ExecStatus
955 postnegcompact(Home home, ViewArray<View>& x, const TupleSet& ts) {
956 if (ts.tuples() == 0)
957 return ES_OK;
958
959 // Check whether a variable does not overlap with supported values
960 for (int i=0; i<x.size(); i++) {
961 TupleSet::Ranges rs(ts,i);
962 ViewRanges<View> rx(x[i]);
963 if (Iter::Ranges::disjoint(rs,rx))
964 return ES_OK;
965 }
966
967 // Choose the right bit set implementation
968 switch (ts.words()) {
969 case 0U:
970 GECODE_NEVER; return ES_OK;
971 case 1U:
972 return NegCompact<View,TinyBitSet<1U>>::post(home,x,ts);
973 case 2U:
974 return NegCompact<View,TinyBitSet<2U>>::post(home,x,ts);
975 case 3U:
976 return NegCompact<View,TinyBitSet<3U>>::post(home,x,ts);
977 case 4U:
978 return NegCompact<View,TinyBitSet<4U>>::post(home,x,ts);
979 default:
980 switch (Gecode::Support::u_type(ts.words())) {
981 case Gecode::Support::IT_CHAR:
982 return NegCompact<View,BitSet<unsigned char>>
983 ::post(home,x,ts);
984 case Gecode::Support::IT_SHRT:
985 return NegCompact<View,BitSet<unsigned short int>>
986 ::post(home,x,ts);
987 case Gecode::Support::IT_INT:
988 return NegCompact<View,BitSet<unsigned int>>
989 ::post(home,x,ts);
990 default: GECODE_NEVER;
991 }
992 }
993 GECODE_NEVER;
994 return ES_OK;
995 }
996
997
998 /*
999 * The reified propagator
1000 *
1001 */
1002 template<class View, class Table, class CtrlView, ReifyMode rm>
1003 template<class TableProp>
1004 forceinline
1005 ReCompact<View,Table,CtrlView,rm>::ReCompact(Space& home, TableProp& p)
1006 : Compact<View,false>(home,p), table(home,p.table) {
1007 b.update(home,p.b);
1008 y.update(home,p.y);
1009 assert(!table.empty());
1010 }
1011
1012 template<class View, class Table, class CtrlView, ReifyMode rm>
1013 Actor*
1014 ReCompact<View,Table,CtrlView,rm>::copy(Space& home) {
1015 assert((table.words() > 0U) && (table.width() >= table.words()));
1016 if (table.words() <= 4U) {
1017 switch (table.width()) {
1018 case 0U:
1019 GECODE_NEVER; break;
1020 case 1U:
1021 return new (home) ReCompact<View,TinyBitSet<1U>,CtrlView,rm>
1022 (home,*this);
1023 case 2U:
1024 return new (home) ReCompact<View,TinyBitSet<2U>,CtrlView,rm>
1025 (home,*this);
1026 case 3U:
1027 return new (home) ReCompact<View,TinyBitSet<3U>,CtrlView,rm>
1028 (home,*this);
1029 case 4U:
1030 return new (home) ReCompact<View,TinyBitSet<4U>,CtrlView,rm>
1031 (home,*this);
1032 default:
1033 break;
1034 }
1035 }
1036 if (std::is_same<Table,BitSet<unsigned char>>::value) {
1037 goto copy_char;
1038 } else if (std::is_same<Table,BitSet<unsigned short int>>::value) {
1039 switch (Gecode::Support::u_type(table.width())) {
1040 case Gecode::Support::IT_CHAR: goto copy_char;
1041 case Gecode::Support::IT_SHRT: goto copy_short;
1042 case Gecode::Support::IT_INT: GECODE_NEVER;
1043 default: GECODE_NEVER;
1044 }
1045 } else {
1046 switch (Gecode::Support::u_type(table.width())) {
1047 case Gecode::Support::IT_CHAR: goto copy_char;
1048 case Gecode::Support::IT_SHRT: goto copy_short;
1049 case Gecode::Support::IT_INT: goto copy_int;
1050 default: GECODE_NEVER;
1051 }
1052 GECODE_NEVER;
1053 return nullptr;
1054 }
1055 copy_char:
1056 return new (home) ReCompact<View,BitSet<unsigned char>,CtrlView,rm>
1057 (home,*this);
1058 copy_short:
1059 return new (home) ReCompact<View,BitSet<unsigned short int>,CtrlView,rm>
1060 (home,*this);
1061 copy_int:
1062 return new (home) ReCompact<View,BitSet<unsigned int>,CtrlView,rm>
1063 (home,*this);
1064 }
1065
1066 template<class View, class Table, class CtrlView, ReifyMode rm>
1067 forceinline
1068 ReCompact<View,Table,CtrlView,rm>::ReCompact(Home home, ViewArray<View>& x,
1069 const TupleSet& ts, CtrlView b0)
1070 : Compact<View,false>(home,ts), table(home,ts.words()), b(b0), y(x) {
1071 b.subscribe(home,*this,PC_BOOL_VAL);
1072 setup(home,table,x);
1073 }
1074
1075 template<class View, class Table, class CtrlView, ReifyMode rm>
1076 forceinline ExecStatus
1077 ReCompact<View,Table,CtrlView,rm>::post(Home home, ViewArray<View>& x,
1078 const TupleSet& ts, CtrlView b) {
1079 if (b.one()) {
1080 if (rm == RM_PMI)
1081 return ES_OK;
1082 return postposcompact(home,x,ts);
1083 }
1084 if (b.zero()) {
1085 if (rm == RM_IMP)
1086 return ES_OK;
1087 return postnegcompact(home,x,ts);
1088 }
1089 (void) new (home) ReCompact(home,x,ts,b);
1090 return ES_OK;
1091 }
1092
1093 template<class View, class Table, class CtrlView, ReifyMode rm>
1094 forceinline size_t
1095 ReCompact<View,Table,CtrlView,rm>::dispose(Space& home) {
1096 b.cancel(home,*this,PC_BOOL_VAL);
1097 (void) Compact<View,false>::dispose(home);
1098 return sizeof(*this);
1099 }
1100
1101 template<class View, class Table, class CtrlView, ReifyMode rm>
1102 void
1103 ReCompact<View,Table,CtrlView,rm>::reschedule(Space& home) {
1104 View::schedule(home,*this,ME_INT_DOM);
1105 }
1106
1107 template<class View, class Table, class CtrlView, ReifyMode rm>
1108 ExecStatus
1109 ReCompact<View,Table,CtrlView,rm>::propagate(Space& home,
1110 const ModEventDelta&) {
1111 if (b.one()) {
1112 if (rm == RM_PMI)
1113 return home.ES_SUBSUMED(*this);
1114 TupleSet keep(ts);
1115 GECODE_REWRITE(*this,postposcompact(home(*this),y,keep));
1116 }
1117 if (b.zero()) {
1118 if (rm == RM_IMP)
1119 return home.ES_SUBSUMED(*this);
1120 TupleSet keep(ts);
1121 GECODE_REWRITE(*this,postnegcompact(home(*this),y,keep));
1122 }
1123
1124 if (table.empty()) {
1125 if (rm != RM_PMI)
1126 GECODE_ME_CHECK(b.zero_none(home));
1127 return home.ES_SUBSUMED(*this);
1128 }
1129 if (full(table)) {
1130 if (rm != RM_IMP)
1131 GECODE_ME_CHECK(b.one_none(home));
1132 return home.ES_SUBSUMED(*this);
1133 }
1134
1135 return ES_FIX;
1136 }
1137
1138 template<class View, class Table, class CtrlView, ReifyMode rm>
1139 ExecStatus
1140 ReCompact<View,Table,CtrlView,rm>::advise(Space& home,
1141 Advisor& a0, const Delta&) {
1142 CTAdvisor& a = static_cast<CTAdvisor&>(a0);
1143
1144 // We are subsumed
1145 if (table.empty() || b.assigned())
1146 return home.ES_NOFIX_DISPOSE(c,a);
1147
1148 View x = a.view();
1149
1150 a.adjust();
1151
1152 if (x.assigned()) {
1153 // Variable is assigned -- intersect with its value
1154 if (const BitSetData* s = supports(a,x.val()))
1155 table.template intersect_with_mask<true>(s);
1156 else
1157 table.flush(); // Mark as failed
1158 return home.ES_NOFIX_DISPOSE(c,a);
1159 }
1160
1161 {
1162 ValidSupports vs(*this,a);
1163 if (!vs()) {
1164 table.flush(); // Mark as failed
1165 return home.ES_NOFIX_DISPOSE(c,a);
1166 }
1167
1168 Region r;
1169 BitSetData* mask = r.alloc<BitSetData>(table.size());
1170 // Collect all tuples to be kept in a temporary mask
1171 table.clear_mask(mask);
1172 do {
1173 table.add_to_mask(vs.supports(),mask);
1174 ++vs;
1175 } while (vs());
1176 table.template intersect_with_mask<false>(mask);
1177 }
1178
1179 if (table.empty())
1180 return home.ES_NOFIX_DISPOSE(c,a);
1181
1182 // Schedule propagator
1183 return ES_NOFIX;
1184 }
1185
1186
1187 /*
1188 * Post function
1189 */
1190 template<class View, class CtrlView, ReifyMode rm>
1191 ExecStatus
1192 postrecompact(Home home, ViewArray<View>& x, const TupleSet& ts,
1193 CtrlView b) {
1194 // Enforce invariant that there is at least one tuple...
1195 if (ts.tuples() == 0) {
1196 if (x.size() != 0) {
1197 if (rm != RM_PMI)
1198 GECODE_ME_CHECK(b.zero(home));
1199 } else {
1200 if (rm != RM_IMP)
1201 GECODE_ME_CHECK(b.one(home));
1202 }
1203 return ES_OK;
1204 }
1205 // Check whether a variable does not overlap with supported values
1206 for (int i=0; i<x.size(); i++) {
1207 TupleSet::Ranges rs(ts,i);
1208 ViewRanges<View> rx(x[i]);
1209 if (Iter::Ranges::disjoint(rs,rx)) {
1210 if (rm != RM_PMI)
1211 GECODE_ME_CHECK(b.zero(home));
1212 return ES_OK;
1213 }
1214 }
1215 // Choose the right bit set implementation
1216 switch (ts.words()) {
1217 case 0U:
1218 GECODE_NEVER; return ES_OK;
1219 case 1U:
1220 return ReCompact<View,TinyBitSet<1U>,CtrlView,rm>::post(home,x,ts,b);
1221 case 2U:
1222 return ReCompact<View,TinyBitSet<2U>,CtrlView,rm>::post(home,x,ts,b);
1223 case 3U:
1224 return ReCompact<View,TinyBitSet<3U>,CtrlView,rm>::post(home,x,ts,b);
1225 case 4U:
1226 return ReCompact<View,TinyBitSet<4U>,CtrlView,rm>::post(home,x,ts,b);
1227 default:
1228 switch (Gecode::Support::u_type(ts.words())) {
1229 case Gecode::Support::IT_CHAR:
1230 return ReCompact<View,BitSet<unsigned char>,CtrlView,rm>
1231 ::post(home,x,ts,b);
1232 case Gecode::Support::IT_SHRT:
1233 return ReCompact<View,BitSet<unsigned short int>,CtrlView,rm>
1234 ::post(home,x,ts,b);
1235 case Gecode::Support::IT_INT:
1236 return ReCompact<View,BitSet<unsigned int>,CtrlView,rm>
1237 ::post(home,x,ts,b);
1238 default: GECODE_NEVER;
1239 }
1240 }
1241 GECODE_NEVER;
1242 return ES_OK;
1243 }
1244
1245}}}
1246
1247// STATISTICS: int-prop