Generated on Sat Feb 7 2015 02:01:17 for Gecode by doxygen 1.8.9.1
eq.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  * Vincent Barichard <Vincent.Barichard@univ-angers.fr>
6  *
7  * Copyright:
8  * Christian Schulte, 2004
9  * Vincent Barichard, 2012
10  *
11  * Last modified:
12  * $Date: 2013-01-24 19:28:06 +0100 (Thu, 24 Jan 2013) $ by $Author: schulte $
13  * $Revision: 13235 $
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 namespace Gecode { namespace Float { namespace Rel {
41 
42  /*
43  * Binary bounds consistent equality
44  *
45  */
46 
47  template<class View0, class View1>
49  Eq<View0,View1>::Eq(Home home, View0 x0, View1 x1)
50  : MixBinaryPropagator<View0,PC_FLOAT_BND,View1,PC_FLOAT_BND>(home,x0,x1) {}
51 
52  template<class View0, class View1>
54  Eq<View0,View1>::post(Home home, View0 x0, View1 x1){
55  if (x0.assigned()) {
56  GECODE_ME_CHECK(x1.eq(home,x0.val()));
57  } else if (x1.assigned()) {
58  GECODE_ME_CHECK(x0.eq(home,x1.val()));
59  } else if (!same(x0,x1)) {
60  GECODE_ME_CHECK(x0.lq(home,x1.max()));
61  GECODE_ME_CHECK(x1.lq(home,x0.max()));
62  GECODE_ME_CHECK(x0.gq(home,x1.min()));
63  GECODE_ME_CHECK(x1.gq(home,x0.min()));
64  (void) new (home) Eq<View0,View1>(home,x0,x1);
65  }
66  return ES_OK;
67  }
68 
69  template<class View0, class View1>
72  : MixBinaryPropagator<View0,PC_FLOAT_BND,View1,PC_FLOAT_BND>(home,share,p) {}
73 
74  template<class View0, class View1>
76  Eq<View0,View1>::Eq(Space& home, bool share, Propagator& p,
77  View0 x0, View1 x1)
78  : MixBinaryPropagator<View0,PC_FLOAT_BND,View1,PC_FLOAT_BND>(home,share,p,
79  x0,x1) {}
80 
81  template<class View0, class View1>
82  Actor*
83  Eq<View0,View1>::copy(Space& home, bool share) {
84  return new (home) Eq<View0,View1>(home,share,*this);
85  }
86 
87  template<class View0, class View1>
90  if (x0.assigned()) {
91  GECODE_ME_CHECK(x1.eq(home,x0.val()));
92  } else if (x1.assigned()) {
93  GECODE_ME_CHECK(x0.eq(home,x1.val()));
94  } else {
95  do {
96  GECODE_ME_CHECK(x0.gq(home,x1.min()));
97  GECODE_ME_CHECK(x1.gq(home,x0.min()));
98  } while (x0.min() != x1.min());
99  do {
100  GECODE_ME_CHECK(x0.lq(home,x1.max()));
101  GECODE_ME_CHECK(x1.lq(home,x0.max()));
102  } while (x0.max() != x1.max());
103  if (!x0.assigned())
104  return ES_FIX;
105  }
106  assert(x0.assigned() && x1.assigned());
107  return home.ES_SUBSUMED(*this);
108  }
109 
110 
111  /*
112  * Nary bound consistent equality
113  *
114  */
115 
116  template<class View>
119  : NaryPropagator<View,PC_FLOAT_BND>(home,x) {}
120 
121  template<class View>
122  ExecStatus
124  x.unique(home);
125  if (x.size() == 2) {
126  return Eq<View,View>::post(home,x[0],x[1]);
127  } else if (x.size() > 2) {
128  FloatNum l = x[0].min();
129  FloatNum u = x[0].max();
130  for (int i=x.size(); i-- > 1; ) {
131  l = std::max(l,x[i].min());
132  u = std::min(u,x[i].max());
133  }
134  for (int i=x.size(); i--; ) {
135  GECODE_ME_CHECK(x[i].gq(home,l));
136  GECODE_ME_CHECK(x[i].lq(home,u));
137  }
138  (void) new (home) NaryEq<View>(home,x);
139  }
140  return ES_OK;
141  }
142 
143  template<class View>
146  : NaryPropagator<View,PC_FLOAT_BND>(home,share,p) {}
147 
148  template<class View>
149  Actor*
150  NaryEq<View>::copy(Space& home, bool share) {
151  return new (home) NaryEq<View>(home,share,*this);
152  }
153 
154  template<class View>
155  PropCost
156  NaryEq<View>::cost(const Space&, const ModEventDelta& med) const {
157  if (View::me(med) == ME_FLOAT_VAL)
159  else
160  return PropCost::linear(PropCost::LO, x.size());
161  }
162 
163  template<class View>
164  ExecStatus
166  assert(x.size() > 2);
167  if (View::me(med) == ME_FLOAT_VAL) {
168  // One of the variables is assigned
169  for (int i = 0; ; i++)
170  if (x[i].assigned()) {
171  FloatVal n = x[i].val();
172  x.move_lst(i);
173  for (int j = x.size(); j--; )
174  GECODE_ME_CHECK(x[j].eq(home,n));
175  return home.ES_SUBSUMED(*this);
176  }
177  GECODE_NEVER;
178  }
179 
180  FloatNum mn = x[0].min();
181  restart_min:
182  for (int i = x.size(); i--; ) {
183  GECODE_ME_CHECK(x[i].gq(home,mn));
184  if (mn < x[i].min()) {
185  mn = x[i].min();
186  goto restart_min;
187  }
188  }
189  FloatNum mx = x[0].max();
190  restart_max:
191  for (int i = x.size(); i--; ) {
192  GECODE_ME_CHECK(x[i].lq(home,mx));
193  if (mx > x[i].max()) {
194  mx = x[i].max();
195  goto restart_max;
196  }
197  }
198  return x[0].assigned() ? home.ES_SUBSUMED(*this) : ES_FIX;
199  }
200 
201 
202 
203  /*
204  * Reified bounds consistent equality
205  *
206  */
207 
208  template<class View, class CtrlView, ReifyMode rm>
210  ReEq<View,CtrlView,rm>::ReEq(Home home, View x0, View x1, CtrlView b)
211  : Int::ReBinaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,x0,x1,b) {}
212 
213  template<class View, class CtrlView, ReifyMode rm>
214  ExecStatus
215  ReEq<View,CtrlView,rm>::post(Home home, View x0, View x1, CtrlView b){
216  if (b.one()) {
217  if (rm == RM_PMI)
218  return ES_OK;
219  return Eq<View,View>::post(home,x0,x1);
220  }
221  if (b.zero()) {
222  if (rm == RM_IMP)
223  return ES_OK;
224  return Nq<View,View>::post(home,x0,x1);
225  }
226  if (!same(x0,x1)) {
227  (void) new (home) ReEq(home,x0,x1,b);
228  } else if (rm != RM_IMP) {
229  GECODE_ME_CHECK(b.one(home));
230  }
231  return ES_OK;
232  }
233 
234 
235  template<class View, class CtrlView, ReifyMode rm>
238  : Int::ReBinaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,share,p) {}
239 
240  template<class View, class CtrlView, ReifyMode rm>
241  Actor*
242  ReEq<View,CtrlView,rm>::copy(Space& home, bool share) {
243  return new (home) ReEq<View,CtrlView,rm>(home,share,*this);
244  }
245 
246  template<class View, class CtrlView, ReifyMode rm>
247  ExecStatus
249  if (b.one()) {
250  if (rm == RM_PMI)
251  return home.ES_SUBSUMED(*this);
252  GECODE_REWRITE(*this,(Eq<View,View>::post(home(*this),x0,x1)));
253  }
254  if (b.zero()) {
255  if (rm == RM_IMP)
256  return home.ES_SUBSUMED(*this);
257  GECODE_REWRITE(*this,(Nq<View,View>::post(home(*this),x0,x1)));
258  }
259  switch (rtest_eq(x0,x1)) {
260  case RT_TRUE:
261  if (rm != RM_IMP)
262  GECODE_ME_CHECK(b.one_none(home));
263  break;
264  case RT_FALSE:
265  if (rm != RM_PMI)
266  GECODE_ME_CHECK(b.zero_none(home));
267  break;
268  case RT_MAYBE:
269  return ES_FIX;
270  default: GECODE_NEVER;
271  }
272  return home.ES_SUBSUMED(*this);
273  }
274 
275 
276  /*
277  * Reified bounds consistent equality (one variable)
278  *
279  */
280 
281  template<class View, class CtrlView, ReifyMode rm>
284  (Home home, View x, FloatVal c0, CtrlView b)
286 
287  template<class View, class CtrlView, ReifyMode rm>
288  ExecStatus
289  ReEqFloat<View,CtrlView,rm>::post(Home home, View x, FloatVal c, CtrlView b) {
290  if (b.one()) {
291  if (rm != RM_PMI)
292  GECODE_ME_CHECK(x.eq(home,c));
293  } else if (x.assigned()) {
294  if (overlap(x.val(),c)) {
295  if (rm != RM_IMP)
296  GECODE_ME_CHECK(b.one(home));
297  } else {
298  if (rm != RM_PMI)
299  GECODE_ME_CHECK(b.zero(home));
300  }
301  } else {
302  (void) new (home) ReEqFloat(home,x,c,b);
303  }
304  return ES_OK;
305  }
306 
307 
308  template<class View, class CtrlView, ReifyMode rm>
311  : Int::ReUnaryPropagator<View,PC_FLOAT_BND,CtrlView>(home,share,p), c(p.c) {}
312 
313  template<class View, class CtrlView, ReifyMode rm>
314  Actor*
316  return new (home) ReEqFloat<View,CtrlView,rm>(home,share,*this);
317  }
318 
319  template<class View, class CtrlView, ReifyMode rm>
320  ExecStatus
322  if (b.one()) {
323  if (rm != RM_PMI)
324  GECODE_ME_CHECK(x0.eq(home,c));
325  } else {
326  switch (rtest_eq(x0,c)) {
327  case RT_TRUE:
328  if (rm != RM_IMP)
329  GECODE_ME_CHECK(b.one(home));
330  break;
331  case RT_FALSE:
332  if (rm != RM_PMI)
333  GECODE_ME_CHECK(b.zero(home));
334  break;
335  case RT_MAYBE:
336  return ES_FIX;
337  default: GECODE_NEVER;
338  }
339  }
340  return home.ES_SUBSUMED(*this);
341  }
342 
343 
344 }}}
345 
346 // STATISTICS: float-prop
Reified binary bounds consistent equality propagator.
Definition: rel.hh:129
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:109
NNF * l
Left subtree.
Definition: bool-expr.cpp:244
Inverse implication for reification.
Definition: int.hh:847
static PropCost linear(PropCost::Mod m, unsigned int n)
Linear complexity for modifier pcm and size measure n.
Definition: core.hpp:4041
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:2973
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:57
bool overlap(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:502
Reified binary propagator.
Definition: propagator.hpp:89
Binary bounds consistent equality propagator.
Definition: rel.hh:70
Relation does hold.
Definition: view.hpp:498
Base-class for propagators.
Definition: core.hpp:755
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: eq.hpp:242
Relation does not hold.
Definition: view.hpp:496
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: eq.hpp:321
const Gecode::ModEvent ME_FLOAT_VAL
Domain operation has resulted in a value (assigned variable)
Definition: var-type.hpp:264
Propagation has computed fixpoint.
Definition: core.hpp:528
static PropCost unary(PropCost::Mod m)
Single variable for modifier pcm.
Definition: core.hpp:4058
void unique(const Space &home)
Remove all duplicate views from array (changes element order)
Definition: array.hpp:1498
Computation spaces.
Definition: core.hpp:1362
NaryEq(Space &home, bool share, NaryEq< View > &p)
Constructor for cloning p.
Definition: eq.hpp:145
static ExecStatus post(Home home, View x, FloatVal c, CtrlView b)
Post bounds consistent propagator .
Definition: eq.hpp:289
Base-class for both propagators and branchers.
Definition: core.hpp:666
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: eq.hpp:248
Reified bounds consistent equality with float propagator.
Definition: rel.hh:155
static ExecStatus post(Home home, View0 x0, View1 x1)
Post bounds consistent propagator .
Definition: eq.hpp:54
Binary bounds consistent disequality propagator.
Definition: rel.hh:183
Gecode::FloatVal c(-8, 8)
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
const FloatNum min
Smallest allowed float value.
Definition: float.hh:833
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Eq(Space &home, bool share, Eq< View0, View1 > &p)
Constructor for cloning p.
Definition: eq.hpp:71
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: eq.hpp:315
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: eq.hpp:150
n-ary propagator
Definition: propagator.hpp:143
static ExecStatus post(Home home, ViewArray< View > &x)
Post bounds consistent propagator .
Definition: eq.hpp:123
View arrays.
Definition: array.hpp:234
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:45
union Gecode::@518::NNF::@57 u
Union depending on nodetype t.
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:75
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: eq.hpp:83
Float value type.
Definition: float.hh:321
RelTest rtest_eq(View x, View y)
Test whether views x and y are equal.
Definition: rel-test.hpp:44
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
Mixed binary propagator.
Definition: propagator.hpp:203
Propagation cost.
Definition: core.hpp:537
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: eq.hpp:165
ExecStatus
Definition: core.hpp:523
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:47
static ExecStatus post(Home home, View x0, View x1, CtrlView b)
Post bounds consistent propagator .
Definition: eq.hpp:215
#define forceinline
Definition: config.hpp:132
static ExecStatus post(Home home, View0 x0, View1 x1)
Post bounds consistent propagator .
Definition: nq.hpp:53
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: eq.hpp:89
ReEqFloat(Space &home, bool share, ReEqFloat &p)
Constructor for cloning p.
Definition: eq.hpp:310
Execution is okay.
Definition: core.hpp:527
const Gecode::PropCond PC_FLOAT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:292
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1215
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
Gecode toplevel namespace
ReEq(Space &home, bool share, ReEq &p)
Constructor for cloning p.
Definition: eq.hpp:237
Implication for reification.
Definition: int.hh:840
n-ary bounds consistent equality propagator
Definition: rel.hh:98
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function.
Definition: eq.hpp:156
Relation may hold or not.
Definition: view.hpp:497
int ModEventDelta
Modification event deltas.
Definition: core.hpp:173
Home class for posting propagators
Definition: core.hpp:717
double FloatNum
Floating point number base type.
Definition: float.hh:108
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60