| 2172 | } |
| 2173 | |
| 2174 | expr expr::mkForAll(const set<expr> &vars, expr &&val) { |
| 2175 | if (vars.empty() || val.isConst() || !val.isValid()) |
| 2176 | return std::move(val); |
| 2177 | |
| 2178 | auto vars_ast = make_unique<Z3_app[]>(vars.size()); |
| 2179 | unsigned i = 0; |
| 2180 | for (auto &v : vars) { |
| 2181 | vars_ast[i++] = (Z3_app)v(); |
| 2182 | } |
| 2183 | return Z3_mk_forall_const(ctx(), 0, vars.size(), vars_ast.get(), 0, nullptr, |
| 2184 | val()); |
| 2185 | } |
| 2186 | |
| 2187 | expr expr::mkForAll(unsigned num_vars, const expr *vars, const char **names, |
| 2188 | expr &&val) { |