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
Hashertdzdd::PathCounter::Hasher55 Hasher(Spec const& spec, int level)
56 : spec(spec), level(level) {
57 }
58
operator ()tdzdd::PathCounter::Hasher59 size_t operator()(Word const* p) const {
60 return spec.hash_code(state(p), level);
61 }
62
operator ()tdzdd::PathCounter::Hasher63 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
numWords(int n)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
state(Word * p)79 static void* state(Word* p) {
80 return p;
81 }
82
state(Word const * p)83 static void const* state(Word const* p) {
84 return p;
85 }
86
number(Word * p) const87 BigNumber number(Word* p) const {
88 return BigNumber(p + stateWords);
89 }
90
number64(Word * p) const91 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 // }
PathCounter(S & s)98 PathCounter(S& s)
99 : spec(s), stateWords(numWords(spec.datasize())) {
100 }
101
count()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
countFast()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
count64()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
435 /**
436 * Counts the number of paths from the root to the 1-terminal
437 * without building entire DD structure.
438 * This function uses arbitrary-precision integer for counting.
439 * @param spec DD specification.
440 * @param fast @p true to select a faster algorithm instead of a memory-efficient one.
441 */
442 template<typename S>
countPaths(S & spec,bool fast=false)443 std::string countPaths(S& spec, bool fast = false) {
444 PathCounter<S> pc(spec);
445 return fast ? pc.countFast() : pc.count();
446 }
447
448 /**
449 * Counts the number of paths from the root to the 1-terminal
450 * without building entire DD structure.
451 * This function uses unsigned 64-bit integer for counting.
452 * @param spec DD specification.
453 */
454 template<typename S>
countPaths64(S & spec)455 uint64_t countPaths64(S& spec) {
456 return PathCounter<S>(spec).count64();
457 }
458
459 } // namespace tdzdd
460