| 487 | } |
| 488 | |
| 489 | bool expr::isConcat(expr &a, expr &b) const { |
| 490 | if (auto app = isAppOf(Z3_OP_CONCAT)) { |
| 491 | auto nargs = Z3_get_app_num_args(ctx(), app); |
| 492 | assert(nargs >= 2); |
| 493 | a = Z3_get_app_arg(ctx(), app, 0); |
| 494 | b = Z3_get_app_arg(ctx(), app, 1); |
| 495 | for (unsigned i = 2; i < nargs; ++i) { |
| 496 | b = b.concat(Z3_get_app_arg(ctx(), app, i)); |
| 497 | } |
| 498 | return true; |
| 499 | } |
| 500 | return false; |
| 501 | } |
| 502 | |
| 503 | bool expr::isExtract(expr &e, unsigned &high, unsigned &low) const { |
| 504 | if (auto app = isAppOf(Z3_OP_EXTRACT)) { |
no test coverage detected