| 663 | } |
| 664 | |
| 665 | expr expr::binop_commutative(const expr &rhs, |
| 666 | Z3_ast (*op)(Z3_context, Z3_ast, Z3_ast), |
| 667 | expr (expr::*expr_op)(const expr &) const, |
| 668 | bool (expr::*identity)() const, |
| 669 | bool (expr::*absorvent)() const, |
| 670 | int z3_app) const { |
| 671 | if ((this->*absorvent)() || (rhs.*identity)()) |
| 672 | return *this; |
| 673 | |
| 674 | if ((rhs.*absorvent)() || (this->*identity)()) |
| 675 | return rhs; |
| 676 | |
| 677 | if (z3_app) { |
| 678 | if (isConst()) { |
| 679 | auto app = rhs.isAppOf(z3_app); |
| 680 | if (app && Z3_get_app_num_args(ctx(), app) == 2) { |
| 681 | expr app_a = Z3_get_app_arg(ctx(), app, 0); |
| 682 | expr app_b = Z3_get_app_arg(ctx(), app, 1); |
| 683 | if (app_a.isConst()) |
| 684 | return ((this->*expr_op)(app_a).*expr_op)(app_b); |
| 685 | if (app_b.isConst()) |
| 686 | return ((this->*expr_op)(app_b).*expr_op)(app_a); |
| 687 | } |
| 688 | } |
| 689 | else if (rhs.isConst()) |
| 690 | return rhs.binop_commutative(*this, op, expr_op, identity, absorvent, |
| 691 | z3_app); |
| 692 | } |
| 693 | |
| 694 | return binop_commutative(rhs, op); |
| 695 | } |
| 696 | |
| 697 | expr expr::binop_commutative(const expr &rhs, |
| 698 | Z3_ast(*op)(Z3_context, Z3_ast, Z3_ast)) const { |
nothing calls this directly
no test coverage detected