Generated on Sat Nov 9 2013 19:18:30 for Gecode by doxygen 1.8.4
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-04-29 14:55:17 +0200 (Mon, 29 Apr 2013) $ by $Author: schulte $
15  * $Revision: 13588 $
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
64 #endif
65 #ifdef GECODE_HAS_SET_VARS
66  SetRel rs;
68 #endif
69  MiscExpr* m;
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  */
91  : use(1), l(NULL), r(NULL), m(NULL) {}
92 
94  delete m;
95  }
96 
97  void*
98  BoolExpr::Node::operator new(size_t size) {
99  return heap.ralloc(size);
100  }
101  void
102  BoolExpr::Node::operator delete(void* p, size_t) {
103  heap.rfree(p);
104  }
105 
106  bool
108  if (--use == 0) {
109  if ((l != NULL) && l->decrement())
110  delete l;
111  if ((r != NULL) && r->decrement())
112  delete r;
113  return true;
114  }
115  return false;
116  }
117 
118  BoolExpr::BoolExpr(void) : n(new Node) {}
119 
120  BoolExpr::BoolExpr(const BoolExpr& e) : n(e.n) {
121  n->use++;
122  }
123 
124  BoolExpr::BoolExpr(const BoolVar& x) : n(new Node) {
125  n->same = 1;
126  n->t = NT_VAR;
127  n->l = NULL;
128  n->r = NULL;
129  n->x = x;
130  }
131 
133  : n(new Node) {
134  int ls = ((l.n->t == t) || (l.n->t == NT_VAR)) ? l.n->same : 1;
135  int rs = ((r.n->t == t) || (r.n->t == NT_VAR)) ? r.n->same : 1;
136  n->same = ls+rs;
137  n->t = t;
138  n->l = l.n;
139  n->l->use++;
140  n->r = r.n;
141  n->r->use++;
142  }
143 
145  (void) t;
146  assert(t == NT_NOT);
147  if (l.n->t == NT_NOT) {
148  n = l.n->l;
149  n->use++;
150  } else {
151  n = new Node;
152  n->same = 1;
153  n->t = NT_NOT;
154  n->l = l.n;
155  n->l->use++;
156  n->r = NULL;
157  }
158  }
159 
161  : n(new Node) {
162  n->same = 1;
163  n->t = NT_RLIN;
164  n->l = NULL;
165  n->r = NULL;
166  n->rl = rl;
167  }
168 
169 #ifdef GECODE_HAS_FLOAT_VARS
171  : n(new Node) {
172  n->same = 1;
173  n->t = NT_RLINFLOAT;
174  n->l = NULL;
175  n->r = NULL;
176  n->rfl = rfl;
177  }
178 #endif
179 
180 #ifdef GECODE_HAS_SET_VARS
182  : n(new Node) {
183  n->same = 1;
184  n->t = NT_RSET;
185  n->l = NULL;
186  n->r = NULL;
187  n->rs = rs;
188  }
189 
191  : n(new Node) {
192  n->same = 1;
193  n->t = NT_RSET;
194  n->l = NULL;
195  n->r = NULL;
196  n->rs = rs;
197  }
198 #endif
199 
201  : n(new Node) {
202  n->same = 1;
203  n->t = NT_MISC;
204  n->l = NULL;
205  n->r = NULL;
206  n->m = m;
207  }
208 
209  const BoolExpr&
211  if (this != &e) {
212  if (n->decrement())
213  delete n;
214  n = e.n;
215  n->use++;
216  }
217  return *this;
218  }
219 
221 
223  if (n->decrement())
224  delete n;
225  }
226 
227  namespace {
229  class NNF {
230  public:
232  typedef BoolExpr::Node Node;
236  int p;
238  int n;
240  union {
242  struct {
244  NNF* l;
246  NNF* r;
247  } b;
249  struct {
251  bool neg;
253  Node* x;
254  } a;
255  } u;
258  static NNF* nnf(Region& r, Node* n, bool neg);
261  void post(Home home, NodeType t,
262  BoolVarArgs& bp, BoolVarArgs& bn,
263  int& ip, int& in,
264  IntConLevel icl) const;
267  BoolVar expr(Home home, IntConLevel icl) const;
270  void rel(Home home, IntConLevel icl) const;
272  static void* operator new(size_t s, Region& r);
274  static void operator delete(void*);
276  static void operator delete(void*, Region&);
277  };
278 
279  /*
280  * Operations for negation normalform
281  *
282  */
283  forceinline void
284  NNF::operator delete(void*) {}
285 
286  forceinline void
287  NNF::operator delete(void*, Region&) {}
288 
289  forceinline void*
290  NNF::operator new(size_t s, Region& r) {
291  return r.ralloc(s);
292  }
293 
294  BoolVar
295  NNF::expr(Home home, IntConLevel icl) const {
296  if ((t == BoolExpr::NT_VAR) && !u.a.neg)
297  return u.a.x->x;
298  BoolVar b(home,0,1);
299  switch (t) {
300  case BoolExpr::NT_VAR:
301  assert(u.a.neg);
302  Gecode::rel(home, u.a.x->x, IRT_NQ, b);
303  break;
304  case BoolExpr::NT_RLIN:
305  u.a.x->rl.post(home, b, !u.a.neg, icl);
306  break;
307 #ifdef GECODE_HAS_FLOAT_VARS
309  u.a.x->rfl.post(home, b, !u.a.neg);
310  break;
311 #endif
312 #ifdef GECODE_HAS_SET_VARS
313  case BoolExpr::NT_RSET:
314  u.a.x->rs.post(home, b, !u.a.neg);
315  break;
316 #endif
317  case BoolExpr::NT_MISC:
318  u.a.x->m->post(home, b, !u.a.neg, icl);
319  break;
320  case BoolExpr::NT_AND:
321  {
322  BoolVarArgs bp(p), bn(n);
323  int ip=0, in=0;
324  post(home, BoolExpr::NT_AND, bp, bn, ip, in, icl);
325  clause(home, BOT_AND, bp, bn, b);
326  }
327  break;
328  case BoolExpr::NT_OR:
329  {
330  BoolVarArgs bp(p), bn(n);
331  int ip=0, in=0;
332  post(home, BoolExpr::NT_OR, bp, bn, ip, in, icl);
333  clause(home, BOT_OR, bp, bn, b);
334  }
335  break;
336  case BoolExpr::NT_EQV:
337  {
338  bool n = false;
339  BoolVar l;
340  if (u.b.l->t == BoolExpr::NT_VAR) {
341  l = u.b.l->u.a.x->x;
342  if (u.b.l->u.a.neg) n = !n;
343  } else {
344  l = u.b.l->expr(home,icl);
345  }
346  BoolVar r;
347  if (u.b.r->t == BoolExpr::NT_VAR) {
348  r = u.b.r->u.a.x->x;
349  if (u.b.r->u.a.neg) n = !n;
350  } else {
351  r = u.b.r->expr(home,icl);
352  }
353  Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, icl);
354  }
355  break;
356  default:
357  GECODE_NEVER;
358  }
359  return b;
360  }
361 
362  void
363  NNF::post(Home home, NodeType t,
364  BoolVarArgs& bp, BoolVarArgs& bn,
365  int& ip, int& in,
366  IntConLevel icl) const {
367  if (this->t != t) {
368  switch (this->t) {
369  case BoolExpr::NT_VAR:
370  if (u.a.neg) {
371  bn[in++]=u.a.x->x;
372  } else {
373  bp[ip++]=u.a.x->x;
374  }
375  break;
376  case BoolExpr::NT_RLIN:
377  {
378  BoolVar b(home,0,1);
379  u.a.x->rl.post(home, b, !u.a.neg, icl);
380  bp[ip++]=b;
381  }
382  break;
383 #ifdef GECODE_HAS_FLOAT_VARS
385  {
386  BoolVar b(home,0,1);
387  u.a.x->rfl.post(home, b, !u.a.neg);
388  bp[ip++]=b;
389  }
390  break;
391 #endif
392 #ifdef GECODE_HAS_SET_VARS
393  case BoolExpr::NT_RSET:
394  {
395  BoolVar b(home,0,1);
396  u.a.x->rs.post(home, b, !u.a.neg);
397  bp[ip++]=b;
398  }
399  break;
400 #endif
401  case BoolExpr::NT_MISC:
402  {
403  BoolVar b(home,0,1);
404  u.a.x->m->post(home, b, !u.a.neg, icl);
405  bp[ip++]=b;
406  }
407  break;
408  default:
409  bp[ip++] = expr(home, icl);
410  break;
411  }
412  } else {
413  u.b.l->post(home, t, bp, bn, ip, in, icl);
414  u.b.r->post(home, t, bp, bn, ip, in, icl);
415  }
416  }
417 
418  void
419  NNF::rel(Home home, IntConLevel icl) const {
420  switch (t) {
421  case BoolExpr::NT_VAR:
422  Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
423  break;
424  case BoolExpr::NT_RLIN:
425  u.a.x->rl.post(home, !u.a.neg, icl);
426  break;
427 #ifdef GECODE_HAS_FLOAT_VARS
429  u.a.x->rfl.post(home, !u.a.neg);
430  break;
431 #endif
432 #ifdef GECODE_HAS_SET_VARS
433  case BoolExpr::NT_RSET:
434  u.a.x->rs.post(home, !u.a.neg);
435  break;
436 #endif
437  case BoolExpr::NT_MISC:
438  {
439  BoolVar b(home,!u.a.neg,!u.a.neg);
440  u.a.x->m->post(home, b, false, icl);
441  }
442  break;
443  case BoolExpr::NT_AND:
444  u.b.l->rel(home, icl);
445  u.b.r->rel(home, icl);
446  break;
447  case BoolExpr::NT_OR:
448  {
449  BoolVarArgs bp(p), bn(n);
450  int ip=0, in=0;
451  post(home, BoolExpr::NT_OR, bp, bn, ip, in, icl);
452  clause(home, BOT_OR, bp, bn, 1);
453  }
454  break;
455  case BoolExpr::NT_EQV:
456  if (u.b.l->t==BoolExpr::NT_VAR &&
457  u.b.r->t==BoolExpr::NT_RLIN) {
458  u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
459  u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
460  } else if (u.b.r->t==BoolExpr::NT_VAR &&
461  u.b.l->t==BoolExpr::NT_RLIN) {
462  u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
463  u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
464  } else if (u.b.l->t==BoolExpr::NT_RLIN) {
465  u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,icl),
466  !u.b.l->u.a.neg,icl);
467  } else if (u.b.r->t==BoolExpr::NT_RLIN) {
468  u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,icl),
469  !u.b.r->u.a.neg,icl);
470 #ifdef GECODE_HAS_FLOAT_VARS
471  } else if (u.b.l->t==BoolExpr::NT_VAR &&
472  u.b.r->t==BoolExpr::NT_RLINFLOAT) {
473  u.b.r->u.a.x->rfl.post(home, u.b.l->u.a.x->x,
474  u.b.l->u.a.neg==u.b.r->u.a.neg);
475  } else if (u.b.r->t==BoolExpr::NT_VAR &&
476  u.b.l->t==BoolExpr::NT_RLINFLOAT) {
477  u.b.l->u.a.x->rfl.post(home, u.b.r->u.a.x->x,
478  u.b.l->u.a.neg==u.b.r->u.a.neg);
479  } else if (u.b.l->t==BoolExpr::NT_RLINFLOAT) {
480  u.b.l->u.a.x->rfl.post(home, u.b.r->expr(home,icl),
481  !u.b.l->u.a.neg);
482  } else if (u.b.r->t==BoolExpr::NT_RLINFLOAT) {
483  u.b.r->u.a.x->rfl.post(home, u.b.l->expr(home,icl),
484  !u.b.r->u.a.neg);
485 #endif
486 #ifdef GECODE_HAS_SET_VARS
487  } else if (u.b.l->t==BoolExpr::NT_VAR &&
488  u.b.r->t==BoolExpr::NT_RSET) {
489  u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
490  u.b.l->u.a.neg==u.b.r->u.a.neg);
491  } else if (u.b.r->t==BoolExpr::NT_VAR &&
492  u.b.l->t==BoolExpr::NT_RSET) {
493  u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
494  u.b.l->u.a.neg==u.b.r->u.a.neg);
495  } else if (u.b.l->t==BoolExpr::NT_RSET) {
496  u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,icl),
497  !u.b.l->u.a.neg);
498  } else if (u.b.r->t==BoolExpr::NT_RSET) {
499  u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,icl),
500  !u.b.r->u.a.neg);
501 #endif
502  } else {
503  Gecode::rel(home, expr(home, icl), IRT_EQ, 1);
504  }
505  break;
506  default:
507  GECODE_NEVER;
508  }
509  }
510 
511  NNF*
512  NNF::nnf(Region& r, Node* n, bool neg) {
513  switch (n->t) {
514  case BoolExpr::NT_VAR:
515  case BoolExpr::NT_RLIN:
516  case BoolExpr::NT_MISC:
517  #ifdef GECODE_HAS_FLOAT_VARS
519  #endif
520  #ifdef GECODE_HAS_SET_VARS
521  case BoolExpr::NT_RSET:
522  #endif
523  {
524  NNF* x = new (r) NNF;
525  x->t = n->t; x->u.a.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 BoolExpr::NT_NOT:
534  return nnf(r,n->l,!neg);
536  {
537  NodeType t = ((n->t == BoolExpr::NT_AND) == neg) ?
539  NNF* x = new (r) NNF;
540  x->t = t;
541  x->u.b.l = nnf(r,n->l,neg);
542  x->u.b.r = nnf(r,n->r,neg);
543  int p_l, n_l;
544  if ((x->u.b.l->t == t) ||
545  (x->u.b.l->t == BoolExpr::NT_VAR)) {
546  p_l=x->u.b.l->p; n_l=x->u.b.l->n;
547  } else {
548  p_l=1; n_l=0;
549  }
550  int p_r, n_r;
551  if ((x->u.b.r->t == t) ||
552  (x->u.b.r->t == BoolExpr::NT_VAR)) {
553  p_r=x->u.b.r->p; n_r=x->u.b.r->n;
554  } else {
555  p_r=1; n_r=0;
556  }
557  x->p = p_l+p_r;
558  x->n = n_l+n_r;
559  return x;
560  }
561  case BoolExpr::NT_EQV:
562  {
563  NNF* x = new (r) NNF;
564  x->t = BoolExpr::NT_EQV;
565  x->u.b.l = nnf(r,n->l,neg);
566  x->u.b.r = nnf(r,n->r,false);
567  x->p = 2; x->n = 0;
568  return x;
569  }
570  default:
571  GECODE_NEVER;
572  }
573  GECODE_NEVER;
574  return NULL;
575  }
576  }
577 
578  BoolVar
579  BoolExpr::expr(Home home, IntConLevel icl) const {
580  Region r(home);
581  return NNF::nnf(r,n,false)->expr(home,icl);
582  }
583 
584  void
585  BoolExpr::rel(Home home, IntConLevel icl) const {
586  Region r(home);
587  return NNF::nnf(r,n,false)->rel(home,icl);
588  }
589 
590 
591  BoolExpr
592  operator &&(const BoolExpr& l, const BoolExpr& r) {
593  return BoolExpr(l,BoolExpr::NT_AND,r);
594  }
595  BoolExpr
596  operator ||(const BoolExpr& l, const BoolExpr& r) {
597  return BoolExpr(l,BoolExpr::NT_OR,r);
598  }
599  BoolExpr
600  operator ^(const BoolExpr& l, const BoolExpr& r) {
602  }
603 
604  BoolExpr
605  operator !(const BoolExpr& e) {
606  return BoolExpr(e,BoolExpr::NT_NOT);
607  }
608 
609  BoolExpr
610  operator !=(const BoolExpr& l, const BoolExpr& r) {
611  return !BoolExpr(l, BoolExpr::NT_EQV, r);
612  }
613  BoolExpr
614  operator ==(const BoolExpr& l, const BoolExpr& r) {
615  return BoolExpr(l, BoolExpr::NT_EQV, r);
616  }
617  BoolExpr
618  operator >>(const BoolExpr& l, const BoolExpr& r) {
620  BoolExpr::NT_OR,r);
621  }
622  BoolExpr
623  operator <<(const BoolExpr& l, const BoolExpr& r) {
625  BoolExpr::NT_OR,l);
626  }
627  /*
628  * Posting Boolean expressions and relations
629  *
630  */
631  BoolVar
632  expr(Home home, const BoolExpr& e, IntConLevel icl) {
633  if (!home.failed())
634  return e.expr(home,icl);
635  BoolVar x(home,0,1);
636  return x;
637  }
638 
639  void
640  rel(Home home, const BoolExpr& e, IntConLevel icl) {
641  if (home.failed()) return;
642  e.rel(home,icl);
643  }
644 
645  /*
646  * Boolean element constraints
647  *
648  */
649 
652  public:
656  int n;
660  BElementExpr(int size);
662  virtual ~BElementExpr(void);
664  virtual void post(Space& home, BoolVar b, bool neg, IntConLevel icl);
665  };
666 
668  : a(heap.alloc<BoolExpr>(size)), n(size) {}
669 
671  heap.free<BoolExpr>(a,n);
672  }
673 
674  void
676  IntVar z = idx.post(home, icl);
677  if (z.assigned() && z.val() >= 0 && z.val() < n) {
678  BoolExpr be = pos ? (a[z.val()] == b) : (a[z.val()] == !b);
679  be.rel(home,icl);
680  } else {
681  BoolVarArgs x(n);
682  for (int i=n; i--;)
683  x[i] = a[i].expr(home,icl);
684  BoolVar res = pos ? b : (!b).expr(home,icl);
685  element(home, x, z, res, icl);
686  }
687  }
688 
689  BoolExpr
690  element(const BoolVarArgs& b, const LinIntExpr& idx) {
691  BElementExpr* be = new BElementExpr(b.size());
692  for (int i=b.size(); i--;)
693  new (&be->a[i]) BoolExpr(b[i]);
694  be->idx = idx;
695  return BoolExpr(be);
696  }
697 
698 }
699 
700 // STATISTICS: minimodel-any