| 2250 | } |
| 2251 | |
| 2252 | expr expr::subst(const vector<pair<expr, expr>> &repls) const { |
| 2253 | C(); |
| 2254 | if (repls.empty()) |
| 2255 | return *this; |
| 2256 | |
| 2257 | auto from = make_unique<Z3_ast[]>(repls.size()); |
| 2258 | auto to = make_unique<Z3_ast[]>(repls.size()); |
| 2259 | |
| 2260 | unsigned i = 0; |
| 2261 | for (auto &p : repls) { |
| 2262 | C2(p.first, p.second); |
| 2263 | from[i] = p.first(); |
| 2264 | to[i] = p.second(); |
| 2265 | ++i; |
| 2266 | } |
| 2267 | return Z3_substitute(ctx(), ast(), repls.size(), from.get(), to.get()); |
| 2268 | } |
| 2269 | |
| 2270 | expr expr::subst_simplify(const vector<pair<expr, expr>> &repls) const { |
| 2271 | if (repls.empty()) |
no test coverage detected