this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Christian Schulte <schulte@gecode.org>
5 *
6 * Copyright:
7 * Christian Schulte, 2004
8 *
9 * This file is part of Gecode, the generic constraint
10 * development environment:
11 * http://www.gecode.org
12 *
13 * Permission is hereby granted, free of charge, to any person obtaining
14 * a copy of this software and associated documentation files (the
15 * "Software"), to deal in the Software without restriction, including
16 * without limitation the rights to use, copy, modify, merge, publish,
17 * distribute, sublicense, and/or sell copies of the Software, and to
18 * permit persons to whom the Software is furnished to do so, subject to
19 * the following conditions:
20 *
21 * The above copyright notice and this permission notice shall be
22 * included in all copies or substantial portions of the Software.
23 *
24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31 *
32 */
33
34#include <climits>
35#include <algorithm>
36
37namespace Gecode { namespace Int { namespace Extensional {
38
39 /**
40 * \brief Traits class for variables
41 *
42 * Each variable must specialize this traits class and add a \code
43 * typedef \endcode for the view \a View corresponding to this variable.
44 */
45 template<class Var>
46 class VarTraits {};
47
48 /**
49 * \brief Traits class for variables
50 *
51 * This class specializes the VarTraits for integer variables.
52 */
53 template<>
54 class VarTraits<IntVar> {
55 public:
56 /// The variable type of an IntView
57 typedef Int::IntView View;
58 };
59
60 /**
61 * \brief Traits class for variables
62 *
63 * This class specializes the VarTraits for Boolean variables.
64 */
65 template<>
66 class VarTraits<BoolVar> {
67 public:
68 /// The variable type of an IntView
69 typedef Int::BoolView View;
70 };
71
72
73 /*
74 * States
75 */
76 template<class View, class Val, class Degree, class StateIdx>
77 forceinline void
78 LayeredGraph<View,Val,Degree,StateIdx>::State::init(void) {
79 i_deg=o_deg=0;
80 }
81
82
83 template<class View, class Val, class Degree, class StateIdx>
84 forceinline typename LayeredGraph<View,Val,Degree,StateIdx>::State&
85 LayeredGraph<View,Val,Degree,StateIdx>::i_state(int i, StateIdx is) {
86 return layers[i].states[is];
87 }
88 template<class View, class Val, class Degree, class StateIdx>
89 forceinline typename LayeredGraph<View,Val,Degree,StateIdx>::State&
90 LayeredGraph<View,Val,Degree,StateIdx>::i_state
91 (int i, const typename LayeredGraph<View,Val,Degree,StateIdx>::Edge& e) {
92 return i_state(i,e.i_state);
93 }
94 template<class View, class Val, class Degree, class StateIdx>
95 forceinline bool
96 LayeredGraph<View,Val,Degree,StateIdx>::i_dec
97 (int i, const typename LayeredGraph<View,Val,Degree,StateIdx>::Edge& e) {
98 return --i_state(i,e).o_deg == 0;
99 }
100 template<class View, class Val, class Degree, class StateIdx>
101 forceinline typename LayeredGraph<View,Val,Degree,StateIdx>::State&
102 LayeredGraph<View,Val,Degree,StateIdx>::o_state(int i, StateIdx os) {
103 return layers[i+1].states[os];
104 }
105 template<class View, class Val, class Degree, class StateIdx>
106 forceinline typename LayeredGraph<View,Val,Degree,StateIdx>::State&
107 LayeredGraph<View,Val,Degree,StateIdx>::o_state
108 (int i, const typename LayeredGraph<View,Val,Degree,StateIdx>::Edge& e) {
109 return o_state(i,e.o_state);
110 }
111 template<class View, class Val, class Degree, class StateIdx>
112 forceinline bool
113 LayeredGraph<View,Val,Degree,StateIdx>::o_dec
114 (int i, const typename LayeredGraph<View,Val,Degree,StateIdx>::Edge& e) {
115 return --o_state(i,e).i_deg == 0;
116 }
117
118
119 /*
120 * Value iterator
121 */
122 template<class View, class Val, class Degree, class StateIdx>
123 forceinline
124 LayeredGraph<View,Val,Degree,StateIdx>::LayerValues::LayerValues(void) {}
125 template<class View, class Val, class Degree, class StateIdx>
126 forceinline
127 LayeredGraph<View,Val,Degree,StateIdx>::LayerValues
128 ::LayerValues(const Layer& l)
129 : s1(l.support), s2(l.support+l.size) {}
130 template<class View, class Val, class Degree, class StateIdx>
131 forceinline void
132 LayeredGraph<View,Val,Degree,StateIdx>::LayerValues::init(const Layer& l) {
133 s1=l.support; s2=l.support+l.size;
134 }
135 template<class View, class Val, class Degree, class StateIdx>
136 forceinline bool
137 LayeredGraph<View,Val,Degree,StateIdx>::LayerValues
138 ::operator ()(void) const {
139 return s1<s2;
140 }
141 template<class View, class Val, class Degree, class StateIdx>
142 forceinline void
143 LayeredGraph<View,Val,Degree,StateIdx>::LayerValues::operator ++(void) {
144 s1++;
145 }
146 template<class View, class Val, class Degree, class StateIdx>
147 forceinline int
148 LayeredGraph<View,Val,Degree,StateIdx>::LayerValues::val(void) const {
149 return s1->val;
150 }
151
152
153 /*
154 * Index advisors
155 *
156 */
157 template<class View, class Val, class Degree, class StateIdx>
158 forceinline
159 LayeredGraph<View,Val,Degree,StateIdx>::Index::Index(Space& home, Propagator& p,
160 Council<Index>& c,
161 int i0)
162 : Advisor(home,p,c), i(i0) {}
163
164 template<class View, class Val, class Degree, class StateIdx>
165 forceinline
166 LayeredGraph<View,Val,Degree,StateIdx>::Index::Index(Space& home, Index& a)
167 : Advisor(home,a), i(a.i) {}
168
169
170 /*
171 * Index ranges
172 *
173 */
174 template<class View, class Val, class Degree, class StateIdx>
175 forceinline
176 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::IndexRange(void)
177 : _fst(INT_MAX), _lst(INT_MIN) {}
178 template<class View, class Val, class Degree, class StateIdx>
179 forceinline void
180 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::reset(void) {
181 _fst=INT_MAX; _lst=INT_MIN;
182 }
183 template<class View, class Val, class Degree, class StateIdx>
184 forceinline void
185 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::add(int i) {
186 _fst=std::min(_fst,i); _lst=std::max(_lst,i);
187 }
188 template<class View, class Val, class Degree, class StateIdx>
189 forceinline void
190 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::add
191 (const typename LayeredGraph<View,Val,Degree,StateIdx>::IndexRange& ir) {
192 _fst=std::min(_fst,ir._fst); _lst=std::max(_lst,ir._lst);
193 }
194 template<class View, class Val, class Degree, class StateIdx>
195 forceinline bool
196 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::empty(void) const {
197 return _fst>_lst;
198 }
199 template<class View, class Val, class Degree, class StateIdx>
200 forceinline void
201 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::lshift(int n) {
202 if (empty())
203 return;
204 if (n > _lst) {
205 reset();
206 } else {
207 _fst = std::max(0,_fst-n);
208 _lst -= n;
209 }
210 }
211 template<class View, class Val, class Degree, class StateIdx>
212 forceinline int
213 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::fst(void) const {
214 return _fst;
215 }
216 template<class View, class Val, class Degree, class StateIdx>
217 forceinline int
218 LayeredGraph<View,Val,Degree,StateIdx>::IndexRange::lst(void) const {
219 return _lst;
220 }
221
222
223
224 /*
225 * The layered graph
226 *
227 */
228
229 template<class View, class Val, class Degree, class StateIdx>
230 template<class Var>
231 forceinline
232 LayeredGraph<View,Val,Degree,StateIdx>::LayeredGraph(Home home,
233 const VarArgArray<Var>& x,
234 const DFA& dfa)
235 : Propagator(home), c(home), n(x.size()),
236 max_states(static_cast<StateIdx>(dfa.n_states())) {
237 assert(n > 0);
238 }
239
240 template<class View, class Val, class Degree, class StateIdx>
241 forceinline void
242 LayeredGraph<View,Val,Degree,StateIdx>::audit(void) {
243#ifdef GECODE_AUDIT
244 // Check states and edge information to be consistent
245 unsigned int n_e = 0; // Number of edges
246 unsigned int n_s = 0; // Number of states
247 StateIdx m_s = 0; // Maximal number of states per layer
248 for (int i=n; i--; ) {
249 n_s += layers[i].n_states;
250 m_s = std::max(m_s,layers[i].n_states);
251 for (ValSize j=layers[i].size; j--; )
252 n_e += layers[i].support[j].n_edges;
253 }
254 n_s += layers[n].n_states;
255 m_s = std::max(m_s,layers[n].n_states);
256 assert(n_e == n_edges);
257 assert(n_s <= n_states);
258 assert(m_s <= max_states);
259#endif
260 }
261
262 template<class View, class Val, class Degree, class StateIdx>
263 template<class Var>
264 forceinline ExecStatus
265 LayeredGraph<View,Val,Degree,StateIdx>::initialize(Space& home,
266 const VarArgArray<Var>& x,
267 const DFA& dfa) {
268
269 Region r;
270
271 // Allocate memory for layers
272 layers = home.alloc<Layer>(n+1);
273
274 // Allocate temporary memory for all possible states
275 State* states = r.alloc<State>(max_states*(n+1));
276 for (int i=0; i<static_cast<int>(max_states)*(n+1); i++)
277 states[i].init();
278 for (int i=0; i<n+1; i++)
279 layers[i].states = states + i*max_states;
280
281 // Allocate temporary memory for edges
282 Edge* edges = r.alloc<Edge>(dfa.max_degree());
283
284 // Mark initial state as being reachable
285 i_state(0,0).i_deg = 1;
286
287 // Forward pass: add transitions
288 for (int i=0; i<n; i++) {
289 layers[i].x = x[i];
290 layers[i].support = home.alloc<Support>(layers[i].x.size());
291 ValSize j=0;
292 // Enter links leaving reachable states (indegree != 0)
293 for (ViewValues<View> nx(layers[i].x); nx(); ++nx) {
294 Degree n_edges=0;
295 for (DFA::Transitions t(dfa,nx.val()); t(); ++t)
296 if (i_state(i,static_cast<StateIdx>(t.i_state())).i_deg != 0) {
297 i_state(i,static_cast<StateIdx>(t.i_state())).o_deg++;
298 o_state(i,static_cast<StateIdx>(t.o_state())).i_deg++;
299 edges[n_edges].i_state = static_cast<StateIdx>(t.i_state());
300 edges[n_edges].o_state = static_cast<StateIdx>(t.o_state());
301 n_edges++;
302 }
303 assert(n_edges <= dfa.max_degree());
304 // Found support for value
305 if (n_edges > 0) {
306 Support& s = layers[i].support[j];
307 s.val = static_cast<Val>(nx.val());
308 s.n_edges = n_edges;
309 s.edges = Heap::copy(home.alloc<Edge>(n_edges),edges,n_edges);
310 j++;
311 }
312 }
313 if ((layers[i].size = j) == 0)
314 return ES_FAILED;
315 }
316
317 // Mark final states as reachable
318 for (int s=dfa.final_fst(); s<dfa.final_lst(); s++)
319 if (o_state(n-1,static_cast<StateIdx>(s)).i_deg != 0)
320 o_state(n-1,static_cast<StateIdx>(s)).o_deg = 1;
321
322 // Backward pass: prune all transitions that do not lead to final state
323 for (int i=n; i--; ) {
324 ValSize k=0;
325 for (ValSize j=0; j<layers[i].size; j++) {
326 Support& s = layers[i].support[j];
327 for (Degree d=s.n_edges; d--; )
328 if (o_state(i,s.edges[d]).o_deg == 0) {
329 // Adapt states
330 i_dec(i,s.edges[d]); o_dec(i,s.edges[d]);
331 // Prune edge
332 s.edges[d] = s.edges[--s.n_edges];
333 }
334 // Value has support, copy the support information
335 if (s.n_edges > 0)
336 layers[i].support[k++]=s;
337 }
338 if ((layers[i].size = k) == 0)
339 return ES_FAILED;
340 LayerValues lv(layers[i]);
341 GECODE_ME_CHECK(layers[i].x.narrow_v(home,lv,false));
342 if (!layers[i].x.assigned())
343 layers[i].x.subscribe(home, *new (home) Index(home,*this,c,i));
344 }
345
346 // Copy and compress states, setup other information
347 {
348 // State map for in-states
349 StateIdx* i_map = r.alloc<StateIdx>(max_states);
350 // State map for out-states
351 StateIdx* o_map = r.alloc<StateIdx>(max_states);
352 // Number of in-states
353 StateIdx i_n = 0;
354
355 // Initialize map for in-states (special for last layer)
356 // Degree for single final state
357 unsigned int d = 0;
358 for (StateIdx j=0; j<max_states; j++)
359 d += static_cast<unsigned int>(layers[n].states[j].i_deg);
360 // Check whether all final states can be joined to a single state
361 if (d >
362 static_cast<unsigned int>
363 (Gecode::Support::IntTypeTraits<Degree>::max)) {
364 // Initialize map for in-states
365 for (StateIdx j=max_states; j--; )
366 if ((layers[n].states[j].o_deg != 0) ||
367 (layers[n].states[j].i_deg != 0))
368 i_map[j]=i_n++;
369 } else {
370 i_n = 1;
371 for (StateIdx j=max_states; j--; ) {
372 layers[n].states[j].init();
373 i_map[j] = 0;
374 }
375 layers[n].states[0].i_deg = static_cast<Degree>(d);
376 layers[n].states[0].o_deg = 1;
377 }
378 layers[n].n_states = i_n;
379
380 // Total number of states
381 n_states = i_n;
382 // Total number of edges
383 n_edges = 0;
384 // New maximal number of states
385 StateIdx max_s = i_n;
386
387 for (int i=n; i--; ) {
388 // In-states become out-states
389 std::swap(o_map,i_map); i_n=0;
390 // Initialize map for in-states
391 for (StateIdx j=max_states; j--; )
392 if ((layers[i].states[j].o_deg != 0) ||
393 (layers[i].states[j].i_deg != 0))
394 i_map[j]=i_n++;
395 layers[i].n_states = i_n;
396 n_states += i_n;
397 max_s = std::max(max_s,i_n);
398
399 // Update states in edges
400 for (ValSize j=layers[i].size; j--; ) {
401 Support& ls = layers[i].support[j];
402 n_edges += ls.n_edges;
403 for (Degree deg=ls.n_edges; deg--; ) {
404 ls.edges[deg].i_state = i_map[ls.edges[deg].i_state];
405 ls.edges[deg].o_state = o_map[ls.edges[deg].o_state];
406 }
407 }
408 }
409
410 // Allocate and copy states
411 State* a_states = home.alloc<State>(n_states);
412 for (int i=n+1; i--; ) {
413 StateIdx k=0;
414 for (StateIdx j=max_states; j--; )
415 if ((layers[i].states[j].o_deg != 0) ||
416 (layers[i].states[j].i_deg != 0))
417 a_states[k++] = layers[i].states[j];
418 assert(k == layers[i].n_states);
419 layers[i].states = a_states;
420 a_states += layers[i].n_states;
421 }
422
423 // Update maximal number of states
424 max_states = max_s;
425 }
426
427 // Schedule if subsumption is needed
428 if (c.empty())
429 View::schedule(home,*this,ME_INT_VAL);
430
431 audit();
432 return ES_OK;
433 }
434
435 template<class View, class Val, class Degree, class StateIdx>
436 ExecStatus
437 LayeredGraph<View,Val,Degree,StateIdx>::advise(Space& home,
438 Advisor& _a, const Delta& d) {
439 // Check whether state information has already been created
440 if (layers[0].states == nullptr) {
441 State* states = home.alloc<State>(n_states);
442 for (unsigned int i=0; i<n_states; i++)
443 states[i].init();
444 layers[n].states = states;
445 states += layers[n].n_states;
446 for (int i=n; i--; ) {
447 layers[i].states = states;
448 states += layers[i].n_states;
449 for (ValSize j=layers[i].size; j--; ) {
450 Support& s = layers[i].support[j];
451 for (Degree deg=s.n_edges; deg--; ) {
452 i_state(i,s.edges[deg]).o_deg++;
453 o_state(i,s.edges[deg]).i_deg++;
454 }
455 }
456 }
457 }
458
459 Index& a = static_cast<Index&>(_a);
460 const int i = a.i;
461
462 if (layers[i].size <= layers[i].x.size()) {
463 // Propagator has already done everything
464 if (View::modevent(d) == ME_INT_VAL) {
465 a.dispose(home,c);
466 return c.empty() ? ES_NOFIX : ES_FIX;
467 } else {
468 return ES_FIX;
469 }
470 }
471
472 bool i_mod = false;
473 bool o_mod = false;
474
475 if (View::modevent(d) == ME_INT_VAL) {
476 Val n = static_cast<Val>(layers[i].x.val());
477 ValSize j=0;
478 for (; layers[i].support[j].val < n; j++) {
479 Support& s = layers[i].support[j];
480 n_edges -= s.n_edges;
481 // Supported value not any longer in view
482 for (Degree deg=s.n_edges; deg--; ) {
483 // Adapt states
484 o_mod |= i_dec(i,s.edges[deg]);
485 i_mod |= o_dec(i,s.edges[deg]);
486 }
487 }
488 assert(layers[i].support[j].val == n);
489 layers[i].support[0] = layers[i].support[j++];
490 ValSize s=layers[i].size;
491 layers[i].size = 1;
492 for (; j<s; j++) {
493 Support& ls = layers[i].support[j];
494 n_edges -= ls.n_edges;
495 for (Degree deg=ls.n_edges; deg--; ) {
496 // Adapt states
497 o_mod |= i_dec(i,ls.edges[deg]);
498 i_mod |= o_dec(i,ls.edges[deg]);
499 }
500 }
501 } else if (layers[i].x.any(d)) {
502 ValSize j=0;
503 ValSize k=0;
504 ValSize s=layers[i].size;
505 for (ViewRanges<View> rx(layers[i].x); rx() && (j<s);) {
506 Support& ls = layers[i].support[j];
507 if (ls.val < static_cast<Val>(rx.min())) {
508 // Supported value not any longer in view
509 n_edges -= ls.n_edges;
510 for (Degree deg=ls.n_edges; deg--; ) {
511 // Adapt states
512 o_mod |= i_dec(i,ls.edges[deg]);
513 i_mod |= o_dec(i,ls.edges[deg]);
514 }
515 ++j;
516 } else if (ls.val > static_cast<Val>(rx.max())) {
517 ++rx;
518 } else {
519 layers[i].support[k++]=ls;
520 ++j;
521 }
522 }
523 assert(k > 0);
524 layers[i].size = k;
525 // Remove remaining values
526 for (; j<s; j++) {
527 Support& ls=layers[i].support[j];
528 n_edges -= ls.n_edges;
529 for (Degree deg=ls.n_edges; deg--; ) {
530 // Adapt states
531 o_mod |= i_dec(i,ls.edges[deg]);
532 i_mod |= o_dec(i,ls.edges[deg]);
533 }
534 }
535 } else {
536 Val min = static_cast<Val>(layers[i].x.min(d));
537 ValSize j=0;
538 // Skip values smaller than min (to keep)
539 for (; layers[i].support[j].val < min; j++) {}
540 Val max = static_cast<Val>(layers[i].x.max(d));
541 ValSize k=j;
542 ValSize s=layers[i].size;
543 // Remove pruned values
544 for (; (j<s) && (layers[i].support[j].val <= max); j++) {
545 Support& ls=layers[i].support[j];
546 n_edges -= ls.n_edges;
547 for (Degree deg=ls.n_edges; deg--; ) {
548 // Adapt states
549 o_mod |= i_dec(i,ls.edges[deg]);
550 i_mod |= o_dec(i,ls.edges[deg]);
551 }
552 }
553 // Keep remaining values
554 while (j<s)
555 layers[i].support[k++]=layers[i].support[j++];
556 layers[i].size=k;
557 assert(k > 0);
558 }
559
560 audit();
561
562 bool fix = true;
563 if (o_mod && (i > 0)) {
564 o_ch.add(i-1); fix = false;
565 }
566 if (i_mod && (i+1 < n)) {
567 i_ch.add(i+1); fix = false;
568 }
569 if (fix) {
570 if (View::modevent(d) == ME_INT_VAL) {
571 a.dispose(home,c);
572 return c.empty() ? ES_NOFIX : ES_FIX;
573 }
574 return ES_FIX;
575 } else {
576 return (View::modevent(d) == ME_INT_VAL)
577 ? home.ES_NOFIX_DISPOSE(c,a) : ES_NOFIX;
578 }
579 }
580
581 template<class View, class Val, class Degree, class StateIdx>
582 forceinline size_t
583 LayeredGraph<View,Val,Degree,StateIdx>::dispose(Space& home) {
584 c.dispose(home);
585 (void) Propagator::dispose(home);
586 return sizeof(*this);
587 }
588
589 template<class View, class Val, class Degree, class StateIdx>
590 void
591 LayeredGraph<View,Val,Degree,StateIdx>::reschedule(Space& home) {
592 View::schedule(home,*this,c.empty() ? ME_INT_VAL : ME_INT_DOM);
593 }
594
595 template<class View, class Val, class Degree, class StateIdx>
596 ExecStatus
597 LayeredGraph<View,Val,Degree,StateIdx>::propagate(Space& home,
598 const ModEventDelta&) {
599 // Forward pass
600 for (int i=i_ch.fst(); i<=i_ch.lst(); i++) {
601 bool i_mod = false;
602 bool o_mod = false;
603 ValSize j=0;
604 ValSize k=0;
605 ValSize ls=layers[i].size;
606 do {
607 Support& s=layers[i].support[j];
608 n_edges -= s.n_edges;
609 for (Degree d=s.n_edges; d--; )
610 if (i_state(i,s.edges[d]).i_deg == 0) {
611 // Adapt states
612 o_mod |= i_dec(i,s.edges[d]);
613 i_mod |= o_dec(i,s.edges[d]);
614 // Remove edge
615 s.edges[d] = s.edges[--s.n_edges];
616 }
617 n_edges += s.n_edges;
618 // Check whether value is still supported
619 if (s.n_edges == 0) {
620 layers[i].size--;
621 GECODE_ME_CHECK(layers[i].x.nq(home,s.val));
622 } else {
623 layers[i].support[k++]=s;
624 }
625 } while (++j<ls);
626 assert(k > 0);
627 // Update modification information
628 if (o_mod && (i > 0))
629 o_ch.add(i-1);
630 if (i_mod && (i+1 < n))
631 i_ch.add(i+1);
632 }
633
634 // Backward pass
635 for (int i=o_ch.lst(); i>=o_ch.fst(); i--) {
636 bool o_mod = false;
637 ValSize j=0;
638 ValSize k=0;
639 ValSize ls=layers[i].size;
640 do {
641 Support& s=layers[i].support[j];
642 n_edges -= s.n_edges;
643 for (Degree d=s.n_edges; d--; )
644 if (o_state(i,s.edges[d]).o_deg == 0) {
645 // Adapt states
646 o_mod |= i_dec(i,s.edges[d]);
647 (void) o_dec(i,s.edges[d]);
648 // Remove edge
649 s.edges[d] = s.edges[--s.n_edges];
650 }
651 n_edges += s.n_edges;
652 // Check whether value is still supported
653 if (s.n_edges == 0) {
654 layers[i].size--;
655 GECODE_ME_CHECK(layers[i].x.nq(home,s.val));
656 } else {
657 layers[i].support[k++]=s;
658 }
659 } while (++j<ls);
660 assert(k > 0);
661 // Update modification information
662 if (o_mod && (i > 0))
663 o_ch.add(i-1);
664 }
665
666 a_ch.add(i_ch); i_ch.reset();
667 a_ch.add(o_ch); o_ch.reset();
668
669 audit();
670
671 // Check subsumption
672 if (c.empty())
673 return home.ES_SUBSUMED(*this);
674 else
675 return ES_FIX;
676 }
677
678
679 template<class View, class Val, class Degree, class StateIdx>
680 template<class Var>
681 ExecStatus
682 LayeredGraph<View,Val,Degree,StateIdx>::post(Home home,
683 const VarArgArray<Var>& x,
684 const DFA& dfa) {
685 if (x.size() == 0) {
686 // Check whether the start state 0 is also a final state
687 if ((dfa.final_fst() <= 0) && (dfa.final_lst() >= 0))
688 return ES_OK;
689 return ES_FAILED;
690 }
691 assert(x.size() > 0);
692 for (int i=0; i<x.size(); i++) {
693 DFA::Symbols s(dfa);
694 typename VarTraits<Var>::View xi(x[i]);
695 GECODE_ME_CHECK(xi.inter_v(home,s,false));
696 }
697 LayeredGraph<View,Val,Degree,StateIdx>* p =
698 new (home) LayeredGraph<View,Val,Degree,StateIdx>(home,x,dfa);
699 return p->initialize(home,x,dfa);
700 }
701
702 template<class View, class Val, class Degree, class StateIdx>
703 forceinline
704 LayeredGraph<View,Val,Degree,StateIdx>
705 ::LayeredGraph(Space& home, LayeredGraph<View,Val,Degree,StateIdx>& p)
706 : Propagator(home,p),
707 n(p.n), layers(home.alloc<Layer>(n+1)),
708 max_states(p.max_states), n_states(p.n_states), n_edges(p.n_edges) {
709 c.update(home,p.c);
710 // Do not allocate states, postpone to advise!
711 layers[n].n_states = p.layers[n].n_states;
712 layers[n].states = nullptr;
713 // Allocate memory for edges
714 Edge* edges = home.alloc<Edge>(n_edges);
715 // Copy layers
716 for (int i=0; i<n; i++) {
717 layers[i].x.update(home,p.layers[i].x);
718 assert(layers[i].x.size() == p.layers[i].size);
719 layers[i].size = p.layers[i].size;
720 layers[i].support = home.alloc<Support>(layers[i].size);
721 for (ValSize j=0; j<layers[i].size; j++) {
722 layers[i].support[j].val = p.layers[i].support[j].val;
723 layers[i].support[j].n_edges = p.layers[i].support[j].n_edges;
724 assert(layers[i].support[j].n_edges > 0);
725 layers[i].support[j].edges =
726 Heap::copy(edges,p.layers[i].support[j].edges,
727 layers[i].support[j].n_edges);
728 edges += layers[i].support[j].n_edges;
729 }
730 layers[i].n_states = p.layers[i].n_states;
731 layers[i].states = nullptr;
732 }
733 audit();
734 }
735
736 template<class View, class Val, class Degree, class StateIdx>
737 PropCost
738 LayeredGraph<View,Val,Degree,StateIdx>::cost(const Space&,
739 const ModEventDelta&) const {
740 return PropCost::linear(PropCost::HI,n);
741 }
742
743 template<class View, class Val, class Degree, class StateIdx>
744 Actor*
745 LayeredGraph<View,Val,Degree,StateIdx>::copy(Space& home) {
746 // Eliminate an assigned prefix
747 {
748 int k=0;
749 while (layers[k].size == 1) {
750 assert(layers[k].support[0].n_edges == 1);
751 n_states -= layers[k].n_states;
752 k++;
753 }
754 if (k > 0) {
755 /*
756 * The state information is always available: either the propagator
757 * has been created (hence, also the state information has been
758 * created), or the first variable become assigned and hence
759 * an advisor must have been run (which then has created the state
760 * information).
761 */
762 // Eliminate assigned layers
763 n -= k; layers += k;
764 // Eliminate edges
765 n_edges -= static_cast<unsigned int>(k);
766 // Update advisor indices
767 for (Advisors<Index> as(c); as(); ++as)
768 as.advisor().i -= k;
769 // Update all change information
770 a_ch.lshift(k);
771 }
772 }
773 audit();
774
775 // Compress states
776 if (!a_ch.empty()) {
777 int f = a_ch.fst();
778 int l = a_ch.lst();
779 assert((f >= 0) && (l <= n));
780 Region r;
781 // State map for in-states
782 StateIdx* i_map = r.alloc<StateIdx>(max_states);
783 // State map for out-states
784 StateIdx* o_map = r.alloc<StateIdx>(max_states);
785 // Number of in-states
786 StateIdx i_n = 0;
787
788 n_states -= layers[l].n_states;
789 // Initialize map for in-states and compress
790 for (StateIdx j=0; j<layers[l].n_states; j++)
791 if ((layers[l].states[j].i_deg != 0) ||
792 (layers[l].states[j].o_deg != 0)) {
793 layers[l].states[i_n]=layers[l].states[j];
794 i_map[j]=i_n++;
795 }
796 layers[l].n_states = i_n;
797 n_states += layers[l].n_states;
798 assert(i_n > 0);
799
800 // Update in-states in edges for last layer, if any
801 if (l < n)
802 for (ValSize j=layers[l].size; j--; ) {
803 Support& s = layers[l].support[j];
804 for (Degree d=s.n_edges; d--; )
805 s.edges[d].i_state = i_map[s.edges[d].i_state];
806 }
807
808 // Update all changed layers
809 for (int i=l-1; i>=f; i--) {
810 // In-states become out-states
811 std::swap(o_map,i_map); i_n=0;
812 // Initialize map for in-states and compress
813 n_states -= layers[i].n_states;
814 for (StateIdx j=0; j<layers[i].n_states; j++)
815 if ((layers[i].states[j].o_deg != 0) ||
816 (layers[i].states[j].i_deg != 0)) {
817 layers[i].states[i_n]=layers[i].states[j];
818 i_map[j]=i_n++;
819 }
820 layers[i].n_states = i_n;
821 n_states += layers[i].n_states;
822 assert(i_n > 0);
823
824 // Update states in edges
825 for (ValSize j=layers[i].size; j--; ) {
826 Support& s = layers[i].support[j];
827 for (Degree d=s.n_edges; d--; ) {
828 s.edges[d].i_state = i_map[s.edges[d].i_state];
829 s.edges[d].o_state = o_map[s.edges[d].o_state];
830 }
831 }
832 }
833
834 // Update out-states in edges for previous layer, if any
835 if (f > 0)
836 for (ValSize j=layers[f-1].size; j--; ) {
837 Support& s = layers[f-1].support[j];
838 for (Degree d=s.n_edges; d--; )
839 s.edges[d].o_state = i_map[s.edges[d].o_state];
840 }
841
842 a_ch.reset();
843 }
844 audit();
845
846 return new (home) LayeredGraph<View,Val,Degree,StateIdx>(home,*this);
847 }
848
849 /// Select small types for the layered graph propagator
850 template<class Var>
851 forceinline ExecStatus
852 post_lgp(Home home, const VarArgArray<Var>& x, const DFA& dfa) {
853 Gecode::Support::IntType t_state_idx =
854 Gecode::Support::u_type(static_cast<unsigned int>(dfa.n_states()));
855 Gecode::Support::IntType t_degree =
856 Gecode::Support::u_type(dfa.max_degree());
857 Gecode::Support::IntType t_val =
858 std::max(Support::s_type(dfa.symbol_min()),
859 Support::s_type(dfa.symbol_max()));
860 switch (t_val) {
861 case Gecode::Support::IT_CHAR:
862 // fall through
863 case Gecode::Support::IT_SHRT:
864 switch (t_state_idx) {
865 case Gecode::Support::IT_CHAR:
866 switch (t_degree) {
867 case Gecode::Support::IT_CHAR:
868 return Extensional::LayeredGraph
869 <typename VarTraits<Var>::View,short int,unsigned char,unsigned char>
870 ::post(home,x,dfa);
871 case Gecode::Support::IT_SHRT:
872 return Extensional::LayeredGraph
873 <typename VarTraits<Var>::View,short int,unsigned short int,unsigned char>
874 ::post(home,x,dfa);
875 case Gecode::Support::IT_INT:
876 return Extensional::LayeredGraph
877 <typename VarTraits<Var>::View,short int,unsigned int,unsigned char>
878 ::post(home,x,dfa);
879 default: GECODE_NEVER;
880 }
881 break;
882 case Gecode::Support::IT_SHRT:
883 switch (t_degree) {
884 case Gecode::Support::IT_CHAR:
885 return Extensional::LayeredGraph
886 <typename VarTraits<Var>::View,short int,unsigned char,unsigned short int>
887 ::post(home,x,dfa);
888 case Gecode::Support::IT_SHRT:
889 return Extensional::LayeredGraph
890 <typename VarTraits<Var>::View,short int,unsigned short int,unsigned short int>
891 ::post(home,x,dfa);
892 case Gecode::Support::IT_INT:
893 return Extensional::LayeredGraph
894 <typename VarTraits<Var>::View,short int,unsigned int,unsigned short int>
895 ::post(home,x,dfa);
896 default: GECODE_NEVER;
897 }
898 break;
899 case Gecode::Support::IT_INT:
900 switch (t_degree) {
901 case Gecode::Support::IT_CHAR:
902 return Extensional::LayeredGraph
903 <typename VarTraits<Var>::View,short int,unsigned char,unsigned int>
904 ::post(home,x,dfa);
905 case Gecode::Support::IT_SHRT:
906 return Extensional::LayeredGraph
907 <typename VarTraits<Var>::View,short int,unsigned short int,unsigned int>
908 ::post(home,x,dfa);
909 case Gecode::Support::IT_INT:
910 return Extensional::LayeredGraph
911 <typename VarTraits<Var>::View,short int,unsigned int,unsigned int>
912 ::post(home,x,dfa);
913 default: GECODE_NEVER;
914 }
915 break;
916 default: GECODE_NEVER;
917 }
918 break;
919 case Gecode::Support::IT_INT:
920 switch (t_state_idx) {
921 case Gecode::Support::IT_CHAR:
922 switch (t_degree) {
923 case Gecode::Support::IT_CHAR:
924 return Extensional::LayeredGraph
925 <typename VarTraits<Var>::View,int,unsigned char,unsigned char>
926 ::post(home,x,dfa);
927 case Gecode::Support::IT_SHRT:
928 return Extensional::LayeredGraph
929 <typename VarTraits<Var>::View,int,unsigned short int,unsigned char>
930 ::post(home,x,dfa);
931 case Gecode::Support::IT_INT:
932 return Extensional::LayeredGraph
933 <typename VarTraits<Var>::View,int,unsigned int,unsigned char>
934 ::post(home,x,dfa);
935 default: GECODE_NEVER;
936 }
937 break;
938 case Gecode::Support::IT_SHRT:
939 switch (t_degree) {
940 case Gecode::Support::IT_CHAR:
941 return Extensional::LayeredGraph
942 <typename VarTraits<Var>::View,int,unsigned char,unsigned short int>
943 ::post(home,x,dfa);
944 case Gecode::Support::IT_SHRT:
945 return Extensional::LayeredGraph
946 <typename VarTraits<Var>::View,int,unsigned short int,unsigned short int>
947 ::post(home,x,dfa);
948 case Gecode::Support::IT_INT:
949 return Extensional::LayeredGraph
950 <typename VarTraits<Var>::View,int,unsigned int,unsigned short int>
951 ::post(home,x,dfa);
952 default: GECODE_NEVER;
953 }
954 break;
955 case Gecode::Support::IT_INT:
956 switch (t_degree) {
957 case Gecode::Support::IT_CHAR:
958 return Extensional::LayeredGraph
959 <typename VarTraits<Var>::View,int,unsigned char,unsigned int>
960 ::post(home,x,dfa);
961 case Gecode::Support::IT_SHRT:
962 return Extensional::LayeredGraph
963 <typename VarTraits<Var>::View,int,unsigned short int,unsigned int>
964 ::post(home,x,dfa);
965 case Gecode::Support::IT_INT:
966 return Extensional::LayeredGraph
967 <typename VarTraits<Var>::View,int,unsigned int,unsigned int>
968 ::post(home,x,dfa);
969 default: GECODE_NEVER;
970 }
971 break;
972 default: GECODE_NEVER;
973 }
974
975 default: GECODE_NEVER;
976 }
977 return ES_OK;
978 }
979
980}}}
981
982// STATISTICS: int-prop
983