1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     ext_numeral.h
7 
8 Abstract:
9 
10     Goodies for handling extended numerals such as R union { -oo, +oo }.
11     We can have extended sets of mpq, mpz, mpbq, mpf, etc.
12 
13 Author:
14 
15     Leonardo de Moura (leonardo) 2011-12-04.
16 
17 Revision History:
18 
19 --*/
20 #pragma once
21 
22 #include<iostream>
23 #include "util/debug.h"
24 
25 enum ext_numeral_kind { EN_MINUS_INFINITY, EN_NUMERAL, EN_PLUS_INFINITY };
26 
27 template<typename numeral_manager>
is_zero(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak)28 bool is_zero(numeral_manager & m,
29              typename numeral_manager::numeral const & a,
30              ext_numeral_kind ak) {
31     return ak == EN_NUMERAL && m.is_zero(a);
32 }
33 
34 template<typename numeral_manager>
is_pos(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak)35 bool is_pos(numeral_manager & m,
36             typename numeral_manager::numeral const & a,
37             ext_numeral_kind ak) {
38     return ak == EN_PLUS_INFINITY || (ak == EN_NUMERAL && m.is_pos(a));
39 }
40 
41 template<typename numeral_manager>
is_neg(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak)42 bool is_neg(numeral_manager & m,
43             typename numeral_manager::numeral const & a,
44             ext_numeral_kind ak) {
45     return ak == EN_MINUS_INFINITY || (ak == EN_NUMERAL && m.is_neg(a));
46 }
47 
is_infinite(ext_numeral_kind ak)48 inline bool is_infinite(ext_numeral_kind ak) { return ak != EN_NUMERAL; }
49 
50 template<typename numeral_manager>
set(numeral_manager & m,typename numeral_manager::numeral & a,ext_numeral_kind & ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk)51 void set(numeral_manager & m,
52          typename numeral_manager::numeral & a,
53          ext_numeral_kind & ak,
54          typename numeral_manager::numeral const & b,
55          ext_numeral_kind bk) {
56     m.set(a, b);
57     ak = bk;
58 }
59 
60 template<typename numeral_manager>
reset(numeral_manager & m,typename numeral_manager::numeral & a,ext_numeral_kind & ak)61 void reset(numeral_manager & m,
62            typename numeral_manager::numeral & a,
63            ext_numeral_kind & ak) {
64     m.reset(a);
65     ak = EN_NUMERAL;
66 }
67 
68 template<typename numeral_manager>
neg(numeral_manager & m,typename numeral_manager::numeral & a,ext_numeral_kind & ak)69 void neg(numeral_manager & m,
70          typename numeral_manager::numeral & a,
71          ext_numeral_kind & ak) {
72     switch (ak) {
73     case EN_MINUS_INFINITY:
74         ak = EN_PLUS_INFINITY;
75         break;
76     case EN_NUMERAL:
77         m.neg(a);
78         break;
79     case EN_PLUS_INFINITY:
80         ak = EN_MINUS_INFINITY;
81         break;
82     }
83 }
84 
85 template<typename numeral_manager>
inv(numeral_manager & m,typename numeral_manager::numeral & a,ext_numeral_kind & ak)86 void inv(numeral_manager & m,
87          typename numeral_manager::numeral & a,
88          ext_numeral_kind & ak) {
89     SASSERT(numeral_manager::field());
90     switch (ak) {
91     case EN_MINUS_INFINITY:
92         ak = EN_NUMERAL;
93         m.reset(a);
94         break;
95     case EN_NUMERAL:
96         SASSERT(!m.is_zero(a));
97         m.inv(a);
98         break;
99     case EN_PLUS_INFINITY:
100         ak = EN_NUMERAL;
101         m.reset(a);
102         break;
103     }
104 }
105 
106 template<typename numeral_manager>
add(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk,typename numeral_manager::numeral & c,ext_numeral_kind & ck)107 void add(numeral_manager & m,
108          typename numeral_manager::numeral const & a,
109          ext_numeral_kind ak,
110          typename numeral_manager::numeral const & b,
111          ext_numeral_kind bk,
112          typename numeral_manager::numeral & c,
113          ext_numeral_kind & ck) {
114     SASSERT(!(ak == EN_MINUS_INFINITY && bk == EN_PLUS_INFINITY));  // result is undefined
115     SASSERT(!(ak == EN_PLUS_INFINITY  && bk == EN_MINUS_INFINITY)); // result is undefined
116     if (ak != EN_NUMERAL) {
117         m.reset(c);
118         ck = ak;
119     }
120     else if (bk != EN_NUMERAL) {
121         m.reset(c);
122         ck = bk;
123     }
124     else {
125         m.add(a, b, c);
126         ck = EN_NUMERAL;
127     }
128 }
129 
130 template<typename numeral_manager>
sub(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk,typename numeral_manager::numeral & c,ext_numeral_kind & ck)131 void sub(numeral_manager & m,
132          typename numeral_manager::numeral const & a,
133          ext_numeral_kind ak,
134          typename numeral_manager::numeral const & b,
135          ext_numeral_kind bk,
136          typename numeral_manager::numeral & c,
137          ext_numeral_kind & ck) {
138     SASSERT(!(ak == EN_MINUS_INFINITY && bk == EN_MINUS_INFINITY));  // result is undefined
139     SASSERT(!(ak == EN_PLUS_INFINITY  && bk == EN_PLUS_INFINITY));   // result is undefined
140     if (ak != EN_NUMERAL) {
141         SASSERT(bk != ak);
142         m.reset(c);
143         ck = ak;
144     }
145     else {
146         switch (bk) {
147         case EN_MINUS_INFINITY:
148             m.reset(c);
149             ck = EN_PLUS_INFINITY;
150             break;
151         case EN_NUMERAL:
152             m.sub(a, b, c);
153             ck = EN_NUMERAL;
154             break;
155         case EN_PLUS_INFINITY:
156             m.reset(c);
157             ck = EN_MINUS_INFINITY;
158             break;
159         }
160     }
161 }
162 
163 template<typename numeral_manager>
mul(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk,typename numeral_manager::numeral & c,ext_numeral_kind & ck)164 void mul(numeral_manager & m,
165          typename numeral_manager::numeral const & a,
166          ext_numeral_kind ak,
167          typename numeral_manager::numeral const & b,
168          ext_numeral_kind bk,
169          typename numeral_manager::numeral & c,
170          ext_numeral_kind & ck) {
171     if (is_zero(m, a, ak) || is_zero(m, b, bk)) {
172         m.reset(c);
173         ck = EN_NUMERAL;
174     }
175     else if (is_infinite(ak) || is_infinite(bk)) {
176         if (is_pos(m, a, ak) == is_pos(m, b, bk))
177             ck = EN_PLUS_INFINITY;
178         else
179             ck = EN_MINUS_INFINITY;
180         m.reset(c);
181     }
182     else {
183         ck = EN_NUMERAL;
184         m.mul(a, b, c);
185     }
186 }
187 
188 template<typename numeral_manager>
div(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk,typename numeral_manager::numeral & c,ext_numeral_kind & ck)189 void div(numeral_manager & m,
190          typename numeral_manager::numeral const & a,
191          ext_numeral_kind ak,
192          typename numeral_manager::numeral const & b,
193          ext_numeral_kind bk,
194          typename numeral_manager::numeral & c,
195          ext_numeral_kind & ck) {
196     SASSERT(!is_zero(m, b, bk));
197     if (is_zero(m, a, ak)) {
198         SASSERT(!is_zero(m, b, bk));
199         m.reset(c);
200         ck = EN_NUMERAL;
201     }
202     else if (is_infinite(ak)) {
203         SASSERT(!is_infinite(bk));
204         if (is_pos(m, a, ak) == is_pos(m, b, bk))
205             ck = EN_PLUS_INFINITY;
206         else
207             ck = EN_MINUS_INFINITY;
208         m.reset(c);
209     }
210     else if (is_infinite(bk)) {
211         SASSERT(!is_infinite(ak));
212         m.reset(c);
213         ck = EN_NUMERAL;
214     }
215     else {
216         ck = EN_NUMERAL;
217         m.div(a, b, c);
218     }
219 }
220 
221 
222 template<typename numeral_manager>
power(numeral_manager & m,typename numeral_manager::numeral & a,ext_numeral_kind & ak,unsigned n)223 void power(numeral_manager & m,
224            typename numeral_manager::numeral & a,
225            ext_numeral_kind & ak,
226            unsigned n) {
227     switch (ak) {
228     case EN_MINUS_INFINITY:
229         if (n % 2 == 0)
230             ak = EN_PLUS_INFINITY;
231         break;
232     case EN_NUMERAL:
233         m.power(a, n, a);
234         break;
235     case EN_PLUS_INFINITY:
236         break; // do nothing
237     }
238 }
239 
240 /**
241    \brief Return true if (a,ak) == (b,bk).
242 */
243 template<typename numeral_manager>
eq(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk)244 bool eq(numeral_manager & m,
245         typename numeral_manager::numeral const & a,
246         ext_numeral_kind ak,
247         typename numeral_manager::numeral const & b,
248         ext_numeral_kind bk) {
249     if (ak == EN_NUMERAL) {
250         return bk == EN_NUMERAL && m.eq(a, b);
251     }
252     else {
253         return ak == bk;
254     }
255 }
256 
257 template<typename numeral_manager>
neq(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk)258 bool neq(numeral_manager & m,
259          typename numeral_manager::numeral const & a,
260          ext_numeral_kind ak,
261          typename numeral_manager::numeral const & b,
262          ext_numeral_kind bk) {
263     return !eq(m, a, ak, b, bk);
264 }
265 
266 template<typename numeral_manager>
lt(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk)267 bool lt(numeral_manager & m,
268         typename numeral_manager::numeral const & a,
269         ext_numeral_kind ak,
270         typename numeral_manager::numeral const & b,
271         ext_numeral_kind bk) {
272     switch (ak) {
273     case EN_MINUS_INFINITY:
274         return bk != EN_MINUS_INFINITY;
275     case EN_NUMERAL:
276         switch (bk) {
277         case EN_MINUS_INFINITY:
278             return false;
279         case EN_NUMERAL:
280             return m.lt(a, b);
281         case EN_PLUS_INFINITY:
282             return true;
283         default:
284             UNREACHABLE();
285             return false;
286         }
287     case EN_PLUS_INFINITY:
288         return false;
289     default:
290         UNREACHABLE();
291         return false;
292     }
293 }
294 
295 template<typename numeral_manager>
gt(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk)296 bool gt(numeral_manager & m,
297         typename numeral_manager::numeral const & a,
298         ext_numeral_kind ak,
299         typename numeral_manager::numeral const & b,
300         ext_numeral_kind bk) {
301     return lt(m, b, bk, a, ak);
302 }
303 
304 template<typename numeral_manager>
le(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk)305 bool le(numeral_manager & m,
306         typename numeral_manager::numeral const & a,
307         ext_numeral_kind ak,
308         typename numeral_manager::numeral const & b,
309         ext_numeral_kind bk) {
310     return !gt(m, a, ak, b, bk);
311 }
312 
313 template<typename numeral_manager>
ge(numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak,typename numeral_manager::numeral const & b,ext_numeral_kind bk)314 bool ge(numeral_manager & m,
315         typename numeral_manager::numeral const & a,
316         ext_numeral_kind ak,
317         typename numeral_manager::numeral const & b,
318         ext_numeral_kind bk) {
319     return !lt(m, a, ak, b, bk);
320 }
321 
322 template<typename numeral_manager>
display(std::ostream & out,numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak)323 void display(std::ostream & out,
324              numeral_manager & m,
325              typename numeral_manager::numeral const & a,
326              ext_numeral_kind ak) {
327     switch (ak) {
328     case EN_MINUS_INFINITY: out << "-oo"; break;
329     case EN_NUMERAL: m.display(out, a); break;
330     case EN_PLUS_INFINITY: out << "+oo"; break;
331     }
332 }
333 
334 template<typename numeral_manager>
display_pp(std::ostream & out,numeral_manager & m,typename numeral_manager::numeral const & a,ext_numeral_kind ak)335 void display_pp(std::ostream & out,
336                 numeral_manager & m,
337                 typename numeral_manager::numeral const & a,
338                 ext_numeral_kind ak) {
339     switch (ak) {
340     case EN_MINUS_INFINITY: out << "-&infin;"; break;
341     case EN_NUMERAL: m.display_pp(out, a); break;
342     case EN_PLUS_INFINITY: out << "+&infin;"; break;
343     }
344 }
345 
346