Generated on Wed Sep 5 2012 18:52:04 for Gecode by doxygen 1.8.1.1
bool-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, 2004
9  * Christian Schulte, 2004
10  *
11  * Last modified:
12  * $Date: 2012-02-22 16:04:20 +1100 (Wed, 22 Feb 2012) $ by $Author: tack $
13  * $Revision: 12537 $
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 namespace Gecode {
43 
44  /*
45  * Operations for nodes
46  *
47  */
48  bool
50  if (--use == 0) {
51  if ((l != NULL) && l->decrement())
52  delete l;
53  if ((r != NULL) && r->decrement())
54  delete r;
55  return true;
56  }
57  return false;
58  }
59 
60 
61  BoolExpr::BoolExpr(void) : n(new Node) {}
62 
63  BoolExpr::BoolExpr(const BoolVar& 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  n->m = NULL;
70  }
71 
73  : n(new Node) {
74  int ls = ((l.n->t == t) || (l.n->t == NT_VAR)) ? l.n->same : 1;
75  int rs = ((r.n->t == t) || (r.n->t == NT_VAR)) ? r.n->same : 1;
76  n->same = ls+rs;
77  n->t = t;
78  n->l = l.n;
79  n->l->use++;
80  n->r = r.n;
81  n->r->use++;
82  n->m = NULL;
83  }
84 
86  (void) t;
87  assert(t == NT_NOT);
88  if (l.n->t == NT_NOT) {
89  n = l.n->l;
90  n->use++;
91  } else {
92  n = new Node;
93  n->same = 1;
94  n->t = NT_NOT;
95  n->l = l.n;
96  n->l->use++;
97  n->r = NULL;
98  n->m = NULL;
99  }
100  }
101 
103  : n(new Node) {
104  n->same = 1;
105  n->t = NT_RLIN;
106  n->l = NULL;
107  n->r = NULL;
108  n->rl = rl;
109  n->m = NULL;
110  }
111 
112 #ifdef GECODE_HAS_SET_VARS
114  : n(new Node) {
115  n->same = 1;
116  n->t = NT_RSET;
117  n->l = NULL;
118  n->r = NULL;
119  n->rs = rs;
120  n->m = NULL;
121  }
122 
124  : n(new Node) {
125  n->same = 1;
126  n->t = NT_RSET;
127  n->l = NULL;
128  n->r = NULL;
129  n->rs = rs;
130  n->m = NULL;
131  }
132 #endif
133 
135  : n(new Node) {
136  n->same = 1;
137  n->t = NT_MISC;
138  n->l = NULL;
139  n->r = NULL;
140  n->m = m;
141  }
142 
143  const BoolExpr&
145  if (this != &e) {
146  if (n->decrement())
147  delete n;
148  n = e.n;
149  n->use++;
150  }
151  return *this;
152  }
153 
155 
157  if (n->decrement())
158  delete n;
159  }
160 
161  /*
162  * Operations for negation normalform
163  *
164  */
165  forceinline void
166  BoolExpr::NNF::operator delete(void*) {}
167 
168  forceinline void
169  BoolExpr::NNF::operator delete(void*, Region&) {}
170 
171  forceinline void*
172  BoolExpr::NNF::operator new(size_t s, Region& r) {
173  return r.ralloc(s);
174  }
175 
176  BoolVar
178  if ((t == NT_VAR) && !u.a.neg)
179  return u.a.x->x;
180  BoolVar b(home,0,1);
181  switch (t) {
182  case NT_VAR:
183  assert(u.a.neg);
184  Gecode::rel(home, u.a.x->x, IRT_NQ, b);
185  break;
186  case NT_RLIN:
187  u.a.x->rl.post(home, b, !u.a.neg, icl);
188  break;
189 #ifdef GECODE_HAS_SET_VARS
190  case NT_RSET:
191  u.a.x->rs.post(home, b, !u.a.neg);
192  break;
193 #endif
194  case NT_MISC:
195  u.a.x->m->post(home, b, !u.a.neg, icl);
196  break;
197  case NT_AND:
198  {
199  BoolVarArgs bp(p), bn(n);
200  int ip=0, in=0;
201  post(home, NT_AND, bp, bn, ip, in, icl);
202  clause(home, BOT_AND, bp, bn, b);
203  }
204  break;
205  case NT_OR:
206  {
207  BoolVarArgs bp(p), bn(n);
208  int ip=0, in=0;
209  post(home, NT_OR, bp, bn, ip, in, icl);
210  clause(home, BOT_OR, bp, bn, b);
211  }
212  break;
213  case NT_EQV:
214  {
215  bool n = false;
216  BoolVar l;
217  if (u.b.l->t == NT_VAR) {
218  l = u.b.l->u.a.x->x;
219  if (u.b.l->u.a.neg) n = !n;
220  } else {
221  l = u.b.l->expr(home,icl);
222  }
223  BoolVar r;
224  if (u.b.r->t == NT_VAR) {
225  r = u.b.r->u.a.x->x;
226  if (u.b.r->u.a.neg) n = !n;
227  } else {
228  r = u.b.r->expr(home,icl);
229  }
230  Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, icl);
231  }
232  break;
233  default:
234  GECODE_NEVER;
235  }
236  return b;
237  }
238 
239  void
241  BoolVarArgs& bp, BoolVarArgs& bn,
242  int& ip, int& in,
243  IntConLevel icl) const {
244  if (this->t != t) {
245  switch (this->t) {
246  case NT_VAR:
247  if (u.a.neg) {
248  bn[in++]=u.a.x->x;
249  } else {
250  bp[ip++]=u.a.x->x;
251  }
252  break;
253  case NT_RLIN:
254  {
255  BoolVar b(home,0,1);
256  u.a.x->rl.post(home, b, !u.a.neg, icl);
257  bp[ip++]=b;
258  }
259  break;
260 #ifdef GECODE_HAS_SET_VARS
261  case NT_RSET:
262  {
263  BoolVar b(home,0,1);
264  u.a.x->rs.post(home, b, !u.a.neg);
265  bp[ip++]=b;
266  }
267  break;
268 #endif
269  case NT_MISC:
270  {
271  BoolVar b(home,0,1);
272  u.a.x->m->post(home, b, !u.a.neg, icl);
273  bp[ip++]=b;
274  }
275  break;
276  default:
277  bp[ip++] = expr(home, icl);
278  break;
279  }
280  } else {
281  u.b.l->post(home, t, bp, bn, ip, in, icl);
282  u.b.r->post(home, t, bp, bn, ip, in, icl);
283  }
284  }
285 
286  void
288  switch (t) {
289  case NT_VAR:
290  Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
291  break;
292  case NT_RLIN:
293  u.a.x->rl.post(home, !u.a.neg, icl);
294  break;
295 #ifdef GECODE_HAS_SET_VARS
296  case NT_RSET:
297  u.a.x->rs.post(home, !u.a.neg);
298  break;
299 #endif
300  case NT_MISC:
301  {
302  BoolVar b(home,!u.a.neg,!u.a.neg);
303  u.a.x->m->post(home, b, false, icl);
304  }
305  break;
306  case NT_AND:
307  u.b.l->rel(home, icl);
308  u.b.r->rel(home, icl);
309  break;
310  case NT_OR:
311  {
312  BoolVarArgs bp(p), bn(n);
313  int ip=0, in=0;
314  post(home, NT_OR, bp, bn, ip, in, icl);
315  clause(home, BOT_OR, bp, bn, 1);
316  }
317  break;
318  case NT_EQV:
319  if (u.b.l->t==NT_VAR && u.b.r->t==NT_RLIN) {
320  u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
321  u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
322  } else if (u.b.r->t==NT_VAR && u.b.l->t==NT_RLIN) {
323  u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
324  u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
325  } else if (u.b.l->t==NT_RLIN) {
326  u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,icl),
327  !u.b.l->u.a.neg,icl);
328  } else if (u.b.r->t==NT_RLIN) {
329  u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,icl),
330  !u.b.r->u.a.neg,icl);
331 #ifdef GECODE_HAS_SET_VARS
332  } else if (u.b.l->t==NT_VAR && u.b.r->t==NT_RSET) {
333  u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
334  u.b.l->u.a.neg==u.b.r->u.a.neg);
335  } else if (u.b.r->t==NT_VAR && u.b.l->t==NT_RSET) {
336  u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
337  u.b.l->u.a.neg==u.b.r->u.a.neg);
338  } else if (u.b.l->t==NT_RSET) {
339  u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,icl),
340  !u.b.l->u.a.neg);
341  } else if (u.b.r->t==NT_RSET) {
342  u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,icl),
343  !u.b.r->u.a.neg);
344 #endif
345  } else {
346  Gecode::rel(home, expr(home, icl), IRT_EQ, 1);
347  }
348  break;
349  default:
350  GECODE_NEVER;
351  }
352  }
353 
356  switch (n->t) {
357  case NT_VAR: case NT_RLIN: case NT_MISC:
358 #ifdef GECODE_HAS_SET_VARS
359  case NT_RSET:
360 #endif
361  {
362  NNF* x = new (r) NNF;
363  x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
364  if (neg) {
365  x->p = 0; x->n = 1;
366  } else {
367  x->p = 1; x->n = 0;
368  }
369  return x;
370  }
371  case NT_NOT:
372  return nnf(r,n->l,!neg);
373  case NT_AND: case NT_OR:
374  {
375  NodeType t = ((n->t == NT_AND) == neg) ? NT_OR : NT_AND;
376  NNF* x = new (r) NNF;
377  x->t = t;
378  x->u.b.l = nnf(r,n->l,neg);
379  x->u.b.r = nnf(r,n->r,neg);
380  int p_l, n_l;
381  if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) {
382  p_l=x->u.b.l->p; n_l=x->u.b.l->n;
383  } else {
384  p_l=1; n_l=0;
385  }
386  int p_r, n_r;
387  if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) {
388  p_r=x->u.b.r->p; n_r=x->u.b.r->n;
389  } else {
390  p_r=1; n_r=0;
391  }
392  x->p = p_l+p_r;
393  x->n = n_l+n_r;
394  return x;
395  }
396  case NT_EQV:
397  {
398  NNF* x = new (r) NNF;
399  x->t = NT_EQV;
400  x->u.b.l = nnf(r,n->l,neg);
401  x->u.b.r = nnf(r,n->r,false);
402  x->p = 2; x->n = 0;
403  return x;
404  }
405  default:
406  GECODE_NEVER;
407  }
408  GECODE_NEVER;
409  return NULL;
410  }
411 
412 
413  BoolExpr
414  operator &&(const BoolExpr& l, const BoolExpr& r) {
415  return BoolExpr(l,BoolExpr::NT_AND,r);
416  }
417  BoolExpr
418  operator ||(const BoolExpr& l, const BoolExpr& r) {
419  return BoolExpr(l,BoolExpr::NT_OR,r);
420  }
421  BoolExpr
422  operator ^(const BoolExpr& l, const BoolExpr& r) {
424  }
425 
426  BoolExpr
427  operator !(const BoolExpr& e) {
428  return BoolExpr(e,BoolExpr::NT_NOT);
429  }
430 
431  BoolExpr
432  operator !=(const BoolExpr& l, const BoolExpr& r) {
433  return !BoolExpr(l, BoolExpr::NT_EQV, r);
434  }
435  BoolExpr
436  operator ==(const BoolExpr& l, const BoolExpr& r) {
437  return BoolExpr(l, BoolExpr::NT_EQV, r);
438  }
439  BoolExpr
440  operator >>(const BoolExpr& l, const BoolExpr& r) {
442  BoolExpr::NT_OR,r);
443  }
444  BoolExpr
445  operator <<(const BoolExpr& l, const BoolExpr& r) {
447  BoolExpr::NT_OR,l);
448  }
449  /*
450  * Posting Boolean expressions and relations
451  *
452  */
453  BoolVar
454  expr(Home home, const BoolExpr& e, IntConLevel icl) {
455  if (!home.failed())
456  return e.expr(home,icl);
457  BoolVar x(home,0,1);
458  return x;
459  }
460 
461  void
462  rel(Home home, const BoolExpr& e, IntConLevel icl) {
463  if (home.failed()) return;
464  e.rel(home,icl);
465  }
466 
467  /*
468  * Boolean element constraints
469  *
470  */
471 
474  public:
478  int n;
482  BElementExpr(int size);
484  virtual ~BElementExpr(void);
486  virtual void post(Space& home, BoolVar b, bool neg, IntConLevel icl);
487  };
488 
490  : a(heap.alloc<BoolExpr>(size)), n(size) {}
491 
493  heap.free<BoolExpr>(a,n);
494  }
495 
496  void
498  IntVar z = idx.post(home, icl);
499  if (z.assigned() && z.val() >= 0 && z.val() < n) {
500  BoolExpr be = pos ? (a[z.val()] == b) : (a[z.val()] == !b);
501  be.rel(home,icl);
502  } else {
503  BoolVarArgs x(n);
504  for (int i=n; i--;)
505  x[i] = a[i].expr(home,icl);
506  BoolVar res = pos ? b : (!b).expr(home,icl);
507  element(home, x, z, res, icl);
508  }
509  }
510 
511  BoolExpr
512  element(const BoolVarArgs& b, const LinExpr& idx) {
513  BElementExpr* be = new BElementExpr(b.size());
514  for (int i=b.size(); i--;)
515  new (&be->a[i]) BoolExpr(b[i]);
516  be->idx = idx;
517  return BoolExpr(be);
518  }
519 
520 }
521 
522 // STATISTICS: minimodel-any