Generated on Sat Feb 7 2015 02:01:17 for Gecode by doxygen 1.8.9.1
lq-le.hpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Christian Schulte <schulte@gecode.org>
5  * Gabor Szokoli <szokoli@gecode.org>
6  * Vincent Barichard <Vincent.Barichard@univ-angers.fr>
7  *
8  * Copyright:
9  * Christian Schulte, 2003
10  * Gabor Szokoli, 2003
11  * Vincent Barichard, 2012
12  *
13  * Last modified:
14  * $Date: 2013-03-18 10:20:43 +0100 (Mon, 18 Mar 2013) $ by $Author: vbarichard $
15  * $Revision: 13548 $
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 namespace Gecode { namespace Float { namespace Rel {
43 
44  /*
45  * Less or equal propagator
46  *
47  */
48 
49  template<class View>
51  Lq<View>::Lq(Home home, View x0, View x1)
52  : BinaryPropagator<View,PC_FLOAT_BND>(home,x0,x1) {}
53 
54  template<class View>
56  Lq<View>::post(Home home, View x0, View x1) {
57  GECODE_ME_CHECK(x0.lq(home,x1.max()));
58  GECODE_ME_CHECK(x1.gq(home,x0.min()));
59  if (!same(x0,x1) && (x0.max() > x1.min()))
60  (void) new (home) Lq<View>(home,x0,x1);
61  return ES_OK;
62  }
63 
64  template<class View>
66  Lq<View>::Lq(Space& home, bool share, Lq<View>& p)
67  : BinaryPropagator<View,PC_FLOAT_BND>(home,share,p) {}
68 
69  template<class View>
70  Actor*
71  Lq<View>::copy(Space& home, bool share) {
72  return new (home) Lq<View>(home,share,*this);
73  }
74 
75  template<class View>
78  GECODE_ME_CHECK(x0.lq(home,x1.max()));
79  GECODE_ME_CHECK(x1.gq(home,x0.min()));
80  return (x0.assigned() || x1.assigned() || (x0.max() <= x1.min())) ? home.ES_SUBSUMED(*this) : ES_FIX;
81  }
82 
83 
84  /*
85  * Less propagator
86  *
87  */
88  template<class View>
90  Le<View>::Le(Home home, View x0, View x1)
91  : BinaryPropagator<View,PC_FLOAT_BND>(home,x0,x1) {}
92 
93  template<class View>
95  Le<View>::post(Home home, View x0, View x1) {
96  GECODE_ME_CHECK(x0.lq(home,x1.max()));
97  GECODE_ME_CHECK(x1.gq(home,x0.min()));
98  if (x0.assigned() && x1.assigned()) {
99  if (x0.max() >= x1.min())
100  return ES_FAILED;
101  } else if (same(x0,x1))
102  return ES_FAILED;
103  if (x0.max() >= x1.min())
104  (void) new (home) Le<View>(home,x0,x1);
105  return ES_OK;
106  }
107 
108  template<class View>
110  Le<View>::Le(Space& home, bool share, Le<View>& p)
111  : BinaryPropagator<View,PC_FLOAT_BND>(home,share,p) {}
112 
113  template<class View>
114  Actor*
115  Le<View>::copy(Space& home, bool share) {
116  return new (home) Le<View>(home,share,*this);
117  }
118 
119  template<class View>
120  ExecStatus
122  GECODE_ME_CHECK(x0.lq(home,x1.max()));
123  GECODE_ME_CHECK(x1.gq(home,x0.min()));
124  if (x0.assigned() && x1.assigned()) {
125  return (x0.max() >= x1.min()) ? ES_FAILED : home.ES_SUBSUMED(*this);
126  }
127  return (x0.max() < x1.min()) ? home.ES_SUBSUMED(*this) : ES_FIX;
128  }
129 
130 
131 
132 
133  /*
134  * Reified less or equal propagator
135  *
136  */
137 
138  template<class View, class CtrlView, ReifyMode rm>
140  ReLq<View,CtrlView,rm>::ReLq(Home home, View x0, View x1, CtrlView b)
141  : Int::ReBinaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,x0,x1,b) {}
142 
143  template<class View, class CtrlView, ReifyMode rm>
144  ExecStatus
145  ReLq<View,CtrlView,rm>::post(Home home, View x0, View x1, CtrlView b) {
146  if (b.one()) {
147  if (rm == RM_PMI)
148  return ES_OK;
149  return Lq<View>::post(home,x0,x1);
150  }
151  if (b.zero()) {
152  if (rm == RM_IMP)
153  return ES_OK;
154  return Le<View>::post(home,x1,x0);
155  }
156  if (!same(x0,x1)) {
157  switch (rtest_lq(x0,x1)) {
158  case RT_TRUE:
159  if (rm != RM_IMP)
160  GECODE_ME_CHECK(b.one_none(home));
161  break;
162  case RT_FALSE:
163  if (rm != RM_PMI)
164  GECODE_ME_CHECK(b.zero_none(home));
165  break;
166  case RT_MAYBE:
167  if (!x0.assigned() || !x1.assigned())
168  (void) new (home) ReLq<View,CtrlView,rm>(home,x0,x1,b);
169  else {
170  if (rm != RM_IMP)
171  GECODE_ME_CHECK(b.one_none(home));
172  }
173  break;
174  default: GECODE_NEVER;
175  }
176  } else if (rm != RM_IMP) {
177  GECODE_ME_CHECK(b.one_none(home));
178  }
179  return ES_OK;
180  }
181 
182  template<class View, class CtrlView, ReifyMode rm>
185  : Int::ReBinaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,share,p) {}
186 
187  template<class View, class CtrlView, ReifyMode rm>
188  Actor*
189  ReLq<View,CtrlView,rm>::copy(Space& home, bool share) {
190  return new (home) ReLq<View,CtrlView,rm>(home,share,*this);
191  }
192 
193  template<class View, class CtrlView, ReifyMode rm>
194  ExecStatus
196  if (b.one()) {
197  if (rm != RM_PMI)
198  GECODE_REWRITE(*this,Lq<View>::post(home(*this),x0,x1));
199  } else if (b.zero()) {
200  if (rm != RM_IMP)
201  GECODE_REWRITE(*this,Le<View>::post(home(*this),x1,x0));
202  } else {
203  switch (rtest_lq(x0,x1)) {
204  case RT_TRUE:
205  if (rm != RM_IMP)
206  GECODE_ME_CHECK(b.one_none(home));
207  break;
208  case RT_FALSE:
209  if (rm != RM_PMI)
210  GECODE_ME_CHECK(b.zero_none(home));
211  break;
212  case RT_MAYBE:
213  if (!x0.assigned() || !x1.assigned())
214  return ES_FIX;
215  else {
216  if (rm != RM_IMP)
217  GECODE_ME_CHECK(b.one_none(home));
218  break;
219  }
220  default: GECODE_NEVER;
221  }
222  }
223  return home.ES_SUBSUMED(*this);
224  }
225 
226  /*
227  * Reified less or equal propagator involving one variable
228  *
229  */
230 
231  template<class View, class CtrlView, ReifyMode rm>
234  : Int::ReUnaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,x,b), c(c0) {}
235 
236  template<class View, class CtrlView, ReifyMode rm>
237  ExecStatus
239  if (b.one()) {
240  if (rm != RM_PMI)
241  GECODE_ME_CHECK(x.lq(home,c.max()));
242  } if (b.zero()) {
243  if (rm != RM_IMP) {
244  GECODE_ME_CHECK(x.gq(home,c.min()));
245  if (x.assigned() && (x.min() <= c.max()))
246  return ES_FAILED;
247  (void) new (home) ReLqFloat<View,CtrlView,rm>(home,x,c,b);
248  }
249  } else {
250  switch (rtest_lq(x,c)) {
251  case RT_TRUE:
252  if (rm != RM_IMP)
253  GECODE_ME_CHECK(b.one(home));
254  break;
255  case RT_FALSE:
256  if (rm != RM_PMI)
257  GECODE_ME_CHECK(b.zero(home));
258  break;
259  case RT_MAYBE:
260  (void) new (home) ReLqFloat<View,CtrlView,rm>(home,x,c,b);
261  break;
262  default: GECODE_NEVER;
263  }
264  }
265  return ES_OK;
266  }
267 
268 
269  template<class View, class CtrlView, ReifyMode rm>
272  : Int::ReUnaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,share,p), c(p.c) {}
273 
274  template<class View, class CtrlView, ReifyMode rm>
275  Actor*
277  return new (home) ReLqFloat<View,CtrlView,rm>(home,share,*this);
278  }
279 
280  template<class View, class CtrlView, ReifyMode rm>
281  ExecStatus
283  if (b.one()) {
284  if (rm != RM_PMI)
285  GECODE_ME_CHECK(x0.lq(home,c.max()));
286  } else if (b.zero()) {
287  if (rm != RM_IMP)
288  {
289  GECODE_ME_CHECK(x0.gq(home,c.min()));
290  if (x0.assigned()) {
291  return (x0.min() <= c.max()) ? ES_FAILED : home.ES_SUBSUMED(*this);
292  }
293  }
294  } else {
295  switch (rtest_lq(x0,c)) {
296  case RT_TRUE:
297  if (rm != RM_IMP)
298  GECODE_ME_CHECK(b.one(home));
299  break;
300  case RT_FALSE:
301  if (rm != RM_PMI)
302  GECODE_ME_CHECK(b.zero(home));
303  break;
304  case RT_MAYBE:
305  return ES_FIX;
306  default: GECODE_NEVER;
307  }
308  }
309  return home.ES_SUBSUMED(*this);
310  }
311 
312 
313  /*
314  * Reified less
315  *
316  */
317 
318  template<class View, class CtrlView, ReifyMode rm>
321  : Int::ReUnaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,x,b), c(c0) {}
322 
323  template<class View, class CtrlView, ReifyMode rm>
324  ExecStatus
326  if (b.one()) {
327  if (rm != RM_PMI)
328  {
329  GECODE_ME_CHECK(x.lq(home,c.max()));
330  if (x.assigned() && (x.max() >= c.min()))
331  return ES_FAILED;
332  (void) new (home) ReLeFloat<View,CtrlView,rm>(home,x,c,b);
333  }
334  } else if (b.zero()) {
335  if (rm != RM_IMP)
336  GECODE_ME_CHECK(x.gq(home,c.min()));
337  } else {
338  switch (rtest_le(x,c)) {
339  case RT_TRUE:
340  if (rm != RM_IMP)
341  GECODE_ME_CHECK(b.one(home));
342  break;
343  case RT_FALSE:
344  if (rm != RM_PMI)
345  GECODE_ME_CHECK(b.zero(home));
346  break;
347  case RT_MAYBE:
348  (void) new (home) ReLeFloat<View,CtrlView,rm>(home,x,c,b);
349  break;
350  default: GECODE_NEVER;
351  }
352  }
353  return ES_OK;
354  }
355 
356 
357  template<class View, class CtrlView, ReifyMode rm>
360  : Int::ReUnaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,share,p), c(p.c) {}
361 
362  template<class View, class CtrlView, ReifyMode rm>
363  Actor*
365  return new (home) ReLeFloat<View,CtrlView,rm>(home,share,*this);
366  }
367 
368  template<class View, class CtrlView, ReifyMode rm>
369  ExecStatus
371  if (b.one()) {
372  if (rm != RM_PMI)
373  {
374  GECODE_ME_CHECK(x0.lq(home,c.max()));
375  if (x0.assigned()) {
376  return (x0.max() >= c.min()) ? ES_FAILED : home.ES_SUBSUMED(*this);
377  }
378  }
379  } else if (b.zero()) {
380  if (rm != RM_IMP)
381  GECODE_ME_CHECK(x0.gq(home,c.min()));
382  } else {
383  switch (rtest_le(x0,c)) {
384  case RT_TRUE:
385  if (rm != RM_IMP)
386  GECODE_ME_CHECK(b.one(home));
387  break;
388  case RT_FALSE:
389  if (rm != RM_PMI)
390  GECODE_ME_CHECK(b.zero(home));
391  break;
392  case RT_MAYBE:
393  return ES_FIX;
394  default: GECODE_NEVER;
395  }
396  }
397  return home.ES_SUBSUMED(*this);
398  }
399 
400 }}}
401 
402 // STATISTICS: float-prop
403 
static ExecStatus post(Home home, View x, FloatVal c, CtrlView b)
Post propagator for .
Definition: lq-le.hpp:238
Le(Space &home, bool share, Le &p)
Constructor for cloning p.
Definition: lq-le.hpp:110
RelTest rtest_lq(View x, View y)
Test whether view x is less or equal than view y.
Definition: rel-test.hpp:58
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:109
Reified less or equal propagator.
Definition: rel.hh:358
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lq-le.hpp:77
Inverse implication for reification.
Definition: int.hh:847
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:2973
Reified unary propagator.
Definition: propagator.hpp:58
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lq-le.hpp:195
static ExecStatus post(Home home, View x, FloatVal c, CtrlView b)
Post propagator for .
Definition: lq-le.hpp:325
Reified binary propagator.
Definition: propagator.hpp:89
Relation does hold.
Definition: view.hpp:498
Relation does not hold.
Definition: view.hpp:496
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lq-le.hpp:282
Propagation has computed fixpoint.
Definition: core.hpp:528
Computation spaces.
Definition: core.hpp:1362
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lq-le.hpp:115
Base-class for both propagators and branchers.
Definition: core.hpp:666
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lq-le.hpp:121
Gecode::FloatVal c(-8, 8)
ReLeFloat(Space &home, bool share, ReLeFloat &p)
Constructor for cloning p.
Definition: lq-le.hpp:359
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
bool same(const ConstView< ViewA > &, const ConstView< ViewB > &)
Test whether two views are the same.
Definition: view.hpp:603
Reified less or equal with float propagator.
Definition: rel.hh:302
Execution has resulted in failure.
Definition: core.hpp:525
Binary propagator.
Definition: propagator.hpp:87
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lq-le.hpp:276
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lq-le.hpp:364
static ExecStatus post(Home home, View x0, View x1)
Post propagator .
Definition: lq-le.hpp:95
ReLqFloat(Space &home, bool share, ReLqFloat &p)
Constructor for cloning p.
Definition: lq-le.hpp:271
static ExecStatus post(Home home, View x0, View x1)
Post propagator .
Definition: lq-le.hpp:56
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:45
Less or equal propagator.
Definition: rel.hh:245
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lq-le.hpp:71
Float value type.
Definition: float.hh:321
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
static ExecStatus post(Home home, View x0, View x1, CtrlView b)
Post propagator for .
Definition: lq-le.hpp:145
ExecStatus
Definition: core.hpp:523
#define forceinline
Definition: config.hpp:132
Execution is okay.
Definition: core.hpp:527
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lq-le.hpp:189
const Gecode::PropCond PC_FLOAT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:292
RelTest rtest_le(View x, View y)
Test whether view x is less than view y.
Definition: rel-test.hpp:74
ReLq(Space &home, bool share, ReLq &p)
Constructor for cloning p.
Definition: lq-le.hpp:184
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
Gecode toplevel namespace
Implication for reification.
Definition: int.hh:840
Relation may hold or not.
Definition: view.hpp:497
friend FloatVal max(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:390
int ModEventDelta
Modification event deltas.
Definition: core.hpp:173
friend FloatVal min(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:402
Home class for posting propagators
Definition: core.hpp:717
Lq(Space &home, bool share, Lq &p)
Constructor for cloning p.
Definition: lq-le.hpp:66
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lq-le.hpp:370
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60
Less propagator.
Definition: rel.hh:271
Reified less with float propagator.
Definition: rel.hh:330