27     typedef typename fmanager::numeral numeral;  typedef
35     numeral           m_tmp1;
36     numeral           m_one;
38     void check(numeral const & n) { if (!m().is_regular(n)) throw exception(); }  in check()
66     double to_double(numeral & x) const { return m().to_double(x); }  in to_double()
68     void del(numeral & x) { m().del(x); }  in del()
70     void abs(numeral & o) { m().abs(o); }  in abs()
71     void abs(numeral const & x, numeral & o) { m().abs(x, o); }  in abs()
73     void neg(numeral & o) { m().neg(o); }  in neg()
74     void neg(numeral const & x, numeral & o) { m().neg(x, o); }  in neg()
76     bool is_zero(numeral const & x) { return m().is_zero(x); }  in is_zero()
77 …bool is_neg(numeral const & x) { return m().is_neg(x) && !m().is_zero(x); /* it is not clear wheth…  in is_neg()
78     bool is_pos(numeral const & x) { return m().is_pos(x) && !m().is_zero(x); }  in is_pos()
79     bool is_nonneg(numeral const & x) { return !is_neg(x); }  in is_nonneg()
80     bool is_nonpos(numeral const & x) { return !is_pos(x); }  in is_nonpos()
82     void set(numeral & o, int value) { m().set(o, m_ebits, m_sbits, value); check(o); }  in set()
83     void set(numeral & o, int n, int d) { m().set(o, m_ebits, m_sbits, m_mode, n, d); check(o); }  in set()
84     void set(numeral & o, double x) { m().set(o, m_ebits, m_sbits, x); check(o); }  in set()
85     void set(numeral & o, unsigned value) { m().set(o, m_ebits, m_sbits, (double)value); check(o); }  in set()
86     void set(numeral & o, numeral const & x) { m().set(o, x); check(o); }  in set()
87     void set(numeral & o, mpq const & x) { m().set(o, m_ebits, m_sbits, m_mode, x); check(o); }  in set()
88     void reset(numeral & o) { m().reset(o, m_ebits, m_sbits); }  in reset()
89     static void swap(numeral & x, numeral & y) { x.swap(y); }  in swap()
91 …void add(numeral const & x, numeral const & y, numeral & o) { m().add(m_mode, x, y, o); check(o); }  in add()
92 …void sub(numeral const & x, numeral const & y, numeral & o) { m().sub(m_mode, x, y, o); check(o); }  in sub()
93 …void mul(numeral const & x, numeral const & y, numeral & o) { m().mul(m_mode, x, y, o); check(o); }  in mul()
94 …void div(numeral const & x, numeral const & y, numeral & o) { m().div(m_mode, x, y, o); check(o); }  in div()
95     void inv(numeral & o) { numeral a; set(a, 1); div(a, o, o); del(a);  check(o); }  in inv()
96     void inv(numeral const & x, numeral & o) { set(o, x); inv(o); }  in inv()
97     void inc(numeral & x) { add(x, m_one, x); }  in inc()
98     void dec(numeral & x) { sub(x, m_one, x); }  in dec()
100     void power(numeral const & a, unsigned p, numeral & b) {  in power()
102         numeral power;  in power()
117     void floor(numeral const & a, numeral & b) {  in floor()
135     void ceil(numeral const & a, numeral & b) {  in ceil()
150     unsigned prev_power_of_two(numeral const & a) { return m().prev_power_of_two(a); }  in prev_power_of_two()
152     bool eq(numeral const & x, numeral const & y) { return m().eq(x, y); }  in eq()
153     bool lt(numeral const & x, numeral const & y) { return m().lt(x, y); }  in lt()
154     bool le(numeral const & x, numeral const & y) { return m().le(x, y); }  in le()
155     bool gt(numeral const & x, numeral const & y) { return m().gt(x, y); }  in gt()
156     bool ge(numeral const & x, numeral const & y) { return m().ge(x, y); }  in ge()
158     bool is_int(numeral const & x) { return m().is_int(x); }  in is_int()
159     bool is_one(numeral const & x) { return m().is_one(x); }  in is_one()
160 …bool is_minus_one(numeral const & x) { numeral & _x = const_cast<numeral &>(x); m().neg(_x); bool …  in is_minus_one()
162     std::string to_string(numeral const & a) { return m().to_string(a); }  in to_string()
163     std::string to_rational_string(numeral const & a) { return m().to_rational_string(a); }  in to_rational_string()
164     void display(std::ostream & out, numeral const & a) { out << to_string(a); }  in display()
165 …void display_decimal(std::ostream & out, numeral const & a, unsigned k) { m().display_decimal(out,…  in display_decimal()
166 …void display_smt2(std::ostream & out, numeral const & a, bool decimal) { m().display_smt2(out, a, …  in display_smt2()