Generated on Thu Feb 21 2013 23:11:48 for Gecode by doxygen 1.8.3.1
set-expr.cpp
Go to the documentation of this file.
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  * Last modified:
12  * $Date: 2011-01-22 02:01:14 +1100 (Sat, 22 Jan 2011) $ by $Author: schulte $
13  * $Revision: 11553 $
14  *
15  * This file is part of Gecode, the generic constraint
16  * development environment:
17  * http://www.gecode.org
18  *
19  * Permission is hereby granted, free of charge, to any person obtaining
20  * a copy of this software and associated documentation files (the
21  * "Software"), to deal in the Software without restriction, including
22  * without limitation the rights to use, copy, modify, merge, publish,
23  * distribute, sublicense, and/or sell copies of the Software, and to
24  * permit persons to whom the Software is furnished to do so, subject to
25  * the following conditions:
26  *
27  * The above copyright notice and this permission notice shall be
28  * included in all copies or substantial portions of the Software.
29  *
30  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
31  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
32  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
33  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
34  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
35  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
36  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
37  *
38  */
39 
40 #include <gecode/minimodel.hh>
41 
42 #ifdef GECODE_HAS_SET_VARS
43 
44 namespace Gecode {
45 
46  /*
47  * Operations for nodes
48  *
49  */
50  bool
52  if (--use == 0) {
53  if ((l != NULL) && l->decrement())
54  delete l;
55  if ((r != NULL) && r->decrement())
56  delete r;
57  return true;
58  }
59  return false;
60  }
61 
62 
63  SetExpr::SetExpr(const SetVar& x) : n(new Node) {
64  n->same = 1;
65  n->t = NT_VAR;
66  n->l = NULL;
67  n->r = NULL;
68  n->x = x;
69  }
70 
71  SetExpr::SetExpr(const IntSet& s) : n(new Node) {
72  n->same = 1;
73  n->t = NT_CONST;
74  n->l = NULL;
75  n->r = NULL;
76  n->s = s;
77  }
78 
79  SetExpr::SetExpr(const LinExpr& e) : n(new Node) {
80  n->same = 1;
81  n->t = NT_LEXP;
82  n->l = NULL;
83  n->r = NULL;
84  n->e = e;
85  }
86 
87  SetExpr::SetExpr(const SetExpr& l, NodeType t, const SetExpr& r)
88  : n(new Node) {
89  int ls = same(t,l.n->t) ? l.n->same : 1;
90  int rs = same(t,r.n->t) ? r.n->same : 1;
91  n->same = ls+rs;
92  n->t = t;
93  n->l = l.n;
94  n->l->use++;
95  n->r = r.n;
96  n->r->use++;
97  }
98 
100  (void) t;
101  assert(t == NT_CMPL);
102  if (l.n->t == NT_CMPL) {
103  n = l.n->l;
104  n->use++;
105  } else {
106  n = new Node;
107  n->same = 1;
108  n->t = NT_CMPL;
109  n->l = l.n;
110  n->l->use++;
111  n->r = NULL;
112  }
113  }
114 
115  const SetExpr&
117  if (this != &e) {
118  if (n != NULL && n->decrement())
119  delete n;
120  n = e.n;
121  n->use++;
122  }
123  return *this;
124  }
125 
127  if (n != NULL && n->decrement())
128  delete n;
129  }
130 
131  /*
132  * Operations for negation normalform
133  *
134  */
135  forceinline void
136  SetExpr::NNF::operator delete(void*) {}
137 
138  forceinline void
139  SetExpr::NNF::operator delete(void*, Region&) {}
140 
141  forceinline void*
142  SetExpr::NNF::operator new(size_t s, Region& r) {
143  return r.ralloc(s);
144  }
145 
146  void
147  SetExpr::NNF::post(Home home, SetRelType srt, SetVar s) const {
148  switch (t) {
149  case NT_VAR:
150  if (neg) {
151  switch (srt) {
152  case SRT_EQ:
153  rel(home, u.a.x->x, SRT_CMPL, s);
154  break;
155  case SRT_CMPL:
156  rel(home, u.a.x->x, SRT_EQ, s);
157  break;
158  default:
159  SetVar bc(home,IntSet::empty,
161  rel(home, s, SRT_CMPL, bc);
162  rel(home, u.a.x->x, srt, bc);
163  break;
164  }
165  } else
166  rel(home, u.a.x->x, srt, s);
167  break;
168  case NT_CONST:
169  {
170  IntSet ss;
171  if (neg) {
172  IntSetRanges sr(u.a.x->s);
174  ss = IntSet(src);
175  } else {
176  ss = u.a.x->s;
177  }
178  switch (srt) {
179  case SRT_SUB: srt = SRT_SUP; break;
180  case SRT_SUP: srt = SRT_SUB; break;
181  default: break;
182  }
183  dom(home, s, srt, ss);
184  }
185  break;
186  case NT_LEXP:
187  {
188  IntVar iv = u.a.x->e.post(home,ICL_DEF);
189  if (neg) {
190  SetVar ic(home,IntSet::empty,
192  rel(home, iv, SRT_CMPL, ic);
193  rel(home,ic,srt,s);
194  } else {
195  rel(home,iv,srt,s);
196  }
197  }
198  break;
199  case NT_INTER:
200  {
201  SetVarArgs bs(p+n);
202  int i=0;
203  post(home, NT_INTER, bs, i);
204  if (i == 2) {
205  rel(home, bs[0], SOT_INTER, bs[1], srt, s);
206  } else {
207  if (srt == SRT_EQ)
208  rel(home, SOT_INTER, bs, s);
209  else {
210  SetVar bc(home,IntSet::empty,
212  rel(home, SOT_INTER, bs, bc);
213  rel(home, bc, srt, s);
214  }
215  }
216  }
217  break;
218  case NT_UNION:
219  {
220  SetVarArgs bs(p+n);
221  int i=0;
222  post(home, NT_UNION, bs, i);
223  if (i == 2) {
224  rel(home, bs[0], SOT_UNION, bs[1], srt, s);
225  } else {
226  if (srt == SRT_EQ)
227  rel(home, SOT_UNION, bs, s);
228  else {
229  SetVar bc(home,IntSet::empty,
231  rel(home, SOT_UNION, bs, bc);
232  rel(home, bc, srt, s);
233  }
234  }
235  }
236  break;
237  case NT_DUNION:
238  {
239  SetVarArgs bs(p+n);
240  int i=0;
241  post(home, NT_DUNION, bs, i);
242 
243  if (i == 2) {
244  if (neg) {
245  if (srt == SRT_CMPL) {
246  rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
247  } else {
248  SetVar bc(home,IntSet::empty,
250  rel(home,s,SRT_CMPL,bc);
251  rel(home, bs[0], SOT_DUNION, bs[1], srt, bc);
252  }
253  } else {
254  rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
255  }
256  } else {
257  if (neg) {
258  if (srt == SRT_CMPL) {
259  rel(home, SOT_DUNION, bs, s);
260  } else {
261  SetVar br(home,IntSet::empty,
263  rel(home, SOT_DUNION, bs, br);
264  if (srt == SRT_EQ)
265  rel(home, br, SRT_CMPL, s);
266  else {
267  SetVar bc(home,IntSet::empty,
269  rel(home, br, srt, bc);
270  rel(home, bc, SRT_CMPL, s);
271  }
272  }
273  } else {
274  if (srt == SRT_EQ)
275  rel(home, SOT_DUNION, bs, s);
276  else {
277  SetVar br(home,IntSet::empty,
279  rel(home, SOT_DUNION, bs, br);
280  rel(home, br, srt, s);
281  }
282  }
283  }
284  }
285  break;
286  default:
287  GECODE_NEVER;
288  }
289  }
290 
291  void
293  switch (t) {
294  case NT_VAR:
295  if (neg) {
296  switch (srt) {
297  case SRT_EQ:
298  rel(home, u.a.x->x, SRT_CMPL, s, b);
299  break;
300  case SRT_CMPL:
301  rel(home, u.a.x->x, SRT_EQ, s, b);
302  break;
303  default:
304  SetVar bc(home,IntSet::empty,
306  rel(home, s, SRT_CMPL, bc);
307  rel(home, u.a.x->x, srt, bc, b);
308  break;
309  }
310  } else
311  rel(home, u.a.x->x, srt, s, b);
312  break;
313  case NT_CONST:
314  {
315  IntSet ss;
316  if (neg) {
317  IntSetRanges sr(u.a.x->s);
319  ss = IntSet(src);
320  } else {
321  ss = u.a.x->s;
322  }
323  dom(home, s, srt, ss, b);
324  }
325  break;
326  case NT_LEXP:
327  {
328  IntVar iv = u.a.x->e.post(home,ICL_DEF);
329  if (neg) {
330  SetVar ic(home,IntSet::empty,
332  rel(home, iv, SRT_CMPL, ic);
333  rel(home,ic,srt,s,b);
334  } else {
335  rel(home,iv,srt,s,b);
336  }
337  }
338  case NT_INTER:
339  {
340  SetVarArgs bs(p+n);
341  int i=0;
342  post(home, NT_INTER, bs, i);
343  SetVar br(home,IntSet::empty,
345  rel(home, SOT_INTER, bs, br);
346  rel(home, br, srt, s, b);
347  }
348  break;
349  case NT_UNION:
350  {
351  SetVarArgs bs(p+n);
352  int i=0;
353  post(home, NT_UNION, bs, i);
354  SetVar br(home,IntSet::empty,
356  rel(home, SOT_UNION, bs, br);
357  rel(home, br, srt, s, b);
358  }
359  break;
360  case NT_DUNION:
361  {
362  SetVarArgs bs(p+n);
363  int i=0;
364  post(home, NT_DUNION, bs, i);
365 
366  if (neg) {
367  SetVar br(home,IntSet::empty,
369  rel(home, SOT_DUNION, bs, br);
370  if (srt == SRT_CMPL)
371  rel(home, br, SRT_EQ, s, b);
372  else if (srt == SRT_EQ)
373  rel(home, br, SRT_CMPL, s, b);
374  else {
375  SetVar bc(home,IntSet::empty,
377  rel(home, br, srt, bc);
378  rel(home, bc, SRT_CMPL, s, b);
379  }
380  } else {
381  SetVar br(home,IntSet::empty,
383  rel(home, SOT_DUNION, bs, br);
384  rel(home, br, srt, s, b);
385  }
386  }
387  break;
388  default:
389  GECODE_NEVER;
390  }
391  }
392 
393  void
395  SetVarArgs& b, int& i) const {
396  if (this->t != t) {
397  switch (this->t) {
398  case NT_VAR:
399  if (neg) {
400  SetVar xc(home,IntSet::empty,
402  rel(home, xc, SRT_CMPL, u.a.x->x);
403  b[i++]=xc;
404  } else {
405  b[i++]=u.a.x->x;
406  }
407  break;
408  default:
409  {
410  SetVar s(home,IntSet::empty,
412  post(home,SRT_EQ,s);
413  b[i++] = s;
414  }
415  break;
416  }
417  } else {
418  u.b.l->post(home, t, b, i);
419  u.b.r->post(home, t, b, i);
420  }
421  }
422 
423  void
424  SetExpr::NNF::post(Home home, SetRelType srt, const NNF* n) const {
425  if (n->t == NT_VAR && !n->neg) {
426  post(home,srt,n->u.a.x->x);
427  } else if (t == NT_VAR && !neg) {
428  SetRelType n_srt;
429  switch (srt) {
430  case SRT_SUB: n_srt = SRT_SUP; break;
431  case SRT_SUP: n_srt = SRT_SUB; break;
432  default: n_srt = srt;
433  }
434  n->post(home,n_srt,this);
435  } else {
436  SetVar nx(home,IntSet::empty,
438  n->post(home,SRT_EQ,nx);
439  post(home,srt,nx);
440  }
441  }
442 
443  void
445  SetRelType srt, const NNF* n) const {
446  if (t) {
447  if (n->t == NT_VAR && !n->neg) {
448  post(home,srt,n->u.a.x->x,b);
449  } else if (t == NT_VAR && !neg) {
450  SetRelType n_srt;
451  switch (srt) {
452  case SRT_SUB: n_srt = SRT_SUP; break;
453  case SRT_SUP: n_srt = SRT_SUB; break;
454  default: n_srt = srt;
455  }
456  n->post(home,b,true,n_srt,this);
457  } else {
458  SetVar nx(home,IntSet::empty,
460  n->post(home,SRT_EQ,nx);
461  post(home,srt,nx,b);
462  }
463  } else if (srt == SRT_EQ) {
464  post(home,b,true,SRT_NQ,n);
465  } else if (srt == SRT_NQ) {
466  post(home,b,true,SRT_EQ,n);
467  } else {
468  BoolVar nb(home,0,1);
469  rel(home,b,IRT_NQ,nb);
470  post(home,nb,true,srt,n);
471  }
472  }
473 
474  SetExpr::NNF*
476  switch (n->t) {
477  case NT_VAR: case NT_CONST: case NT_LEXP:
478  {
479  NNF* x = new (r) NNF;
480  x->t = n->t; x->neg = neg; x->u.a.x = n;
481  if (neg) {
482  x->p = 0; x->n = 1;
483  } else {
484  x->p = 1; x->n = 0;
485  }
486  return x;
487  }
488  case NT_CMPL:
489  return nnf(r,n->l,!neg);
490  case NT_INTER: case NT_UNION: case NT_DUNION:
491  {
492  NodeType t; bool xneg;
493  if (n->t == NT_DUNION) {
494  t = n->t; xneg = neg; neg = false;
495  } else {
496  t = ((n->t == NT_INTER) == neg) ? NT_UNION : NT_INTER;
497  xneg = false;
498  }
499  NNF* x = new (r) NNF;
500  x->neg = xneg;
501  x->t = t;
502  x->u.b.l = nnf(r,n->l,neg);
503  x->u.b.r = nnf(r,n->r,neg);
504  int p_l, n_l;
505  if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) {
506  p_l=x->u.b.l->p; n_l=x->u.b.l->n;
507  } else {
508  p_l=1; n_l=0;
509  }
510  int p_r, n_r;
511  if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) {
512  p_r=x->u.b.r->p; n_r=x->u.b.r->n;
513  } else {
514  p_r=1; n_r=0;
515  }
516  x->p = p_l+p_r;
517  x->n = n_l+n_r;
518  return x;
519  }
520  default:
521  GECODE_NEVER;
522  }
523  GECODE_NEVER;
524  return NULL;
525  }
526 
527 
528  SetExpr
529  operator &(const SetExpr& l, const SetExpr& r) {
530  return SetExpr(l,SetExpr::NT_INTER,r);
531  }
532  SetExpr
533  operator |(const SetExpr& l, const SetExpr& r) {
534  return SetExpr(l,SetExpr::NT_UNION,r);
535  }
536  SetExpr
537  operator +(const SetExpr& l, const SetExpr& r) {
538  return SetExpr(l,SetExpr::NT_DUNION,r);
539  }
540  SetExpr
541  operator -(const SetExpr& e) {
542  return SetExpr(e,SetExpr::NT_CMPL);
543  }
544  SetExpr
545  operator -(const SetExpr& l, const SetExpr& r) {
546  return SetExpr(l,SetExpr::NT_INTER,-r);
547  }
548  SetExpr
549  singleton(const LinExpr& e) {
550  return SetExpr(e);
551  }
552 
553  SetExpr
554  inter(const SetVarArgs& x) {
555  if (x.size() == 0)
557  SetExpr r(x[0]);
558  for (int i=1; i<x.size(); i++)
559  r = (r & x[i]);
560  return r;
561  }
562  SetExpr
563  setunion(const SetVarArgs& x) {
564  if (x.size() == 0)
565  return SetExpr(IntSet::empty);
566  SetExpr r(x[0]);
567  for (int i=1; i<x.size(); i++)
568  r = (r | x[i]);
569  return r;
570  }
571  SetExpr
572  setdunion(const SetVarArgs& x) {
573  if (x.size() == 0)
574  return SetExpr(IntSet::empty);
575  SetExpr r(x[0]);
576  for (int i=1; i<x.size(); i++)
577  r = (r + x[i]);
578  return r;
579  }
580 
581  namespace MiniModel {
584  public:
589  SNLE_MAX
590  } t;
595  : t(t0), e(e0) {}
597  virtual IntVar post(Home home, IntVar* ret, IntConLevel) const {
598  IntVar m = result(home,ret);
599  switch (t) {
600  case SNLE_CARD:
601  cardinality(home, e.post(home), m);
602  break;
603  case SNLE_MIN:
604  min(home, e.post(home), m);
605  break;
606  case SNLE_MAX:
607  max(home, e.post(home), m);
608  break;
609  default:
610  GECODE_NEVER;
611  break;
612  }
613  return m;
614  }
615  virtual void post(Home home, IntRelType irt, int c,
616  IntConLevel icl) const {
617  if (t==SNLE_CARD && irt!=IRT_NQ) {
618  switch (irt) {
619  case IRT_LQ:
620  cardinality(home, e.post(home),
621  0U,
622  static_cast<unsigned int>(c));
623  break;
624  case IRT_LE:
625  cardinality(home, e.post(home),
626  0U,
627  static_cast<unsigned int>(c-1));
628  break;
629  case IRT_GQ:
630  cardinality(home, e.post(home),
631  static_cast<unsigned int>(c),
633  break;
634  case IRT_GR:
635  cardinality(home, e.post(home),
636  static_cast<unsigned int>(c+1),
638  break;
639  case IRT_EQ:
640  cardinality(home, e.post(home),
641  static_cast<unsigned int>(c),
642  static_cast<unsigned int>(c));
643  break;
644  default:
645  GECODE_NEVER;
646  }
647  } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
648  c = (irt==IRT_GQ ? c : c+1);
649  dom(home, e.post(home), SRT_SUB, c, Set::Limits::max);
650  } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
651  c = (irt==IRT_LQ ? c : c-1);
652  dom(home, e.post(home), SRT_SUB, Set::Limits::min, c);
653  } else {
654  rel(home, post(home,NULL,icl), irt, c);
655  }
656  }
657  virtual void post(Home home, IntRelType irt, int c,
658  BoolVar b, IntConLevel icl) const {
659  if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
660  c = (irt==IRT_GQ ? c : c+1);
661  dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b);
662  } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
663  c = (irt==IRT_LQ ? c : c-1);
664  dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b);
665  } else {
666  rel(home, post(home,NULL,icl), irt, c, b);
667  }
668  }
669  };
670  }
671 
672  LinExpr
673  cardinality(const SetExpr& e) {
674  return LinExpr(new MiniModel::SetNonLinExpr(e,
676  }
677  LinExpr
678  min(const SetExpr& e) {
679  return LinExpr(new MiniModel::SetNonLinExpr(e,
681  }
682  LinExpr
683  max(const SetExpr& e) {
684  return LinExpr(new MiniModel::SetNonLinExpr(e,
686  }
687 
688  /*
689  * Posting set expressions
690  *
691  */
692  SetVar
693  expr(Home home, const SetExpr& e) {
694  if (!home.failed())
695  return e.post(home);
697  return x;
698  }
699 
700 }
701 
702 #endif
703 
704 // STATISTICS: minimodel-any