Generated on Tue Jan 26 2021 00:00:00 for Gecode by doxygen 1.9.1
narrowing.hpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Patrick Pekczynski <pekczynski@ps.uni-sb.de>
5  *
6  * Copyright:
7  * Patrick Pekczynski, 2004
8  *
9  * This file is part of Gecode, the generic constraint
10  * development environment:
11  * http://www.gecode.org
12  *
13  * Permission is hereby granted, free of charge, to any person obtaining
14  * a copy of this software and associated documentation files (the
15  * "Software"), to deal in the Software without restriction, including
16  * without limitation the rights to use, copy, modify, merge, publish,
17  * distribute, sublicense, and/or sell copies of the Software, and to
18  * permit persons to whom the Software is furnished to do so, subject to
19  * the following conditions:
20  *
21  * The above copyright notice and this permission notice shall be
22  * included in all copies or substantial portions of the Software.
23  *
24  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31  *
32  */
33 
34 namespace Gecode { namespace Int { namespace Sorted {
35 
52  template<class View>
53  inline void
55  int phi[], SccComponent sinfo[], int scclist[]) {
56 
57  // number of sccs is bounded by xs (number of x-nodes)
58  int xs = x.size();
59  Region r;
61 
62  //select an y node from the graph
63  for (int j = 0; j < xs; j++) {
64  int yjmin = y[j].min(); // the processed min
65  while (!cs.empty() && x[phi[sinfo[cs.top()].rightmost]].max() < yjmin) {
66  // the topmost scc cannot "reach" y_j or a node to the right of it
67  cs.pop();
68  }
69 
70  // a component has the form C(y-Node, matching x-Node)
71  // C is a minimal scc in the oriented intersection graph
72  // we only store y_j-Node, since \phi(j) gives the matching X-node
73  int i = phi[j];
74  int ximin = x[i].min();
75  while (!cs.empty() && ximin <= y[sinfo[cs.top()].rightmost].max()) {
76  // y_j can "reach" cs.top() ,
77  // i.e. component c can reach component cs.top()
78  // merge c and cs.top() into new component
79  int top = cs.top();
80  // connecting
81  sinfo[sinfo[j].leftmost].left = top;
82  sinfo[top].right = sinfo[j].leftmost;
83  // moving leftmost
84  sinfo[j].leftmost = sinfo[top].leftmost;
85  // moving rightmost
86  sinfo[sinfo[top].leftmost].rightmost = j;
87  cs.pop();
88  }
89  cs.push(j);
90  }
91  cs.reset();
92 
93 
94  // now we mark all components with the respective scc-number
95  // labeling is bound by O(k) which is bound by O(n)
96 
97  for (int i = 0; i < xs; i++) {
98  if (sinfo[i].left == i) { // only label variables in sccs
99  int scc = sinfo[i].rightmost;
100  int z = i;
101  //bound by the size of the largest scc = k
102  while (sinfo[z].right != z) {
103  sinfo[z].rightmost = scc;
104  scclist[phi[z]] = scc;
105  z = sinfo[z].right;
106  }
107  sinfo[z].rightmost = scc;
108  scclist[phi[z]] = scc;
109  }
110  }
111  }
112 
128  template<class View, bool Perm>
129  inline bool
132  ViewArray<View>& y,
133  ViewArray<View>& z,
134  int tau[],
135  int[],
136  int scclist[],
137  SccComponent sinfo[],
138  bool& nofix) {
139 
140  int xs = x.size();
141 
142  // For every x node
143  for (int i = 0; i < xs; i++) {
144 
145  int xmin = x[i].min();
146  /*
147  * take the scc-list for the current x node
148  * start from the leftmost reachable y node of the scc
149  * and check which Y node in the scc is
150  * really the rightmost node intersecting x, i.e.
151  * search for the greatest lower bound of x
152  */
153  int start = sinfo[scclist[i]].leftmost;
154  while (y[start].max() < xmin) {
155  start = sinfo[start].right;
156  }
157 
158  if (Perm) {
159  // start is the leftmost-position for x_i
160  // that denotes the lower bound on p_i
161 
162  ModEvent me_plb = z[i].gq(home, start);
163  if (me_failed(me_plb)) {
164  return false;
165  }
166  nofix |= (me_modified(me_plb) && start != z[i].min());
167  }
168 
169  ModEvent me_lb = x[i].gq(home, y[start].min());
170  if (me_failed(me_lb)) {
171  return false;
172  }
173  nofix |= (me_modified(me_lb) &&
174  y[start].min() != x[i].min());
175 
176  int ptau = tau[xs - 1 - i];
177  int xmax = x[ptau].max();
178  /*
179  * take the scc-list for the current x node
180  * start from the rightmost reachable node and check which
181  * y node in the scc is
182  * really the rightmost node intersecting x, i.e.
183  * search for the smallest upper bound of x
184  */
185  start = sinfo[scclist[ptau]].rightmost;
186  while (y[start].min() > xmax) {
187  start = sinfo[start].left;
188  }
189 
190  if (Perm) {
191  //start is the rightmost-position for x_i
192  //that denotes the upper bound on p_i
193  ModEvent me_pub = z[ptau].lq(home, start);
194  if (me_failed(me_pub)) {
195  return false;
196  }
197  nofix |= (me_modified(me_pub) && start != z[ptau].max());
198  }
199 
200  ModEvent me_ub = x[ptau].lq(home, y[start].max());
201  if (me_failed(me_ub)) {
202  return false;
203  }
204  nofix |= (me_modified(me_ub) &&
205  y[start].max() != x[ptau].max());
206  }
207  return true;
208  }
209 
220  template<class View>
221  inline bool
224  int phi[], int phiprime[], bool& nofix) {
225  for (int i=x.size(); i--; ) {
226  ModEvent me_lb = y[i].gq(home, x[phiprime[i]].min());
227  if (me_failed(me_lb)) {
228  return false;
229  }
230  nofix |= (me_modified(me_lb) &&
231  x[phiprime[i]].min() != y[i].min());
232 
233  ModEvent me_ub = y[i].lq(home, x[phi[i]].max());
234  if (me_failed(me_ub)) {
235  return false;
236  }
237  nofix |= (me_modified(me_ub) &&
238  x[phi[i]].max() != y[i].max());
239  }
240  return true;
241  }
242 
243 }}}
244 
245 // STATISTICS: int-prop
246 
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:249
NNF * r
Right subtree.
Definition: bool-expr.cpp:242
Representation of a strongly connected component.
Definition: sortsup.hpp:53
int leftmost
Leftmost y-node in a scc.
Definition: sortsup.hpp:56
int left
Direct left neighbour of an y-node in a scc.
Definition: sortsup.hpp:58
int right
Direct right neighbour of an y-node in a scc.
Definition: sortsup.hpp:60
int rightmost
Rightmost reachable y-node in a scc.
Definition: sortsup.hpp:62
Handle to region.
Definition: region.hpp:55
Computation spaces.
Definition: core.hpp:1742
Stack with fixed number of elements.
void push(const T &x)
Push element x on top of stack.
void reset(void)
Reset stack (pop all elements)
T pop(void)
Pop topmost element from stack and return it.
bool empty(void) const
Test whether stack is empty.
T & top(void) const
Return element on top of stack.
View arrays.
Definition: array.hpp:253
int ModEvent
Type for modification events.
Definition: core.hpp:62
Post propagator for SetVar SetOpType SetVar SetRelType SetVar z
Definition: set.hh:767
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
bool me_failed(ModEvent me)
Check whether modification event me is failed.
Definition: modevent.hpp:54
bool me_modified(ModEvent me)
Check whether modification event me describes variable modification.
Definition: modevent.hpp:59
const FloatNum max
Largest allowed float value.
Definition: float.hh:844
const FloatNum min
Smallest allowed float value.
Definition: float.hh:846
bool narrow_domy(Space &home, ViewArray< View > &x, ViewArray< View > &y, int phi[], int phiprime[], bool &nofix)
Narrowing the domains of the y views.
Definition: narrowing.hpp:222
bool narrow_domx(Space &home, ViewArray< View > &x, ViewArray< View > &y, ViewArray< View > &z, int tau[], int[], int scclist[], SccComponent sinfo[], bool &nofix)
Narrowing the domains of the x variables.
Definition: narrowing.hpp:130
void computesccs(ViewArray< View > &x, ViewArray< View > &y, int phi[], SccComponent sinfo[], int scclist[])
Compute the sccs of the oriented intersection-graph.
Definition: narrowing.hpp:54
Gecode::IntArgs i({1, 2, 3, 4})