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 << "-∞"; break;
341 case EN_NUMERAL: m.display_pp(out, a); break;
342 case EN_PLUS_INFINITY: out << "+∞"; break;
343 }
344 }
345
346