mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

New implementation of mpf_manager::rem.

Browse source 
Partially addresses #561
This commit is contained in:
Christoph M. Wintersteiger 2016-05-12 14:15:24 +01:00
parent ed1861d90d
commit dd83495d5d
2 changed files with 152 additions and 106 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/util/mpf.h
View file

@ -223,7 +223,8 @@ protected:
void round(mpf_rounding_mode rm, mpf & o);
void round_sqrt(mpf_rounding_mode rm, mpf & o);
void prem(scoped_mpf & x, scoped_mpf const & y, mpf_exp_t const & exp_diff, bool partial);
void renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig);
void partial_remainder(scoped_mpf & x, scoped_mpf const & y, mpf_exp_t const & exp_diff, bool partial);
void mk_round_inf(mpf_rounding_mode rm, mpf & o);