| 2363 | } |
| 2364 | |
| 2365 | set<expr> expr::leafs(unsigned max) const { |
| 2366 | C(); |
| 2367 | vector<expr> worklist = { *this }; |
| 2368 | unordered_set<Z3_ast> seen; |
| 2369 | set<expr> ret; |
| 2370 | do { |
| 2371 | auto val = std::move(worklist.back()); |
| 2372 | worklist.pop_back(); |
| 2373 | if (!seen.emplace(val()).second) |
| 2374 | continue; |
| 2375 | |
| 2376 | expr cond, then, els, e, array, idx; |
| 2377 | unsigned high, low; |
| 2378 | if (val.isIf(cond, then, els)) { |
| 2379 | worklist.emplace_back(std::move(then)); |
| 2380 | worklist.emplace_back(std::move(els)); |
| 2381 | } else if (val.isExtract(e, high, low) && e.isIf(cond, then, els)) { |
| 2382 | worklist.emplace_back(then.extract(high, low)); |
| 2383 | worklist.emplace_back(els.extract(high, low)); |
| 2384 | } else if (val.isLoad(array, idx)) { |
| 2385 | if (array.isStore(array, idx, e)) { |
| 2386 | worklist.emplace_back(array.load(idx)); |
| 2387 | worklist.emplace_back(std::move(e)); |
| 2388 | } else if (array.isIf(cond, then, els)) { |
| 2389 | worklist.emplace_back(then.load(idx)); |
| 2390 | worklist.emplace_back(els.load(idx)); |
| 2391 | } else { |
| 2392 | ret.emplace(std::move(val)); |
| 2393 | } |
| 2394 | } else { |
| 2395 | ret.emplace(std::move(val)); |
| 2396 | } |
| 2397 | |
| 2398 | if (ret.size() + worklist.size() >= max) { |
| 2399 | for (auto &v : worklist) |
| 2400 | ret.emplace(std::move(v)); |
| 2401 | break; |
| 2402 | } |
| 2403 | } while (!worklist.empty()); |
| 2404 | |
| 2405 | return ret; |
| 2406 | } |
| 2407 | |
| 2408 | set<expr> expr::get_apps_of(const char *fn_name, const char *prefix) const { |
| 2409 | C(); |