| 2228 | } |
| 2229 | |
| 2230 | expr expr::foldTopLevel() const { |
| 2231 | expr cond, then, els; |
| 2232 | if (isIf(cond, then, els)) |
| 2233 | return |
| 2234 | expr::mkIf(cond.foldTopLevel(), then.foldTopLevel(), els.foldTopLevel()); |
| 2235 | |
| 2236 | expr array, idx; |
| 2237 | if (isLoad(array, idx) && idx.isConst()) |
| 2238 | return array.load(idx); |
| 2239 | |
| 2240 | if (isApp()) { |
| 2241 | bool is_const = true; |
| 2242 | for (unsigned i = 0, e = getFnNumArgs(); i < e; ++i) { |
| 2243 | if (!(is_const &= getFnArg(i).isConst())) |
| 2244 | break; |
| 2245 | } |
| 2246 | if (is_const) |
| 2247 | return simplifyNoTimeout(); |
| 2248 | } |
| 2249 | return *this; |
| 2250 | } |
| 2251 | |
| 2252 | expr expr::subst(const vector<pair<expr, expr>> &repls) const { |
| 2253 | C(); |