mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 07:23:58 +00:00
Code Activity

fpa2bv_approx: added fp.abs, fixed rounding mode model extraction

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-02 18:17:49 +01:00
parent 65a6845945
commit 610c549104
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/tactic/fpa/fpa2bv_approx_tactic.cpp
View file

@ -272,8 +272,12 @@ class fpa2bv_approx_tactic: public tactic {
expr_ref arg_e[] = { expr_ref(m), expr_ref(m), expr_ref(m), expr_ref(m) }; expr_ref arg_e[] = { expr_ref(m), expr_ref(m), expr_ref(m), expr_ref(m) };
unsigned i=0; unsigned i=0;
//Set rounding mode //Set rounding mode
if (rhs->get_num_args() > 0 && m_float_util.is_rm(rhs->get_arg(0))) if (rhs->get_num_args() > 0 && m_float_util.is_rm(rhs->get_arg(0))) {
expr_ref rm_val(m);
mdl->eval(rhs->get_arg(0), rm_val, true);
m_float_util.is_rm_numeral(rm_val, rm);
i = 1; i = 1;
}
//Collect argument values //Collect argument values
for (; i < rhs->get_num_args(); i++) { for (; i < rhs->get_num_args(); i++) {
expr * arg = rhs->get_arg(i); expr * arg = rhs->get_arg(i);
@ -372,6 +376,11 @@ class fpa2bv_approx_tactic: public tactic {
mpf_mngr.set(est_rhs_value, ebits, sbits, rm, est_arg_val[1]); mpf_mngr.set(est_rhs_value, ebits, sbits, rm, est_arg_val[1]);
break; break;
} }
case OP_FPA_ABS:
{
mpf_mngr.abs(arg_val[0], rhs_value);
break;
}
default: default:
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;