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" 49 typedef uint64_t Word;
55 Hasher(Spec
const& spec,
int level)
56 : spec(spec), level(level) {
59 size_t operator()(Word
const* p)
const {
60 return spec.hash_code(state(p), level);
63 size_t operator()(Word
const* p, Word
const* q)
const {
64 return spec.equal_to(state(p), state(q), level);
68 typedef MyHashTable<Word*,Hasher,Hasher> UniqTable;
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);
79 static void* state(Word* p) {
83 static void const* state(Word
const* p) {
87 BigNumber number(Word* p)
const {
88 return BigNumber(p + stateWords);
91 uint64_t& number64(Word* p)
const {
99 : spec(s), stateWords(numWords(spec.datasize())) {
102 std::string count() {
104 mh.begin(typenameof(spec));
106 MyVector<Word> tmp(stateWords + 1);
107 Word* ptmp = tmp.data();
108 int const n = spec.get_root(state(ptmp));
112 return (n == 0) ?
"0" :
"1";
115 std::vector<uint64_t> totalStorage(n / 63 + 1);
116 BigNumber total(totalStorage.data());
121 MemoryPools pools(n + 1);
122 MyVector<MyList<Word> > vnodeTable(n + 1);
123 MyVector<UniqTable> uniqTable;
124 MyVector<Hasher> hasher;
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()));
134 Word* p0 = vnodeTable[n].alloc_front(stateWords + 1);
135 spec.get_copy(state(p0), state(ptmp));
136 spec.destruct(state(ptmp));
140 for (
int i = n; i > 0; --i) {
141 MyList<Word>& vnodes = vnodeTable[i];
142 size_t m = vnodes.size();
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);
152 for (; !vnodes.empty(); vnodes.pop_front()) {
153 Word* p = vnodes.front();
154 if (number(p) == 0) {
155 spec.destruct(state(p));
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);
164 spec.destruct(state(pp));
166 total.add(number(p));
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));
175 Word* qqq = uniqTable[ii].add(qq);
178 number(qqq).store(number(p));
181 spec.destruct(state(qq));
182 int w = number(qqq).add(number(p));
183 if (numberWords < w) {
186 vnodeTable[ii].pop_front();
191 Word* ppp = nextUniq.add(pp);
194 number(ppp).store(number(p));
195 pp = nextVnodes.alloc_front(nextWords);
198 spec.destruct(state(pp));
199 int w = number(ppp).add(number(p));
200 if (numberWords < w) {
207 spec.destruct(state(p));
210 nextVnodes.pop_front();
213 spec.destructLevel(i);
221 std::string countFast() {
223 mh.begin(typenameof(spec));
225 MyVector<Word> tmp(stateWords + 1);
226 Word* ptmp = tmp.data();
227 int const n = spec.get_root(state(ptmp));
231 return (n == 0) ?
"0" :
"1";
234 std::vector<uint64_t> totalStorage(n / 63 + 1);
235 BigNumber total(totalStorage.data());
240 MemoryPools pools(n + 1);
241 MyVector<MyList<Word> > vnodeTable(n + 1);
244 Word* p0 = vnodeTable[n].alloc_front(stateWords + 1);
245 spec.get_copy(state(p0), state(ptmp));
246 spec.destruct(state(ptmp));
250 for (
int i = n; i > 0; --i) {
251 MyList<Word>& vnodes = vnodeTable[i];
255 Hasher hasher(spec, i);
256 UniqTable uniq(vnodes.size(), hasher, hasher);
258 for (MyList<Word>::iterator t = vnodes.begin();
259 t != vnodes.end(); ++t) {
261 Word* pp = uniq.add(p);
267 int w = number(pp).add(number(p));
268 if (numberWords < w) {
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);
282 for (; !vnodes.empty(); vnodes.pop_front()) {
283 Word* p = vnodes.front();
284 if (number(p) == 0) {
285 spec.destruct(state(p));
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);
294 spec.destruct(state(pp));
296 total.add(number(p));
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));
308 number(pp).store(number(p));
309 pp = nextVnodes.alloc_front(nextWords);
313 spec.destruct(state(p));
316 nextVnodes.pop_front();
318 spec.destructLevel(i);
328 mh.begin(typenameof(spec));
330 MyVector<Word> tmp(stateWords + 1);
331 Word* ptmp = tmp.data();
332 int const n = spec.get_root(state(ptmp));
336 return (n == 0) ? 0 : 1;
343 MemoryPools pools(n + 1);
344 MyVector<MyList<Word> > vnodeTable(n + 1);
345 MyVector<UniqTable> uniqTable;
346 MyVector<Hasher> hasher;
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()));
355 Word* p0 = vnodeTable[n].alloc_front(stateWords + 1);
356 spec.get_copy(state(p0), state(ptmp));
357 spec.destruct(state(ptmp));
361 for (
int i = n; i > 0; --i) {
362 MyList<Word>& vnodes = vnodeTable[i];
363 size_t m = vnodes.size();
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);
372 for (; !vnodes.empty(); vnodes.pop_front()) {
373 Word* p = vnodes.front();
374 if (number64(p) == 0) {
375 spec.destruct(state(p));
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);
384 spec.destruct(state(pp));
386 total += number64(p);
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));
394 Word* qqq = uniqTable[ii].add(qq);
397 number64(qqq) = number64(p);
400 spec.destruct(state(qq));
401 number64(qqq) += number64(p);
402 vnodeTable[ii].pop_front();
407 Word* ppp = nextUniq.add(pp);
410 number64(ppp) = number64(p);
411 pp = nextVnodes.alloc_front(stateWords + 1);
414 spec.destruct(state(pp));
415 number64(ppp) += number64(p);
420 spec.destruct(state(p));
423 nextVnodes.pop_front();
426 spec.destructLevel(i);
443 std::string countPaths(S& spec,
bool fast =
false) {
444 PathCounter<S> pc(spec);
445 return fast ? pc.countFast() : pc.count();
455 uint64_t countPaths64(S& spec) {
456 return PathCounter<S>(spec).count64();