| 274 | } |
| 275 | |
| 276 | bool expr::isBinOp(expr &a, expr &b, int z3op) const { |
| 277 | if (auto app = isAppOf(z3op)) { |
| 278 | if (Z3_get_app_num_args(ctx(), app) != 2) |
| 279 | return false; |
| 280 | a = Z3_get_app_arg(ctx(), app, 0); |
| 281 | b = Z3_get_app_arg(ctx(), app, 1); |
| 282 | return true; |
| 283 | } |
| 284 | return false; |
| 285 | } |
| 286 | |
| 287 | bool expr::isTernaryOp(expr &a, expr &b, expr &c, int z3op) const { |
| 288 | if (auto app = isAppOf(z3op)) { |