| 2097 | } |
| 2098 | |
| 2099 | expr expr::load(const expr &idx, uint64_t max_idx) const { |
| 2100 | C(idx); |
| 2101 | |
| 2102 | // TODO: add support for alias analysis plugin |
| 2103 | expr array, str_idx, val; |
| 2104 | if (isStore(array, str_idx, val)) { // store(array, idx, val) |
| 2105 | uint64_t str_idx_val; |
| 2106 | // loaded idx can't possibly match the stored idx; there's UB otherwise |
| 2107 | if (str_idx.isUInt(str_idx_val) && str_idx_val > max_idx) |
| 2108 | return array.load(idx, max_idx); |
| 2109 | |
| 2110 | expr cmp = idx == str_idx; |
| 2111 | if (cmp.isTrue()) |
| 2112 | return val; |
| 2113 | |
| 2114 | auto loaded = array.load(idx, max_idx); |
| 2115 | if (cmp.isFalse() || val.eq(loaded)) |
| 2116 | return loaded; |
| 2117 | |
| 2118 | } else if (isConstArray(val)) { |
| 2119 | return val; |
| 2120 | } else if (isLambda(val)) { |
| 2121 | return val.subst_var(idx).foldTopLevel(); |
| 2122 | } |
| 2123 | |
| 2124 | return Z3_mk_select(ctx(), ast(), idx()); |
| 2125 | } |
| 2126 | |
| 2127 | expr expr::mkIf(const expr &cond, const expr &then, const expr &els) { |
| 2128 | C2(cond, then, els); |