| 2201 | } |
| 2202 | |
| 2203 | expr expr::mkLambda(const expr &var, const char *var_name, const expr &val) { |
| 2204 | C2(var, val); |
| 2205 | |
| 2206 | if (!val.vars().count(var)) |
| 2207 | return mkConstArray(var, val); |
| 2208 | |
| 2209 | expr array, idx; |
| 2210 | if (val.isLoad(array, idx) && idx.eq(var)) |
| 2211 | return array; |
| 2212 | |
| 2213 | auto sort = var.sort(); |
| 2214 | auto name = Z3_mk_string_symbol(ctx(), var_name); |
| 2215 | return Z3_mk_lambda(ctx(), 1, &sort, &name, val()); |
| 2216 | } |
| 2217 | |
| 2218 | expr expr::simplify() const { |
| 2219 | C(); |