| 2002 | } |
| 2003 | |
| 2004 | expr expr::float2BV() const { |
| 2005 | if (auto app = isAppOf(Z3_OP_FPA_TO_FP)) // ((_ to_fp e s) BV) |
| 2006 | if (Z3_get_app_num_args(ctx(), app) == 1) |
| 2007 | return Z3_get_app_arg(ctx(), app, 0); |
| 2008 | |
| 2009 | return unop_fold(Z3_mk_fpa_to_ieee_bv); |
| 2010 | } |
| 2011 | |
| 2012 | expr expr::float2Real() const { |
| 2013 | return unop_fold(Z3_mk_fpa_to_real); |