| 1326 | } |
| 1327 | |
| 1328 | expr expr::round(const expr &rm) const { |
| 1329 | C(rm); |
| 1330 | return |
| 1331 | simplify_const(Z3_mk_fpa_round_to_integral(ctx(), rm(), ast()), *this); |
| 1332 | } |
| 1333 | |
| 1334 | expr expr::foeq(const expr &rhs) const { |
| 1335 | return binop_commutative(rhs, Z3_mk_fpa_eq); |