TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
PathCounter.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 <ostream>
29 #include <stdexcept>
30 #include <string>
31 #include <utility>
32 #include <vector>
33 
34 #include "../util/BigNumber.hpp"
35 #include "../util/demangle.hpp"
36 #include "../util/MessageHandler.hpp"
37 #include "../util/MemoryPool.hpp"
38 #include "../util/MyHashTable.hpp"
39 #include "../util/MyList.hpp"
40 #include "../util/MyVector.hpp"
41 #include "../DdSpec.hpp"
42 
43 namespace tdzdd {
44 
45 template<typename S>
46 class PathCounter {
47  //typedef typename std::remove_const<typename std::remove_reference<S>::type>::type Spec;
48  typedef S Spec;
49  typedef uint64_t Word;
50 
51  struct Hasher {
52  Spec const& spec;
53  int const level;
54 
55  Hasher(Spec const& spec, int level)
56  : spec(spec), level(level) {
57  }
58 
59  size_t operator()(Word const* p) const {
60  return spec.hash_code(state(p), level);
61  }
62 
63  size_t operator()(Word const* p, Word const* q) const {
64  return spec.equal_to(state(p), state(q), level);
65  }
66  };
67 
68  typedef MyHashTable<Word*,Hasher,Hasher> UniqTable;
69 
70  Spec& spec;
71  int const stateWords;
72 
73  static int numWords(int n) {
74  if (n < 0) throw std::runtime_error(
75  "storage size is not initialized!!!");
76  return (n + sizeof(Word) - 1) / sizeof(Word);
77  }
78 
79  static void* state(Word* p) {
80  return p;
81  }
82 
83  static void const* state(Word const* p) {
84  return p;
85  }
86 
87  BigNumber number(Word* p) const {
88  return BigNumber(p + stateWords);
89  }
90 
91  uint64_t& number64(Word* p) const {
92  return p[stateWords];
93  }
94 
95 public:
96 // PathCounter(S&& s): spec(std::forward<S>(s)), hasher(spec), stateWords(numWords(spec.datasize())) {
97 // }
98  PathCounter(S& s)
99  : spec(s), stateWords(numWords(spec.datasize())) {
100  }
101 
102  std::string count() {
103  MessageHandler mh;
104  mh.begin(typenameof(spec));
105 
106  MyVector<Word> tmp(stateWords + 1);
107  Word* ptmp = tmp.data();
108  int const n = spec.get_root(state(ptmp));
109  if (n <= 0) {
110  mh << " ...";
111  mh.end(0);
112  return (n == 0) ? "0" : "1";
113  }
114 
115  std::vector<uint64_t> totalStorage(n / 63 + 1);
116  BigNumber total(totalStorage.data());
117  total.store(0);
118  size_t maxWidth = 0;
119  //std::cerr << "\nLevel,Width\n";
120 
121  MemoryPools pools(n + 1);
122  MyVector<MyList<Word> > vnodeTable(n + 1);
123  MyVector<UniqTable> uniqTable;
124  MyVector<Hasher> hasher;
125 
126  uniqTable.reserve(n + 1);
127  hasher.reserve(n + 1);
128  for (int i = 0; i <= n; ++i) {
129  hasher.push_back(Hasher(spec, i));
130  uniqTable.push_back(UniqTable(hasher.back(), hasher.back()));
131  }
132 
133  int numberWords = 1;
134  Word* p0 = vnodeTable[n].alloc_front(stateWords + 1);
135  spec.get_copy(state(p0), state(ptmp));
136  spec.destruct(state(ptmp));
137  number(p0).store(1);
138 
139  mh.setSteps(n);
140  for (int i = n; i > 0; --i) {
141  MyList<Word>& vnodes = vnodeTable[i];
142  size_t m = vnodes.size();
143 
144  //std::cerr << i << "," << m << "\n";
145  maxWidth = std::max(maxWidth, m);
146  MyList<Word>& nextVnodes = vnodeTable[i - 1];
147  UniqTable& nextUniq = uniqTable[i - 1];
148  int const nextWords = stateWords + numberWords + 1;
149  Word* pp = nextVnodes.alloc_front(nextWords);
150  //if (nextUniq.size() < m) nextUniq.rehash(m);
151 
152  for (; !vnodes.empty(); vnodes.pop_front()) {
153  Word* p = vnodes.front();
154  if (number(p) == 0) {
155  spec.destruct(state(p));
156  continue;
157  }
158 
159  for (int b = 0; b < Spec::ARITY; ++b) {
160  spec.get_copy(state(pp), state(p));
161  int ii = spec.get_child(state(pp), i, b);
162 
163  if (ii <= 0) {
164  spec.destruct(state(pp));
165  if (ii != 0) {
166  total.add(number(p));
167  }
168  }
169  else if (ii < i - 1) {
170  Word* qq = vnodeTable[ii].alloc_front(
171  nextWords + (i - ii) / 63);
172  spec.get_copy(state(qq), state(pp));
173  spec.destruct(state(pp));
174 
175  Word* qqq = uniqTable[ii].add(qq);
176 
177  if (qqq == qq) {
178  number(qqq).store(number(p));
179  }
180  else {
181  spec.destruct(state(qq));
182  int w = number(qqq).add(number(p));
183  if (numberWords < w) {
184  numberWords = w; //FIXME might be broken at long skip
185  }
186  vnodeTable[ii].pop_front();
187  }
188  }
189  else {
190  assert(ii == i - 1);
191  Word* ppp = nextUniq.add(pp);
192 
193  if (ppp == pp) {
194  number(ppp).store(number(p));
195  pp = nextVnodes.alloc_front(nextWords);
196  }
197  else {
198  spec.destruct(state(pp));
199  int w = number(ppp).add(number(p));
200  if (numberWords < w) {
201  numberWords = w; //FIXME might be broken at long skip
202  }
203  }
204  }
205  }
206 
207  spec.destruct(state(p));
208  }
209 
210  nextVnodes.pop_front();
211  nextUniq.clear();
212  pools[i].clear();
213  spec.destructLevel(i);
214  mh.step();
215  }
216 
217  mh.end(maxWidth);
218  return total;
219  }
220 
221  std::string countFast() {
222  MessageHandler mh;
223  mh.begin(typenameof(spec));
224 
225  MyVector<Word> tmp(stateWords + 1);
226  Word* ptmp = tmp.data();
227  int const n = spec.get_root(state(ptmp));
228  if (n <= 0) {
229  mh << " ...";
230  mh.end(0);
231  return (n == 0) ? "0" : "1";
232  }
233 
234  std::vector<uint64_t> totalStorage(n / 63 + 1);
235  BigNumber total(totalStorage.data());
236  total.store(0);
237  size_t maxWidth = 0;
238  //std::cerr << "\nLevel,Width\n";
239 
240  MemoryPools pools(n + 1);
241  MyVector<MyList<Word> > vnodeTable(n + 1);
242 
243  int numberWords = 1;
244  Word* p0 = vnodeTable[n].alloc_front(stateWords + 1);
245  spec.get_copy(state(p0), state(ptmp));
246  spec.destruct(state(ptmp));
247  number(p0).store(1);
248 
249  mh.setSteps(n);
250  for (int i = n; i > 0; --i) {
251  MyList<Word>& vnodes = vnodeTable[i];
252  size_t m = 0;
253 
254  {
255  Hasher hasher(spec, i);
256  UniqTable uniq(vnodes.size(), hasher, hasher);
257 
258  for (MyList<Word>::iterator t = vnodes.begin();
259  t != vnodes.end(); ++t) {
260  Word* p = *t;
261  Word* pp = uniq.add(p);
262 
263  if (pp == p) {
264  ++m;
265  }
266  else {
267  int w = number(pp).add(number(p));
268  if (numberWords < w) {
269  numberWords = w; //FIXME might be broken at long skip
270  }
271  number(p).store(0);
272  }
273  }
274  }
275 
276  //std::cerr << i << "," << m << "\n";
277  maxWidth = std::max(maxWidth, m);
278  MyList<Word>& nextVnodes = vnodeTable[i - 1];
279  int const nextWords = stateWords + numberWords + 1;
280  Word* pp = nextVnodes.alloc_front(nextWords);
281 
282  for (; !vnodes.empty(); vnodes.pop_front()) {
283  Word* p = vnodes.front();
284  if (number(p) == 0) {
285  spec.destruct(state(p));
286  continue;
287  }
288 
289  for (int b = 0; b < Spec::ARITY; ++b) {
290  spec.get_copy(state(pp), state(p));
291  int ii = spec.get_child(state(pp), i, b);
292 
293  if (ii <= 0) {
294  spec.destruct(state(pp));
295  if (ii != 0) {
296  total.add(number(p));
297  }
298  }
299  else if (ii < i - 1) {
300  Word* ppp = vnodeTable[ii].alloc_front(
301  nextWords + (i - ii) / 63);
302  spec.get_copy(state(ppp), state(pp));
303  spec.destruct(state(pp));
304  number(ppp).store(number(p));
305  }
306  else {
307  assert(ii == i - 1);
308  number(pp).store(number(p));
309  pp = nextVnodes.alloc_front(nextWords);
310  }
311  }
312 
313  spec.destruct(state(p));
314  }
315 
316  nextVnodes.pop_front();
317  pools[i].clear();
318  spec.destructLevel(i);
319  mh.step();
320  }
321 
322  mh.end(maxWidth);
323  return total;
324  }
325 
326  uint64_t count64() {
327  MessageHandler mh;
328  mh.begin(typenameof(spec));
329 
330  MyVector<Word> tmp(stateWords + 1);
331  Word* ptmp = tmp.data();
332  int const n = spec.get_root(state(ptmp));
333  if (n <= 0) {
334  mh << " ...";
335  mh.end(0);
336  return (n == 0) ? 0 : 1;
337  }
338 
339  uint64_t total = 0;
340  size_t maxWidth = 0;
341  //std::cerr << "\nLevel,Width\n";
342 
343  MemoryPools pools(n + 1);
344  MyVector<MyList<Word> > vnodeTable(n + 1);
345  MyVector<UniqTable> uniqTable;
346  MyVector<Hasher> hasher;
347 
348  uniqTable.reserve(n + 1);
349  hasher.reserve(n + 1);
350  for (int i = 0; i <= n; ++i) {
351  hasher.push_back(Hasher(spec, i));
352  uniqTable.push_back(UniqTable(hasher.back(), hasher.back()));
353  }
354 
355  Word* p0 = vnodeTable[n].alloc_front(stateWords + 1);
356  spec.get_copy(state(p0), state(ptmp));
357  spec.destruct(state(ptmp));
358  number64(p0) = 1;
359 
360  mh.setSteps(n);
361  for (int i = n; i > 0; --i) {
362  MyList<Word>& vnodes = vnodeTable[i];
363  size_t m = vnodes.size();
364 
365  //std::cerr << i << "," << m << "\n";
366  maxWidth = std::max(maxWidth, m);
367  MyList<Word>& nextVnodes = vnodeTable[i - 1];
368  UniqTable& nextUniq = uniqTable[i - 1];
369  Word* pp = nextVnodes.alloc_front(stateWords + 1);
370  //if (nextUniq.size() < m) nextUniq.rehash(m);
371 
372  for (; !vnodes.empty(); vnodes.pop_front()) {
373  Word* p = vnodes.front();
374  if (number64(p) == 0) {
375  spec.destruct(state(p));
376  continue;
377  }
378 
379  for (int b = 0; b < Spec::ARITY; ++b) {
380  spec.get_copy(state(pp), state(p));
381  int ii = spec.get_child(state(pp), i, b);
382 
383  if (ii <= 0) {
384  spec.destruct(state(pp));
385  if (ii != 0) {
386  total += number64(p);
387  }
388  }
389  else if (ii < i - 1) {
390  Word* qq = vnodeTable[ii].alloc_front(stateWords + 1);
391  spec.get_copy(state(qq), state(pp));
392  spec.destruct(state(pp));
393 
394  Word* qqq = uniqTable[ii].add(qq);
395 
396  if (qqq == qq) {
397  number64(qqq) = number64(p);
398  }
399  else {
400  spec.destruct(state(qq));
401  number64(qqq) += number64(p);
402  vnodeTable[ii].pop_front();
403  }
404  }
405  else {
406  assert(ii == i - 1);
407  Word* ppp = nextUniq.add(pp);
408 
409  if (ppp == pp) {
410  number64(ppp) = number64(p);
411  pp = nextVnodes.alloc_front(stateWords + 1);
412  }
413  else {
414  spec.destruct(state(pp));
415  number64(ppp) += number64(p);
416  }
417  }
418  }
419 
420  spec.destruct(state(p));
421  }
422 
423  nextVnodes.pop_front();
424  nextUniq.clear();
425  pools[i].clear();
426  spec.destructLevel(i);
427  mh.step();
428  }
429 
430  mh.end(maxWidth);
431  return total;
432  }
433 };
434 
442 template<typename S>
443 std::string countPaths(S& spec, bool fast = false) {
444  PathCounter<S> pc(spec);
445  return fast ? pc.countFast() : pc.count();
446 }
447 
454 template<typename S>
455 uint64_t countPaths64(S& spec) {
456  return PathCounter<S>(spec).count64();
457 }
458 
459 } // namespace tdzdd