Generated on Sat May 25 2013 18:00:40 for Gecode by doxygen 1.8.3.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  * Vincent Barichard <Vincent.Barichard@univ-angers.fr>
7  *
8  * Copyright:
9  * Guido Tack, 2004
10  * Christian Schulte, 2004
11  * Vincent Barichard, 2012
12  *
13  * Last modified:
14  * $Date: 2013-01-22 13:48:12 +0100 (Tue, 22 Jan 2013) $ by $Author: schulte $
15  * $Revision: 13227 $
16  *
17  * This file is part of Gecode, the generic constraint
18  * development environment:
19  * http://www.gecode.org
20  *
21  * Permission is hereby granted, free of charge, to any person obtaining
22  * a copy of this software and associated documentation files (the
23  * "Software"), to deal in the Software without restriction, including
24  * without limitation the rights to use, copy, modify, merge, publish,
25  * distribute, sublicense, and/or sell copies of the Software, and to
26  * permit persons to whom the Software is furnished to do so, subject to
27  * the following conditions:
28  *
29  * The above copyright notice and this permission notice shall be
30  * included in all copies or substantial portions of the Software.
31  *
32  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
33  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
34  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
36  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
37  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
38  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
39  *
40  */
41 
42 #include <gecode/minimodel.hh>
43 
44 namespace Gecode {
45 
48  public:
50  unsigned int use;
52  int same;
56  Node *l, *r;
61 #ifdef GECODE_HAS_FLOAT_VARS
62 
64 #endif
65 #ifdef GECODE_HAS_SET_VARS
66 
68 #endif
69 
71 
73  Node(void);
75  ~Node(void);
78  bool decrement(void);
80  static void* operator new(size_t size);
82  static void operator delete(void* p, size_t size);
83  };
84 
85 
86  /*
87  * Operations for nodes
88  *
89  */
90  BoolExpr::Node::Node(void) : use(1), m(NULL) {}
91 
92  BoolExpr::Node::~Node(void) { delete m; }
93 
94  void*
95  BoolExpr::Node::operator new(size_t size) {
96  return heap.ralloc(size);
97  }
98  void
99  BoolExpr::Node::operator delete(void* p, size_t) {
100  heap.rfree(p);
101  }
102 
103  bool
105  if (--use == 0) {
106  if ((l != NULL) && l->decrement())
107  delete l;
108  if ((r != NULL) && r->decrement())
109  delete r;
110  return true;
111  }
112  return false;
113  }
114 
115  BoolExpr::BoolExpr(void) : n(new Node) {}
116 
117  BoolExpr::BoolExpr(const BoolExpr& e) : n(e.n) {
118  n->use++;
119  }
120 
121  BoolExpr::BoolExpr(const BoolVar& x) : n(new Node) {
122  n->same = 1;
123  n->t = NT_VAR;
124  n->l = NULL;
125  n->r = NULL;
126  n->x = x;
127  }
128 
130  : n(new Node) {
131  int ls = ((l.n->t == t) || (l.n->t == NT_VAR)) ? l.n->same : 1;
132  int rs = ((r.n->t == t) || (r.n->t == NT_VAR)) ? r.n->same : 1;
133  n->same = ls+rs;
134  n->t = t;
135  n->l = l.n;
136  n->l->use++;
137  n->r = r.n;
138  n->r->use++;
139  }
140 
142  (void) t;
143  assert(t == NT_NOT);
144  if (l.n->t == NT_NOT) {
145  n = l.n->l;
146  n->use++;
147  } else {
148  n = new Node;
149  n->same = 1;
150  n->t = NT_NOT;
151  n->l = l.n;
152  n->l->use++;
153  n->r = NULL;
154  }
155  }
156 
158  : n(new Node) {
159  n->same = 1;
160  n->t = NT_RLIN;
161  n->l = NULL;
162  n->r = NULL;
163  n->rl = rl;
164  }
165 
166 #ifdef GECODE_HAS_FLOAT_VARS
168  : n(new Node) {
169  n->same = 1;
170  n->t = NT_RLINFLOAT;
171  n->l = NULL;
172  n->r = NULL;
173  n->rfl = rfl;
174  }
175 #endif
176 
177 #ifdef GECODE_HAS_SET_VARS
179  : n(new Node) {
180  n->same = 1;
181  n->t = NT_RSET;
182  n->l = NULL;
183  n->r = NULL;
184  n->rs = rs;
185  }
186 
188  : n(new Node) {
189  n->same = 1;
190  n->t = NT_RSET;
191  n->l = NULL;
192  n->r = NULL;
193  n->rs = rs;
194  }
195 #endif
196 
198  : n(new Node) {
199  n->same = 1;
200  n->t = NT_MISC;
201  n->l = NULL;
202  n->r = NULL;
203  n->m = m;
204  }
205 
206  const BoolExpr&
208  if (this != &e) {
209  if (n->decrement())
210  delete n;
211  n = e.n;
212  n->use++;
213  }
214  return *this;
215  }
216 
218 
220  if (n->decrement())
221  delete n;
222  }
223 
224  namespace {
226  class NNF {
227  public:
229  typedef BoolExpr::Node Node;
233  int p;
235  int n;
237  union {
239  struct {
241  NNF* l;
243  NNF* r;
244  } b;
246  struct {
248  bool neg;
250  Node* x;
251  } a;
252  } u;
255  static NNF* nnf(Region& r, Node* n, bool neg);
258  void post(Home home, NodeType t,
259  BoolVarArgs& bp, BoolVarArgs& bn,
260  int& ip, int& in,
261  IntConLevel icl) const;
264  BoolVar expr(Home home, IntConLevel icl) const;
267  void rel(Home home, IntConLevel icl) const;
269  static void* operator new(size_t s, Region& r);
271  static void operator delete(void*);
273  static void operator delete(void*, Region&);
274  };
275 
276  /*
277  * Operations for negation normalform
278  *
279  */
280  forceinline void
281  NNF::operator delete(void*) {}
282 
283  forceinline void
284  NNF::operator delete(void*, Region&) {}
285 
286  forceinline void*
287  NNF::operator new(size_t s, Region& r) {
288  return r.ralloc(s);
289  }
290 
291  BoolVar
292  NNF::expr(Home home, IntConLevel icl) const {
293  if ((t == BoolExpr::NT_VAR) && !u.a.neg)
294  return u.a.x->x;
295  BoolVar b(home,0,1);
296  switch (t) {
297  case BoolExpr::NT_VAR:
298  assert(u.a.neg);
299  Gecode::rel(home, u.a.x->x, IRT_NQ, b);
300  break;
301  case BoolExpr::NT_RLIN:
302  u.a.x->rl.post(home, b, !u.a.neg, icl);
303  break;
304 #ifdef GECODE_HAS_FLOAT_VARS
306  u.a.x->rfl.post(home, b, !u.a.neg);
307  break;
308 #endif
309 #ifdef GECODE_HAS_SET_VARS
310  case BoolExpr::NT_RSET:
311  u.a.x->rs.post(home, b, !u.a.neg);
312  break;
313 #endif
314  case BoolExpr::NT_MISC:
315  u.a.x->m->post(home, b, !u.a.neg, icl);
316  break;
317  case BoolExpr::NT_AND:
318  {
319  BoolVarArgs bp(p), bn(n);
320  int ip=0, in=0;
321  post(home, BoolExpr::NT_AND, bp, bn, ip, in, icl);
322  clause(home, BOT_AND, bp, bn, b);
323  }
324  break;
325  case BoolExpr::NT_OR:
326  {
327  BoolVarArgs bp(p), bn(n);
328  int ip=0, in=0;
329  post(home, BoolExpr::NT_OR, bp, bn, ip, in, icl);
330  clause(home, BOT_OR, bp, bn, b);
331  }
332  break;
333  case BoolExpr::NT_EQV:
334  {
335  bool n = false;
336  BoolVar l;
337  if (u.b.l->t == BoolExpr::NT_VAR) {
338  l = u.b.l->u.a.x->x;
339  if (u.b.l->u.a.neg) n = !n;
340  } else {
341  l = u.b.l->expr(home,icl);
342  }
343  BoolVar r;
344  if (u.b.r->t == BoolExpr::NT_VAR) {
345  r = u.b.r->u.a.x->x;
346  if (u.b.r->u.a.neg) n = !n;
347  } else {
348  r = u.b.r->expr(home,icl);
349  }
350  Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, icl);
351  }
352  break;
353  default:
354  GECODE_NEVER;
355  }
356  return b;
357  }
358 
359  void
360  NNF::post(Home home, NodeType t,
361  BoolVarArgs& bp, BoolVarArgs& bn,
362  int& ip, int& in,
363  IntConLevel icl) const {
364  if (this->t != t) {
365  switch (this->t) {
366  case BoolExpr::NT_VAR:
367  if (u.a.neg) {
368  bn[in++]=u.a.x->x;
369  } else {
370  bp[ip++]=u.a.x->x;
371  }
372  break;
373  case BoolExpr::NT_RLIN:
374  {
375  BoolVar b(home,0,1);
376  u.a.x->rl.post(home, b, !u.a.neg, icl);
377  bp[ip++]=b;
378  }
379  break;
380 #ifdef GECODE_HAS_FLOAT_VARS
382  {
383  BoolVar b(home,0,1);
384  u.a.x->rfl.post(home, b, !u.a.neg);
385  bp[ip++]=b;
386  }
387  break;
388 #endif
389 #ifdef GECODE_HAS_SET_VARS
390  case BoolExpr::NT_RSET:
391  {
392  BoolVar b(home,0,1);
393  u.a.x->rs.post(home, b, !u.a.neg);
394  bp[ip++]=b;
395  }
396  break;
397 #endif
398  case BoolExpr::NT_MISC:
399  {
400  BoolVar b(home,0,1);
401  u.a.x->m->post(home, b, !u.a.neg, icl);
402  bp[ip++]=b;
403  }
404  break;
405  default:
406  bp[ip++] = expr(home, icl);
407  break;
408  }
409  } else {
410  u.b.l->post(home, t, bp, bn, ip, in, icl);
411  u.b.r->post(home, t, bp, bn, ip, in, icl);
412  }
413  }
414 
415  void
416  NNF::rel(Home home, IntConLevel icl) const {
417  switch (t) {
418  case BoolExpr::NT_VAR:
419  Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
420  break;
421  case BoolExpr::NT_RLIN:
422  u.a.x->rl.post(home, !u.a.neg, icl);
423  break;
424 #ifdef GECODE_HAS_FLOAT_VARS
426  u.a.x->rfl.post(home, !u.a.neg);
427  break;
428 #endif
429 #ifdef GECODE_HAS_SET_VARS
430  case BoolExpr::NT_RSET:
431  u.a.x->rs.post(home, !u.a.neg);
432  break;
433 #endif
434  case BoolExpr::NT_MISC:
435  {
436  BoolVar b(home,!u.a.neg,!u.a.neg);
437  u.a.x->m->post(home, b, false, icl);
438  }
439  break;
440  case BoolExpr::NT_AND:
441  u.b.l->rel(home, icl);
442  u.b.r->rel(home, icl);
443  break;
444  case BoolExpr::NT_OR:
445  {
446  BoolVarArgs bp(p), bn(n);
447  int ip=0, in=0;
448  post(home, BoolExpr::NT_OR, bp, bn, ip, in, icl);
449  clause(home, BOT_OR, bp, bn, 1);
450  }
451  break;
452  case BoolExpr::NT_EQV:
453  if (u.b.l->t==BoolExpr::NT_VAR &&
454  u.b.r->t==BoolExpr::NT_RLIN) {
455  u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
456  u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
457  } else if (u.b.r->t==BoolExpr::NT_VAR &&
458  u.b.l->t==BoolExpr::NT_RLIN) {
459  u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
460  u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
461  } else if (u.b.l->t==BoolExpr::NT_RLIN) {
462  u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,icl),
463  !u.b.l->u.a.neg,icl);
464  } else if (u.b.r->t==BoolExpr::NT_RLIN) {
465  u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,icl),
466  !u.b.r->u.a.neg,icl);
467 #ifdef GECODE_HAS_FLOAT_VARS
468  } else if (u.b.l->t==BoolExpr::NT_VAR &&
469  u.b.r->t==BoolExpr::NT_RLINFLOAT) {
470  u.b.r->u.a.x->rfl.post(home, u.b.l->u.a.x->x,
471  u.b.l->u.a.neg==u.b.r->u.a.neg);
472  } else if (u.b.r->t==BoolExpr::NT_VAR &&
473  u.b.l->t==BoolExpr::NT_RLINFLOAT) {
474  u.b.l->u.a.x->rfl.post(home, u.b.r->u.a.x->x,
475  u.b.l->u.a.neg==u.b.r->u.a.neg);
476  } else if (u.b.l->t==BoolExpr::NT_RLINFLOAT) {
477  u.b.l->u.a.x->rfl.post(home, u.b.r->expr(home,icl),
478  !u.b.l->u.a.neg);
479  } else if (u.b.r->t==BoolExpr::NT_RLINFLOAT) {
480  u.b.r->u.a.x->rfl.post(home, u.b.l->expr(home,icl),
481  !u.b.r->u.a.neg);
482 #endif
483 #ifdef GECODE_HAS_SET_VARS
484  } else if (u.b.l->t==BoolExpr::NT_VAR &&
485  u.b.r->t==BoolExpr::NT_RSET) {
486  u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
487  u.b.l->u.a.neg==u.b.r->u.a.neg);
488  } else if (u.b.r->t==BoolExpr::NT_VAR &&
489  u.b.l->t==BoolExpr::NT_RSET) {
490  u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
491  u.b.l->u.a.neg==u.b.r->u.a.neg);
492  } else if (u.b.l->t==BoolExpr::NT_RSET) {
493  u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,icl),
494  !u.b.l->u.a.neg);
495  } else if (u.b.r->t==BoolExpr::NT_RSET) {
496  u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,icl),
497  !u.b.r->u.a.neg);
498 #endif
499  } else {
500  Gecode::rel(home, expr(home, icl), IRT_EQ, 1);
501  }
502  break;
503  default:
504  GECODE_NEVER;
505  }
506  }
507 
508  NNF*
509  NNF::nnf(Region& r, Node* n, bool neg) {
510  switch (n->t) {
511  case BoolExpr::NT_VAR:
512  case BoolExpr::NT_RLIN:
513  case BoolExpr::NT_MISC:
514  #ifdef GECODE_HAS_FLOAT_VARS
516  #endif
517  #ifdef GECODE_HAS_SET_VARS
518  case BoolExpr::NT_RSET:
519  #endif
520  {
521  NNF* x = new (r) NNF;
522  x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
523  if (neg) {
524  x->p = 0; x->n = 1;
525  } else {
526  x->p = 1; x->n = 0;
527  }
528  return x;
529  }
530  case BoolExpr::NT_NOT:
531  return nnf(r,n->l,!neg);
533  {
534  NodeType t = ((n->t == BoolExpr::NT_AND) == neg) ?
536  NNF* x = new (r) NNF;
537  x->t = t;
538  x->u.b.l = nnf(r,n->l,neg);
539  x->u.b.r = nnf(r,n->r,neg);
540  int p_l, n_l;
541  if ((x->u.b.l->t == t) ||
542  (x->u.b.l->t == BoolExpr::NT_VAR)) {
543  p_l=x->u.b.l->p; n_l=x->u.b.l->n;
544  } else {
545  p_l=1; n_l=0;
546  }
547  int p_r, n_r;
548  if ((x->u.b.r->t == t) ||
549  (x->u.b.r->t == BoolExpr::NT_VAR)) {
550  p_r=x->u.b.r->p; n_r=x->u.b.r->n;
551  } else {
552  p_r=1; n_r=0;
553  }
554  x->p = p_l+p_r;
555  x->n = n_l+n_r;
556  return x;
557  }
558  case BoolExpr::NT_EQV:
559  {
560  NNF* x = new (r) NNF;
561  x->t = BoolExpr::NT_EQV;
562  x->u.b.l = nnf(r,n->l,neg);
563  x->u.b.r = nnf(r,n->r,false);
564  x->p = 2; x->n = 0;
565  return x;
566  }
567  default:
568  GECODE_NEVER;
569  }
570  GECODE_NEVER;
571  return NULL;
572  }
573  }
574 
575  BoolVar
576  BoolExpr::expr(Home home, IntConLevel icl) const {
577  Region r(home);
578  return NNF::nnf(r,n,false)->expr(home,icl);
579  }
580 
581  void
582  BoolExpr::rel(Home home, IntConLevel icl) const {
583  Region r(home);
584  return NNF::nnf(r,n,false)->rel(home,icl);
585  }
586 
587 
588  BoolExpr
589  operator &&(const BoolExpr& l, const BoolExpr& r) {
590  return BoolExpr(l,BoolExpr::NT_AND,r);
591  }
592  BoolExpr
593  operator ||(const BoolExpr& l, const BoolExpr& r) {
594  return BoolExpr(l,BoolExpr::NT_OR,r);
595  }
596  BoolExpr
597  operator ^(const BoolExpr& l, const BoolExpr& r) {
599  }
600 
601  BoolExpr
602  operator !(const BoolExpr& e) {
603  return BoolExpr(e,BoolExpr::NT_NOT);
604  }
605 
606  BoolExpr
607  operator !=(const BoolExpr& l, const BoolExpr& r) {
608  return !BoolExpr(l, BoolExpr::NT_EQV, r);
609  }
610  BoolExpr
611  operator ==(const BoolExpr& l, const BoolExpr& r) {
612  return BoolExpr(l, BoolExpr::NT_EQV, r);
613  }
614  BoolExpr
615  operator >>(const BoolExpr& l, const BoolExpr& r) {
617  BoolExpr::NT_OR,r);
618  }
619  BoolExpr
620  operator <<(const BoolExpr& l, const BoolExpr& r) {
622  BoolExpr::NT_OR,l);
623  }
624  /*
625  * Posting Boolean expressions and relations
626  *
627  */
628  BoolVar
629  expr(Home home, const BoolExpr& e, IntConLevel icl) {
630  if (!home.failed())
631  return e.expr(home,icl);
632  BoolVar x(home,0,1);
633  return x;
634  }
635 
636  void
637  rel(Home home, const BoolExpr& e, IntConLevel icl) {
638  if (home.failed()) return;
639  e.rel(home,icl);
640  }
641 
642  /*
643  * Boolean element constraints
644  *
645  */
646 
649  public:
653  int n;
657  BElementExpr(int size);
659  virtual ~BElementExpr(void);
661  virtual void post(Space& home, BoolVar b, bool neg, IntConLevel icl);
662  };
663 
665  : a(heap.alloc<BoolExpr>(size)), n(size) {}
666 
668  heap.free<BoolExpr>(a,n);
669  }
670 
671  void
673  IntVar z = idx.post(home, icl);
674  if (z.assigned() && z.val() >= 0 && z.val() < n) {
675  BoolExpr be = pos ? (a[z.val()] == b) : (a[z.val()] == !b);
676  be.rel(home,icl);
677  } else {
678  BoolVarArgs x(n);
679  for (int i=n; i--;)
680  x[i] = a[i].expr(home,icl);
681  BoolVar res = pos ? b : (!b).expr(home,icl);
682  element(home, x, z, res, icl);
683  }
684  }
685 
686  BoolExpr
687  element(const BoolVarArgs& b, const LinIntExpr& idx) {
688  BElementExpr* be = new BElementExpr(b.size());
689  for (int i=b.size(); i--;)
690  new (&be->a[i]) BoolExpr(b[i]);
691  be->idx = idx;
692  return BoolExpr(be);
693  }
694 
695 }
696 
697 // STATISTICS: minimodel-any