SheafSystem  0.0.0.0
poset_bounds.cc
1 
2 //
3 // Copyright (c) 2014 Limit Point Systems, Inc.
4 //
5 // Licensed under the Apache License, Version 2.0 (the "License");
6 // you may not use this file except in compliance with the License.
7 // You may obtain a copy of the License at
8 //
9 // http://www.apache.org/licenses/LICENSE-2.0
10 //
11 // Unless required by applicable law or agreed to in writing, software
12 // distributed under the License is distributed on an "AS IS" BASIS,
13 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
14 // See the License for the specific language governing permissions and
15 // limitations under the License.
16 //
17 
18 // Implementation for class poset_bounds
19 
20 #include "SheafSystem/poset_bounds.h"
21 
22 #include "SheafSystem/assert_contract.h"
23 
24 // ===========================================================
25 // ANY FACET
26 // ===========================================================
27 
30 clone() const
31 {
32  poset_bounds* result;
33 
34  // Preconditions:
35 
36 
37  // Body:
38 
39  result = new poset_bounds(*this);
40 
41  // Postconditions:
42 
43  // Exit:
44 
45  return result;
46 }
47 
48 bool
50 invariant() const
51 {
52  bool result = true;
53 
54  // Preconditions:
55 
56  // Body:
57 
58  // Must satisfy base class invariant
59 
60  result = result && any::invariant();
61 
62  if(invariant_check())
63  {
64  // Prevent recursive calls to invariant
65 
67 
68  // Finished, turn invariant checking back on.
69 
71  }
72 
73  // Postconditions:
74 
75  // Exit
76 
77  return result;
78 }
79 
80 bool
82 is_ancestor_of(const any* other) const
83 {
84 
85  // Preconditions:
86 
87  require(other != 0);
88 
89  // Body:
90 
91  // True if other conforms to this
92 
93  bool result = dynamic_cast<const poset_bounds*>(other) != 0;
94 
95  // Postconditions:
96 
97  return result;
98 
99 }
100 
101 // ===========================================================
102 // POSET_BOUNDS FACET
103 // ===========================================================
104 
107 {
108 
109  // Preconditions:
110 
111  // Body:
112 
113  _lb = 0;
114  _lb_is_singleton = false;
115  _bounded_below = false;
116 
117  _ub = 0;
118  _ub_is_singleton = false;
119  _bounded_above = false;
120 
121  // Postconditions:
122 
123  ensure(invariant());
124 
125  // Exit:
126 
127  return;
128 }
129 
132  : _descriptor(xother._descriptor)
133 {
134  // Preconditions:
135 
136  // Body:
137 
138  switch(_descriptor.mode())
139  {
140  case poset_bounds_descriptor::MEMBER_MEMBER:
141  _lb = (xother._lb != 0) ? new zn_to_bool(*xother._lb) : 0;
142  _lb_is_singleton = true;
143 
144  _bounded_below = (lb_id() != BOTTOM_INDEX);
145 
146  _ub = (xother._ub != 0) ? new zn_to_bool(*xother._ub) : 0;
147  _ub_is_singleton = true;
148 
149  _bounded_above = (ub_id() != TOP_INDEX);
150 
151  break;
152 
153  case poset_bounds_descriptor::MEMBER_SUBPOSET:
154  _lb = (xother._lb != 0) ? new zn_to_bool(*xother._lb) : 0;
155  _lb_is_singleton = true;
156 
157  _bounded_below = (lb_id() != BOTTOM_INDEX);
158 
159  _ub = xother._ub;
160  _ub_is_singleton = false;
161  _bounded_above = true;
162 
163  break;
164 
165  case poset_bounds_descriptor::SUBPOSET_MEMBER:
166  _lb = xother._lb;
167  _lb_is_singleton = false;
168  _bounded_below = true;
169 
170  _ub = (xother._ub != 0) ? new zn_to_bool(*xother._ub) : 0;
171  _ub_is_singleton = true;
172 
173  _bounded_above = (ub_id() != TOP_INDEX);
174 
175  break;
176 
177  case poset_bounds_descriptor::SUBPOSET_SUBPOSET:
178  _lb = xother._lb;
179  _lb_is_singleton = false;
180  _bounded_below = true;
181 
182  _ub = xother._ub;
183  _ub_is_singleton = false;
184  _bounded_above = true;
185 
186  break;
187 
188  default:
189  post_fatal_error_message("unrecognized specification mode");
190  break;
191  }
192 
193  // Postconditions:
194 
195  ensure(invariant());
196 }
197 
200  : _descriptor(xdesc)
201 {
202  // Preconditions:
203 
204 
205  // Body:
206 
207  switch(_descriptor.mode())
208  {
209  case poset_bounds_descriptor::MEMBER_MEMBER:
210  _lb = 0;
211  _lb_is_singleton = true;
212 
213  _bounded_below = (lb_id() != BOTTOM_INDEX);
214 
215  _ub = 0;
216  _ub_is_singleton = true;
217 
218  _bounded_above = (ub_id() != TOP_INDEX);
219 
220  break;
221 
222  case poset_bounds_descriptor::MEMBER_SUBPOSET:
223  _lb = 0;
224  _lb_is_singleton = true;
225 
226  _bounded_below = (lb_id() != BOTTOM_INDEX);
227 
228  _ub = 0;
229  _ub_is_singleton = false;
230  _bounded_above = true;
231 
232  break;
233 
234  case poset_bounds_descriptor::SUBPOSET_MEMBER:
235  _lb = 0;
236  _lb_is_singleton = false;
237  _bounded_below = true;
238 
239  _ub = 0;
240  _ub_is_singleton = true;
241 
242  _bounded_above = (ub_id() != TOP_INDEX);
243 
244  break;
245 
246  case poset_bounds_descriptor::SUBPOSET_SUBPOSET:
247  _lb = 0;
248  _lb_is_singleton = false;
249  _bounded_below = true;
250 
251  _ub = 0;
252  _ub_is_singleton = false;
253  _bounded_above = true;
254 
255  break;
256 
257  default:
258  post_fatal_error_message("unrecognized specification mode");
259  break;
260  }
261 
262  // Postconditions:
263 
264  // Exit:
265 
266  return;
267 }
268 
271 {
272 
273  // Preconditions:
274 
275  // Body:
276 
277  // Postconditions:
278 
279  // Exit:
280 
281  return;
282 }
283 
284 
287 descriptor() const
288 {
289  return _descriptor;
290 }
291 
294 mode() const
295 {
296  return _descriptor.mode();
297 }
298 
299 
302 lb_id() const
303 {
304  return _descriptor.lb_id();
305 }
306 
307 void
310 {
311  // Preconditions:
312 
313  require(lb_is_singleton());
314 
315  // Body:
316 
317  _descriptor.put_lb_id(xlb_id);
318 
319  // Postconditions:
320 
321  ensure(lb_id() == xlb_id);
322 
323  // Exit
324 
325  return;
326 }
327 
328 void
330 put_lb_id(const scoped_index& xlb_id)
331 {
332  // Preconditions:
333 
334  require(lb_is_singleton());
335 
336  // Body:
337 
338  _descriptor.put_lb_id(xlb_id.hub_pod());
339 
340  // Postconditions:
341 
342  ensure(lb_id() == xlb_id.hub_pod());
343 
344  // Exit
345 
346  return;
347 }
348 
349 bool
352 {
353 
354  // Preconditions:
355 
356  // Body:
357 
358  // Postconditions:
359 
360  // Exit
361 
362  return _lb_is_singleton;
363 }
364 
365 bool
368 {
369  // Preconditions:
370 
371  // Body:
372 
373  // Postconditions:
374 
375  // Exit
376 
377  return _bounded_below;
378 }
379 
382 ub_id() const
383 {
384  return _descriptor.ub_id();
385 }
386 
387 void
390 {
391  // Preconditions:
392 
393  require(ub_is_singleton());
394 
395  // Body:
396 
397  _descriptor.put_ub_id(xub_id);
398 
399  // Postconditions:
400 
401  ensure(ub_id() == xub_id);
402 
403  // Exit
404 
405  return;
406 }
407 
408 void
410 put_ub_id(const scoped_index& xub_id)
411 {
412  // Preconditions:
413 
414  require(ub_is_singleton());
415 
416  // Body:
417 
418  _descriptor.put_ub_id(xub_id.hub_pod());
419 
420  // Postconditions:
421 
422  ensure(ub_id() == xub_id.hub_pod());
423 
424  // Exit
425 
426  return;
427 }
428 
429 bool
432 {
433 
434  // Preconditions:
435 
436  // Body:
437 
438  // Postconditions:
439 
440  // Exit
441 
442  return _ub_is_singleton;
443 }
444 
445 bool
448 {
449  bool result;
450 
451  // Preconditions:
452 
453  // Body:
454 
457 
458  result = !_ub_is_singleton;
459 
460  // Postconditions:
461 
462  // Exit
463 
464  return result;
465 }
466 
467 bool
470 {
471  // Preconditions:
472 
473  // Body:
474 
475  // Postconditions:
476 
477  // Exit
478 
479  return _bounded_above;
480 }
481 
482 
483 
484 // PROTECTED MEMBER FUNCTIONS
485 
virtual bool invariant() const
Class invariant, intended to be redefined in each descendant. See below for template for invariant in...
Definition: any.cc:153
bool _bounded_below
True if the lower bound is not the bottom.
Definition: poset_bounds.h:202
pod_index_type ub_id() const
The index of the upper bound member, if the upper bound contains a single member. ...
bool lb_is_singleton() const
True if the lower bound contains a single member.
bool bounded_below() const
True if the lower bound is not the bottom.
bool _bounded_above
True if the upper bound is not the top.
Definition: poset_bounds.h:217
void put_lb_id(pod_index_type xlb_id)
Sets the index of the lower bound member to xlb_ib, if the lower bound contains a single member...
pod_index_type ub_id() const
The index of the upper bound member, if the upper bound contains a single member. ...
A (lower, upper) bounds pair for a poset. Specifies a portion of a poset for a bounded i/o operation...
Definition: poset_bounds.h:50
void put_lb_id(pod_index_type xlb_id)
Sets the index of the lower bound to xlb_id.
poset_bounds_descriptor::specification_mode mode() const
The specification mode.
void put_ub_id(pod_index_type xub_id)
Sets the index of the upper bound member to xub_ib, if the upper bound contains a single member...
Abstract base class with useful features for all objects.
Definition: any.h:39
A map from Zn (the integers mod n) to bools. A characteristic function used to represent subsets of Z...
Definition: zn_to_bool.h:52
specification_mode
Enumeration for mode of specifying the lower and upper bounds.
virtual ~poset_bounds()
Destructor.
bool _ub_is_singleton
True if the upper bound contains a single member.
Definition: poset_bounds.h:212
An index within the external ("client") scope of a given id space.
Definition: scoped_index.h:116
bool _lb_is_singleton
True if the lower bound contains a single member.
Definition: poset_bounds.h:197
pod_index_type lb_id() const
The index of the lower bound.
bool ub_is_decomposition() const
True if the join of the members of the upper bound is equal to the external schema.
bool ub_is_singleton() const
True if the upper bound contains a single member.
void disable_invariant_check() const
Disable invariant check. Intended for preventing recursive calls to invariant and for suppressing inv...
Definition: any.h:97
zn_to_bool * _lb
The lower bound.
Definition: poset_bounds.h:192
zn_to_bool * _ub
The upper bound.
Definition: poset_bounds.h:207
A description of a (lower, upper) bounds pair for a poset. Specifies a portion of a poset for a bound...
bool bounded_above() const
True if the upper bound is not the top.
bool invariant_check() const
True if invariant checking is enabled.
Definition: any.h:79
int_type pod_index_type
The plain old data index type.
Definition: pod_types.h:49
virtual bool is_ancestor_of(const any *other) const
Conformance test; true if other conforms to this.
Definition: poset_bounds.cc:82
pod_index_type lb_id() const
The index of the lower bound member, if the lower bound contains a single member. ...
poset_bounds()
Default constructor.
virtual poset_bounds_descriptor descriptor() const
A descriptor for this.
poset_bounds_descriptor _descriptor
A descriptor for this.
Definition: poset_bounds.h:187
void enable_invariant_check() const
Enable invariant checking.
Definition: any.h:87
void put_ub_id(pod_index_type xub_id)
Sets the index of the upper bound to xub_id.
virtual poset_bounds * clone() const
Virtual constructor; makes a new instance of the same type as this.
Definition: poset_bounds.cc:30
specification_mode mode() const
Specification mode for this.
virtual bool invariant() const
Class invariant.
Definition: poset_bounds.cc:50
pod_type hub_pod() const
The pod value of this mapped to the unglued hub id space.
Definition: scoped_index.h:710