| 142 | } |
| 143 | |
| 144 | Z3_ast Z3_API Z3_mk_lambda(Z3_context c, |
| 145 | unsigned num_decls, Z3_sort const types[], |
| 146 | Z3_symbol const decl_names[], |
| 147 | Z3_ast body) { |
| 148 | |
| 149 | Z3_TRY; |
| 150 | LOG_Z3_mk_lambda(c, num_decls, types, decl_names, body); |
| 151 | RESET_ERROR_CODE(); |
| 152 | expr_ref result(mk_c(c)->m()); |
| 153 | if (num_decls == 0) { |
| 154 | SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); |
| 155 | RETURN_Z3(nullptr); |
| 156 | } |
| 157 | |
| 158 | sort* const* ts = reinterpret_cast<sort * const*>(types); |
| 159 | svector<symbol> names; |
| 160 | for (unsigned i = 0; i < num_decls; ++i) { |
| 161 | names.push_back(to_symbol(decl_names[i])); |
| 162 | } |
| 163 | result = mk_c(c)->m().mk_lambda(names.size(), ts, names.data(), to_expr(body)); |
| 164 | mk_c(c)->save_ast_trail(result.get()); |
| 165 | RETURN_Z3(of_ast(result.get())); |
| 166 | Z3_CATCH_RETURN(nullptr); |
| 167 | } |
| 168 | |
| 169 | Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, |
| 170 | unsigned num_decls, Z3_app const vars[], |