TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
DegreeConstraint.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 <cstring>
29 #include <iostream>
30 #include <map>
31 #include <vector>
32 
33 #include "../DdSpec.hpp"
34 #include "../util/Graph.hpp"
35 #include "../util/IntSubset.hpp"
36 
37 namespace tdzdd {
38 
39 class DegreeConstraint: public PodArrayDdSpec<DegreeConstraint,int16_t,2> {
40  typedef int16_t Mate;
41 
42  Graph const& graph;
43  std::vector<IntSubset const*> constraints;
44  int const n;
45  int const mateSize;
46  bool const lookahead;
47 
48  void shiftMate(Mate* mate, int d) const {
49  assert(d >= 0);
50  if (d > 0) {
51  std::memmove(mate, mate + d, (mateSize - d) * sizeof(*mate));
52  for (int k = mateSize - d; k < mateSize; ++k) {
53  mate[k] = 0;
54  }
55  }
56  }
57 
58  bool takable(IntSubset const* c, Mate degree, bool final) const {
59  if (c == 0) return true;
60  if (degree >= c->upperBound()) return false;
61  return !final || c->contains(degree + 1);
62  }
63 
64  bool leavable(IntSubset const* c, Mate degree, bool final) const {
65  if (c == 0) return true;
66  return !final || c->contains(degree);
67  }
68 
69 public:
70  DegreeConstraint(Graph const& graph, IntSubset const* c = 0, bool lookahead = true)
71  : graph(graph), n(graph.edgeSize()),
72  mateSize(graph.maxFrontierSize()), lookahead(lookahead) {
73  setArraySize(mateSize);
74 
75  int m = graph.vertexSize();
76  constraints.resize(m + 1);
77  for (int v = 1; v <= m; ++v) {
78  constraints[v] = c;
79  }
80  }
81 
82  void setConstraint(Graph::VertexNumber v, IntSubset const* c) {
83  if (v < 1 || graph.vertexSize() < v) throw std::runtime_error(
84  "ERROR: Vertex number is out of range");
85  constraints[v] = c;
86  }
87 
88  void setConstraint(std::string v, IntSubset const* c) {
89  constraints[graph.getVertex(v)] = c;
90  }
91 
92  int getRoot(Mate* mate) const {
93  for (int k = 0; k < mateSize; ++k) {
94  mate[k] = 0;
95  }
96  return n;
97  }
98 
99  int getChild(Mate* mate, int level, int take) const {
100  assert(1 <= level && level <= n);
101  int i = n - level;
102  Graph::EdgeInfo const& e = graph.edgeInfo(i);
103  Mate& w1 = mate[e.v1 - e.v0];
104  Mate& w2 = mate[e.v2 - e.v0];
105  IntSubset const* c1 = constraints[e.v1];
106  IntSubset const* c2 = constraints[e.v2];
107  assert(e.v1 <= e.v2);
108 
109  if (take) {
110  if (!takable(c1, w1, e.v1final)) return 0;
111  if (!takable(c2, w2, e.v2final)) return 0;
112  if (c1) ++w1;
113  if (c2) ++w2;
114  }
115  else {
116  if (!leavable(c1, w1, e.v1final)) return 0;
117  if (!leavable(c2, w2, e.v2final)) return 0;
118  }
119 
120  if (e.v1final) w1 = 0;
121  if (e.v2final) w2 = 0;
122 
123  if (++i == n) return -1;
124  shiftMate(mate, graph.edgeInfo(i).v0 - e.v0);
125 
126  while (lookahead) {
127  Graph::EdgeInfo const& e = graph.edgeInfo(i);
128  Mate& w1 = mate[e.v1 - e.v0];
129  Mate& w2 = mate[e.v2 - e.v0];
130  IntSubset const* c1 = constraints[e.v1];
131  IntSubset const* c2 = constraints[e.v2];
132  assert(e.v1 <= e.v2);
133 
134  if (takable(c1, w1, e.v1final) && takable(c2, w2, e.v2final)) break;
135  if (!leavable(c1, w1, e.v1final)) return 0;
136  if (!leavable(c2, w2, e.v2final)) return 0;
137 
138  if (e.v1final) w1 = 0;
139  if (e.v2final) w2 = 0;
140 
141  if (++i == n) return -1;
142  shiftMate(mate, graph.edgeInfo(i).v0 - e.v0);
143  }
144 
145  assert(i < n);
146  return n - i;
147  }
148 };
149 
150 } // namespace tdzdd