TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
SizeConstraint.hpp
1 /*
2  * TdZdd: a Top-down/Breadth-first Decision Diagram Manipulation Framework
3  * by Hiroaki Iwashita <iwashita@erato.ist.hokudai.ac.jp>
4  * Copyright (c) 2014 ERATO MINATO Project
5  *
6  * Permission is hereby granted, free of charge, to any person obtaining a
7  * copy of this software and associated documentation files (the "Software"),
8  * to deal in the Software without restriction, including without limitation
9  * the rights to use, copy, modify, merge, publish, distribute, sublicense,
10  * and/or sell copies of the Software, and to permit persons to whom the
11  * Software is furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be included in
14  * all copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21  * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
22  * DEALINGS IN THE SOFTWARE.
23  */
24 
25 #pragma once
26 
27 #include <cassert>
28 #include <iostream>
29 
30 #include "../DdSpec.hpp"
31 #include "../util/IntSubset.hpp"
32 
33 namespace tdzdd {
34 
35 class SizeConstraint: public DdSpec<SizeConstraint,int,2> {
36  int const n;
37  IntSubset const* const constraint;
38 
39 public:
40  SizeConstraint(int n, IntSubset const& constraint)
41  : n(n), constraint(&constraint) {
42  assert(n >= 1);
43  }
44 
45  SizeConstraint(int n, IntSubset const* constraint)
46  : n(n), constraint(constraint) {
47  assert(n >= 1);
48  }
49 
50  int getRoot(int& count) const {
51  count = 0;
52  return (constraint && n < constraint->lowerBound()) ? 0 : n;
53  }
54 
55  int getChild(int& count, int level, int value) const {
56  if (constraint == 0) return (--level >= 1) ? level : -1;
57 
58  if (value) {
59  if (count >= constraint->upperBound()) return 0;
60  ++count;
61  }
62  else {
63  if (count + level <= constraint->lowerBound()) return 0;
64  }
65 
66  return (--level >= 1) ? level : constraint->contains(count) ? -1 : 0;
67  }
68 };
69 
70 } // namespace tdzdd