this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Guido Tack <tack@gecode.org>
5 * Christian Schulte <schulte@gecode.org>
6 *
7 * Copyright:
8 * Guido Tack, 2010
9 * Christian Schulte, 2004
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 <gecode/minimodel.hh>
37
38#ifdef GECODE_HAS_SET_VARS
39
40namespace Gecode {
41
42 namespace {
43 /// Check if types agree
44 static bool same(SetExpr::NodeType t0, SetExpr::NodeType t1) {
45 return (t0==t1) || (t1==SetExpr::NT_VAR) ||
46 (t1==SetExpr::NT_CONST) || (t1==SetExpr::NT_LEXP);
47 }
48 }
49
50 /// %Node for set expression
51 class SetExpr::Node {
52 public:
53 /// Nodes are reference counted
54 unsigned int use;
55 /// Number of variables in subtree with same type (for INTER and UNION)
56 int same;
57 /// Type of expression
58 NodeType t;
59 /// Subexpressions
60 Node *l, *r;
61 /// Possibly a variable
62 SetVar x;
63 /// Possibly a constant
64 IntSet s;
65 /// Possibly a linear expression
66 LinIntExpr e;
67
68 /// Default constructor
69 Node(void);
70 /// Decrement reference count and possibly free memory
71 GECODE_MINIMODEL_EXPORT
72 bool decrement(void);
73 /// Memory management
74 static void* operator new(size_t size);
75 /// Memory management
76 static void operator delete(void* p, size_t size);
77 };
78
79 /*
80 * Operations for nodes
81 *
82 */
83 SetExpr::Node::Node(void) : use(1) {}
84
85 void*
86 SetExpr::Node::operator new(size_t size) {
87 return heap.ralloc(size);
88 }
89 void
90 SetExpr::Node::operator delete(void* p, size_t) {
91 heap.rfree(p);
92 }
93
94 bool
95 SetExpr::Node::decrement(void) {
96 if (--use == 0) {
97 if ((l != nullptr) && l->decrement())
98 delete l;
99 if ((r != nullptr) && r->decrement())
100 delete r;
101 return true;
102 }
103 return false;
104 }
105
106 namespace {
107 /// %Node for negation normalform (%NNF)
108 class NNF {
109 public:
110 typedef SetExpr::NodeType NodeType;
111 typedef SetExpr::Node Node;
112 /// Type of node
113 NodeType t;
114 /// Number of positive literals for node type
115 int p;
116 /// Number of negative literals for node type
117 int n;
118 /// Union depending on nodetype \a t
119 union {
120 /// For binary nodes (and, or, eqv)
121 struct {
122 /// Left subtree
123 NNF* l;
124 /// Right subtree
125 NNF* r;
126 } b;
127 /// For atomic nodes
128 struct {
129 /// Pointer to corresponding Boolean expression node
130 Node* x;
131 } a;
132 } u;
133 /// Is formula negative
134 bool neg;
135 /// Create negation normalform
136 static NNF* nnf(Region& r, Node* n, bool neg);
137 /// Post propagators for nested conjunctive and disjunctive expression
138 void post(Home home, NodeType t, SetVarArgs& b, int& i) const;
139 /// Post propagators for expression
140 void post(Home home, SetRelType srt, SetVar s) const;
141 /// Post propagators for reified expression
142 void post(Home home, SetRelType srt, SetVar s, BoolVar b) const;
143 /// Post propagators for relation
144 void post(Home home, SetRelType srt, const NNF* n) const;
145 /// Post reified propagators for relation (or negated relation if \a t is false)
146 void post(Home home, BoolVar b, bool t, SetRelType srt,
147 const NNF* n) const;
148 /// Allocate memory from region
149 static void* operator new(size_t s, Region& r);
150 /// No-op (for exceptions)
151 static void operator delete(void*);
152 /// No-op
153 static void operator delete(void*, Region&);
154 };
155
156 /*
157 * Operations for negation normalform
158 *
159 */
160 forceinline void
161 NNF::operator delete(void*) {}
162
163 forceinline void
164 NNF::operator delete(void*, Region&) {}
165
166 forceinline void*
167 NNF::operator new(size_t s, Region& r) {
168 return r.ralloc(s);
169 }
170
171 void
172 NNF::post(Home home, SetRelType srt, SetVar s) const {
173 switch (t) {
174 case SetExpr::NT_VAR:
175 if (neg) {
176 switch (srt) {
177 case SRT_EQ:
178 rel(home, u.a.x->x, SRT_CMPL, s);
179 break;
180 case SRT_CMPL:
181 rel(home, u.a.x->x, SRT_EQ, s);
182 break;
183 default:
184 SetVar bc(home,IntSet::empty,
185 IntSet(Set::Limits::min,Set::Limits::max));
186 rel(home, s, SRT_CMPL, bc);
187 rel(home, u.a.x->x, srt, bc);
188 break;
189 }
190 } else
191 rel(home, u.a.x->x, srt, s);
192 break;
193 case SetExpr::NT_CONST:
194 {
195 IntSet ss;
196 if (neg) {
197 IntSetRanges sr(u.a.x->s);
198 Set::RangesCompl<IntSetRanges> src(sr);
199 ss = IntSet(src);
200 } else {
201 ss = u.a.x->s;
202 }
203 switch (srt) {
204 case SRT_SUB: srt = SRT_SUP; break;
205 case SRT_SUP: srt = SRT_SUB; break;
206 default: break;
207 }
208 dom(home, s, srt, ss);
209 }
210 break;
211 case SetExpr::NT_LEXP:
212 {
213 IntVar iv = u.a.x->e.post(home,IntPropLevels::def);
214 if (neg) {
215 SetVar ic(home,IntSet::empty,
216 IntSet(Set::Limits::min,Set::Limits::max));
217 rel(home, iv, SRT_CMPL, ic);
218 rel(home,ic,srt,s);
219 } else {
220 rel(home,iv,srt,s);
221 }
222 }
223 break;
224 case SetExpr::NT_INTER:
225 {
226 SetVarArgs bs(p+n);
227 int i=0;
228 post(home, SetExpr::NT_INTER, bs, i);
229 if (i == 2) {
230 rel(home, bs[0], SOT_INTER, bs[1], srt, s);
231 } else {
232 if (srt == SRT_EQ)
233 rel(home, SOT_INTER, bs, s);
234 else {
235 SetVar bc(home,IntSet::empty,
236 IntSet(Set::Limits::min,Set::Limits::max));
237 rel(home, SOT_INTER, bs, bc);
238 rel(home, bc, srt, s);
239 }
240 }
241 }
242 break;
243 case SetExpr::NT_UNION:
244 {
245 SetVarArgs bs(p+n);
246 int i=0;
247 post(home, SetExpr::NT_UNION, bs, i);
248 if (i == 2) {
249 rel(home, bs[0], SOT_UNION, bs[1], srt, s);
250 } else {
251 if (srt == SRT_EQ)
252 rel(home, SOT_UNION, bs, s);
253 else {
254 SetVar bc(home,IntSet::empty,
255 IntSet(Set::Limits::min,Set::Limits::max));
256 rel(home, SOT_UNION, bs, bc);
257 rel(home, bc, srt, s);
258 }
259 }
260 }
261 break;
262 case SetExpr::NT_DUNION:
263 {
264 SetVarArgs bs(p+n);
265 int i=0;
266 post(home, SetExpr::NT_DUNION, bs, i);
267
268 if (i == 2) {
269 if (neg) {
270 if (srt == SRT_CMPL) {
271 rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
272 } else {
273 SetVar bc(home,IntSet::empty,
274 IntSet(Set::Limits::min,Set::Limits::max));
275 rel(home,s,SRT_CMPL,bc);
276 rel(home, bs[0], SOT_DUNION, bs[1], srt, bc);
277 }
278 } else {
279 rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
280 }
281 } else {
282 if (neg) {
283 if (srt == SRT_CMPL) {
284 rel(home, SOT_DUNION, bs, s);
285 } else {
286 SetVar br(home,IntSet::empty,
287 IntSet(Set::Limits::min,Set::Limits::max));
288 rel(home, SOT_DUNION, bs, br);
289 if (srt == SRT_EQ)
290 rel(home, br, SRT_CMPL, s);
291 else {
292 SetVar bc(home,IntSet::empty,
293 IntSet(Set::Limits::min,Set::Limits::max));
294 rel(home, br, srt, bc);
295 rel(home, bc, SRT_CMPL, s);
296 }
297 }
298 } else {
299 if (srt == SRT_EQ)
300 rel(home, SOT_DUNION, bs, s);
301 else {
302 SetVar br(home,IntSet::empty,
303 IntSet(Set::Limits::min,Set::Limits::max));
304 rel(home, SOT_DUNION, bs, br);
305 rel(home, br, srt, s);
306 }
307 }
308 }
309 }
310 break;
311 default:
312 GECODE_NEVER;
313 }
314 }
315
316 void
317 NNF::post(Home home, SetRelType srt, SetVar s, BoolVar b) const {
318 switch (t) {
319 case SetExpr::NT_VAR:
320 if (neg) {
321 switch (srt) {
322 case SRT_EQ:
323 rel(home, u.a.x->x, SRT_CMPL, s, b);
324 break;
325 case SRT_CMPL:
326 rel(home, u.a.x->x, SRT_EQ, s, b);
327 break;
328 default:
329 SetVar bc(home,IntSet::empty,
330 IntSet(Set::Limits::min,Set::Limits::max));
331 rel(home, s, SRT_CMPL, bc);
332 rel(home, u.a.x->x, srt, bc, b);
333 break;
334 }
335 } else
336 rel(home, u.a.x->x, srt, s, b);
337 break;
338 case SetExpr::NT_CONST:
339 {
340 IntSet ss;
341 if (neg) {
342 IntSetRanges sr(u.a.x->s);
343 Set::RangesCompl<IntSetRanges> src(sr);
344 ss = IntSet(src);
345 } else {
346 ss = u.a.x->s;
347 }
348 SetRelType invsrt;
349 switch (srt) {
350 case SRT_SUB: invsrt = SRT_SUP; break;
351 case SRT_SUP: invsrt = SRT_SUB; break;
352 case SRT_LQ: invsrt = SRT_GQ; break;
353 case SRT_LE: invsrt = SRT_GR; break;
354 case SRT_GQ: invsrt = SRT_LQ; break;
355 case SRT_GR: invsrt = SRT_LE; break;
356 case SRT_EQ:
357 case SRT_NQ:
358 case SRT_DISJ:
359 case SRT_CMPL:
360 invsrt = srt;
361 break;
362 default:
363 invsrt = srt;
364 GECODE_NEVER;
365 }
366 dom(home, s, invsrt, ss, b);
367 }
368 break;
369 case SetExpr::NT_LEXP:
370 {
371 IntVar iv = u.a.x->e.post(home,IntPropLevels::def);
372 if (neg) {
373 SetVar ic(home,IntSet::empty,
374 IntSet(Set::Limits::min,Set::Limits::max));
375 rel(home, iv, SRT_CMPL, ic);
376 rel(home,ic,srt,s,b);
377 } else {
378 rel(home,iv,srt,s,b);
379 }
380 }
381 break;
382 case SetExpr::NT_INTER:
383 {
384 SetVarArgs bs(p+n);
385 int i=0;
386 post(home, SetExpr::NT_INTER, bs, i);
387 SetVar br(home,IntSet::empty,
388 IntSet(Set::Limits::min,Set::Limits::max));
389 rel(home, SOT_INTER, bs, br);
390 rel(home, br, srt, s, b);
391 }
392 break;
393 case SetExpr::NT_UNION:
394 {
395 SetVarArgs bs(p+n);
396 int i=0;
397 post(home, SetExpr::NT_UNION, bs, i);
398 SetVar br(home,IntSet::empty,
399 IntSet(Set::Limits::min,Set::Limits::max));
400 rel(home, SOT_UNION, bs, br);
401 rel(home, br, srt, s, b);
402 }
403 break;
404 case SetExpr::NT_DUNION:
405 {
406 SetVarArgs bs(p+n);
407 int i=0;
408 post(home, SetExpr::NT_DUNION, bs, i);
409
410 if (neg) {
411 SetVar br(home,IntSet::empty,
412 IntSet(Set::Limits::min,Set::Limits::max));
413 rel(home, SOT_DUNION, bs, br);
414 if (srt == SRT_CMPL)
415 rel(home, br, SRT_EQ, s, b);
416 else if (srt == SRT_EQ)
417 rel(home, br, SRT_CMPL, s, b);
418 else {
419 SetVar bc(home,IntSet::empty,
420 IntSet(Set::Limits::min,Set::Limits::max));
421 rel(home, br, srt, bc);
422 rel(home, bc, SRT_CMPL, s, b);
423 }
424 } else {
425 SetVar br(home,IntSet::empty,
426 IntSet(Set::Limits::min,Set::Limits::max));
427 rel(home, SOT_DUNION, bs, br);
428 rel(home, br, srt, s, b);
429 }
430 }
431 break;
432 default:
433 GECODE_NEVER;
434 }
435 }
436
437 void
438 NNF::post(Home home, NodeType t, SetVarArgs& b, int& i) const {
439 if (this->t != t) {
440 switch (this->t) {
441 case SetExpr::NT_VAR:
442 if (neg) {
443 SetVar xc(home,IntSet::empty,
444 IntSet(Set::Limits::min,Set::Limits::max));
445 rel(home, xc, SRT_CMPL, u.a.x->x);
446 b[i++]=xc;
447 } else {
448 b[i++]=u.a.x->x;
449 }
450 break;
451 default:
452 {
453 SetVar s(home,IntSet::empty,
454 IntSet(Set::Limits::min,Set::Limits::max));
455 post(home,SRT_EQ,s);
456 b[i++] = s;
457 }
458 break;
459 }
460 } else {
461 u.b.l->post(home, t, b, i);
462 u.b.r->post(home, t, b, i);
463 }
464 }
465
466 void
467 NNF::post(Home home, SetRelType srt, const NNF* n) const {
468 if (n->t == SetExpr::NT_VAR && !n->neg) {
469 post(home,srt,n->u.a.x->x);
470 } else if (t == SetExpr::NT_VAR && !neg) {
471 SetRelType n_srt;
472 switch (srt) {
473 case SRT_SUB: n_srt = SRT_SUP; break;
474 case SRT_SUP: n_srt = SRT_SUB; break;
475 default: n_srt = srt;
476 }
477 n->post(home,n_srt,this);
478 } else {
479 SetVar nx(home,IntSet::empty,
480 IntSet(Set::Limits::min,Set::Limits::max));
481 n->post(home,SRT_EQ,nx);
482 post(home,srt,nx);
483 }
484 }
485
486 void
487 NNF::post(Home home, BoolVar b, bool pt,
488 SetRelType srt, const NNF* n) const {
489 if (pt) {
490 if (n->t == SetExpr::NT_VAR && !n->neg) {
491 post(home,srt,n->u.a.x->x,b);
492 } else if (t == SetExpr::NT_VAR && !neg) {
493 SetRelType n_srt;
494 switch (srt) {
495 case SRT_SUB: n_srt = SRT_SUP; break;
496 case SRT_SUP: n_srt = SRT_SUB; break;
497 default: n_srt = srt;
498 }
499 n->post(home,b,true,n_srt,this);
500 } else {
501 SetVar nx(home,IntSet::empty,
502 IntSet(Set::Limits::min,Set::Limits::max));
503 n->post(home,SRT_EQ,nx);
504 post(home,srt,nx,b);
505 }
506 } else if (srt == SRT_EQ) {
507 post(home,b,true,SRT_NQ,n);
508 } else if (srt == SRT_NQ) {
509 post(home,b,true,SRT_EQ,n);
510 } else {
511 BoolVar nb(home,0,1);
512 rel(home,b,IRT_NQ,nb);
513 post(home,nb,true,srt,n);
514 }
515 }
516
517 NNF*
518 NNF::nnf(Region& r, Node* n, bool neg) {
519 switch (n->t) {
520 case SetExpr::NT_VAR:
521 case SetExpr::NT_CONST:
522 case SetExpr::NT_LEXP:
523 {
524 NNF* x = new (r) NNF;
525 x->t = n->t; x->neg = neg; x->u.a.x = n;
526 if (neg) {
527 x->p = 0; x->n = 1;
528 } else {
529 x->p = 1; x->n = 0;
530 }
531 return x;
532 }
533 case SetExpr::NT_CMPL:
534 return nnf(r,n->l,!neg);
535 case SetExpr::NT_INTER:
536 case SetExpr::NT_UNION:
537 case SetExpr::NT_DUNION:
538 {
539 NodeType t; bool xneg;
540 if (n->t == SetExpr::NT_DUNION) {
541 t = n->t; xneg = neg; neg = false;
542 } else {
543 t = ((n->t == SetExpr::NT_INTER) == neg) ?
544 SetExpr::NT_UNION : SetExpr::NT_INTER;
545 xneg = false;
546 }
547 NNF* x = new (r) NNF;
548 x->neg = xneg;
549 x->t = t;
550 x->u.b.l = nnf(r,n->l,neg);
551 x->u.b.r = nnf(r,n->r,neg);
552 int p_l, n_l;
553 if ((x->u.b.l->t == t) || (x->u.b.l->t == SetExpr::NT_VAR)) {
554 p_l=x->u.b.l->p; n_l=x->u.b.l->n;
555 } else {
556 p_l=1; n_l=0;
557 }
558 int p_r, n_r;
559 if ((x->u.b.r->t == t) || (x->u.b.r->t == SetExpr::NT_VAR)) {
560 p_r=x->u.b.r->p; n_r=x->u.b.r->n;
561 } else {
562 p_r=1; n_r=0;
563 }
564 x->p = p_l+p_r;
565 x->n = n_l+n_r;
566 return x;
567 }
568 default:
569 GECODE_NEVER;
570 }
571 GECODE_NEVER;
572 return nullptr;
573 }
574 }
575
576 SetExpr::SetExpr(const SetVar& x) : n(new Node) {
577 n->same = 1;
578 n->t = NT_VAR;
579 n->l = nullptr;
580 n->r = nullptr;
581 n->x = x;
582 }
583
584 SetExpr::SetExpr(const IntSet& s) : n(new Node) {
585 n->same = 1;
586 n->t = NT_CONST;
587 n->l = nullptr;
588 n->r = nullptr;
589 n->s = s;
590 }
591
592 SetExpr::SetExpr(const LinIntExpr& e) : n(new Node) {
593 n->same = 1;
594 n->t = NT_LEXP;
595 n->l = nullptr;
596 n->r = nullptr;
597 n->e = e;
598 }
599
600 SetExpr::SetExpr(const SetExpr& l, NodeType t, const SetExpr& r)
601 : n(new Node) {
602 int ls = same(t,l.n->t) ? l.n->same : 1;
603 int rs = same(t,r.n->t) ? r.n->same : 1;
604 n->same = ls+rs;
605 n->t = t;
606 n->l = l.n;
607 n->l->use++;
608 n->r = r.n;
609 n->r->use++;
610 }
611
612 SetExpr::SetExpr(const SetExpr& l, NodeType t) {
613 (void) t;
614 assert(t == NT_CMPL);
615 if (l.n->t == NT_CMPL) {
616 n = l.n->l;
617 n->use++;
618 } else {
619 n = new Node;
620 n->same = 1;
621 n->t = NT_CMPL;
622 n->l = l.n;
623 n->l->use++;
624 n->r = nullptr;
625 }
626 }
627
628 const SetExpr&
629 SetExpr::operator =(const SetExpr& e) {
630 if (this != &e) {
631 if (n != nullptr && n->decrement())
632 delete n;
633 n = e.n;
634 n->use++;
635 }
636 return *this;
637 }
638
639 SetExpr::~SetExpr(void) {
640 if (n != nullptr && n->decrement())
641 delete n;
642 }
643
644 SetExpr::SetExpr(const SetExpr& e) : n(e.n) {
645 n->use++;
646 }
647
648 SetVar
649 SetExpr::post(Home home) const {
650 Region r;
651 SetVar s(home,IntSet::empty,
652 IntSet(Set::Limits::min,Set::Limits::max));
653 NNF::nnf(r,n,false)->post(home,SRT_EQ,s);
654 return s;
655 }
656
657 void
658 SetExpr::post(Home home, SetRelType srt, const SetExpr& e) const {
659 Region r;
660 return NNF::nnf(r,n,false)->post(home,srt,NNF::nnf(r,e.n,false));
661 }
662 void
663 SetExpr::post(Home home, BoolVar b, bool t,
664 SetRelType srt, const SetExpr& e) const {
665 Region r;
666 return NNF::nnf(r,n,false)->post(home,b,t,srt,
667 NNF::nnf(r,e.n,false));
668 }
669
670 SetExpr
671 operator &(const SetExpr& l, const SetExpr& r) {
672 return SetExpr(l,SetExpr::NT_INTER,r);
673 }
674 SetExpr
675 operator |(const SetExpr& l, const SetExpr& r) {
676 return SetExpr(l,SetExpr::NT_UNION,r);
677 }
678 SetExpr
679 operator +(const SetExpr& l, const SetExpr& r) {
680 return SetExpr(l,SetExpr::NT_DUNION,r);
681 }
682 SetExpr
683 operator -(const SetExpr& e) {
684 return SetExpr(e,SetExpr::NT_CMPL);
685 }
686 SetExpr
687 operator -(const SetExpr& l, const SetExpr& r) {
688 return SetExpr(l,SetExpr::NT_INTER,-r);
689 }
690 SetExpr
691 singleton(const LinIntExpr& e) {
692 return SetExpr(e);
693 }
694
695 SetExpr
696 inter(const SetVarArgs& x) {
697 if (x.size() == 0)
698 return SetExpr(IntSet(Set::Limits::min,Set::Limits::max));
699 SetExpr r(x[0]);
700 for (int i=1; i<x.size(); i++)
701 r = (r & x[i]);
702 return r;
703 }
704 SetExpr
705 setunion(const SetVarArgs& x) {
706 if (x.size() == 0)
707 return SetExpr(IntSet::empty);
708 SetExpr r(x[0]);
709 for (int i=1; i<x.size(); i++)
710 r = (r | x[i]);
711 return r;
712 }
713 SetExpr
714 setdunion(const SetVarArgs& x) {
715 if (x.size() == 0)
716 return SetExpr(IntSet::empty);
717 SetExpr r(x[0]);
718 for (int i=1; i<x.size(); i++)
719 r = (r + x[i]);
720 return r;
721 }
722
723 namespace MiniModel {
724 /// Integer valued set expressions
725 class GECODE_MINIMODEL_EXPORT SetNonLinIntExpr : public NonLinIntExpr {
726 public:
727 /// The expression type
728 enum SetNonLinIntExprType {
729 SNLE_CARD, ///< Cardinality expression
730 SNLE_MIN, ///< Minimum element expression
731 SNLE_MAX ///< Maximum element expression
732 } t;
733 /// The expression
734 SetExpr e;
735 /// Constructor
736 SetNonLinIntExpr(const SetExpr& e0, SetNonLinIntExprType t0)
737 : t(t0), e(e0) {}
738 /// Post expression
739 virtual IntVar post(Home home, IntVar* ret,
740 const IntPropLevels&) const {
741 IntVar m = result(home,ret);
742 switch (t) {
743 case SNLE_CARD:
744 cardinality(home, e.post(home), m);
745 break;
746 case SNLE_MIN:
747 min(home, e.post(home), m);
748 break;
749 case SNLE_MAX:
750 max(home, e.post(home), m);
751 break;
752 default:
753 GECODE_NEVER;
754 break;
755 }
756 return m;
757 }
758 virtual void post(Home home, IntRelType irt, int c,
759 const IntPropLevels& ipls) const {
760 if (t==SNLE_CARD && irt!=IRT_NQ) {
761 switch (irt) {
762 case IRT_LQ:
763 cardinality(home, e.post(home),
764 0U,
765 static_cast<unsigned int>(c));
766 break;
767 case IRT_LE:
768 cardinality(home, e.post(home),
769 0U,
770 static_cast<unsigned int>(c-1));
771 break;
772 case IRT_GQ:
773 cardinality(home, e.post(home),
774 static_cast<unsigned int>(c),
775 Set::Limits::card);
776 break;
777 case IRT_GR:
778 cardinality(home, e.post(home),
779 static_cast<unsigned int>(c+1),
780 Set::Limits::card);
781 break;
782 case IRT_EQ:
783 cardinality(home, e.post(home),
784 static_cast<unsigned int>(c),
785 static_cast<unsigned int>(c));
786 break;
787 default:
788 GECODE_NEVER;
789 }
790 } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
791 c = (irt==IRT_GQ ? c : c+1);
792 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max);
793 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
794 c = (irt==IRT_LQ ? c : c-1);
795 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c);
796 } else {
797 rel(home, post(home,nullptr,ipls), irt, c);
798 }
799 }
800 virtual void post(Home home, IntRelType irt, int c,
801 BoolVar b,
802 const IntPropLevels& ipls) const {
803 if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
804 c = (irt==IRT_GQ ? c : c+1);
805 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b);
806 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
807 c = (irt==IRT_LQ ? c : c-1);
808 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b);
809 } else {
810 rel(home, post(home,nullptr,ipls), irt, c, b);
811 }
812 }
813 };
814 }
815
816 LinIntExpr
817 cardinality(const SetExpr& e) {
818 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
819 MiniModel::SetNonLinIntExpr::SNLE_CARD));
820 }
821 LinIntExpr
822 min(const SetExpr& e) {
823 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
824 MiniModel::SetNonLinIntExpr::SNLE_MIN));
825 }
826 LinIntExpr
827 max(const SetExpr& e) {
828 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
829 MiniModel::SetNonLinIntExpr::SNLE_MAX));
830 }
831
832 /*
833 * Posting set expressions
834 *
835 */
836 SetVar
837 expr(Home home, const SetExpr& e) {
838 PostInfo pi(home);
839 if (!home.failed())
840 return e.post(home);
841 SetVar x(home,IntSet::empty,IntSet::empty);
842 return x;
843 }
844
845}
846
847#endif
848
849// STATISTICS: minimodel-any