19 bvt new_fraction=
prop.new_variables(fraction.size());
20 bvt new_exponent=
prop.new_variables(exponent.size());
23 for(
unsigned i=0; i<fraction.size(); i++)
28 for(
unsigned j=0; j<i; j++)
30 !fraction[fraction.size()-1-j]);
33 equal.push_back(fraction[fraction.size()-1-i]);
46 bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
50 bv_utils.build_constant(-
static_cast<int>(i), exponent.size());
51 bvt added_exponent=
bv_utils.add(exponent, adjustment);
52 bv_utils.cond_implies_equal(shift, added_exponent, new_exponent);
60 bv_utils.cond_implies_equal(fraction_all_zero, zero_fraction, new_fraction);
62 fraction=new_fraction;
63 exponent=new_exponent;