1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3
4 Module Name:
5
6 api_rcf.cpp
7
8 Abstract:
9
10 Additional APIs for handling elements of the Z3 real closed field that contains:
11 - transcendental extensions
12 - infinitesimal extensions
13 - algebraic extensions
14
15 Author:
16
17 Leonardo de Moura (leonardo) 2012-01-05
18
19 Notes:
20
21 --*/
22 #include<iostream>
23 #include "api/z3.h"
24 #include "api/api_log_macros.h"
25 #include "api/api_context.h"
26 #include "math/realclosure/realclosure.h"
27
rcfm(Z3_context c)28 static rcmanager & rcfm(Z3_context c) {
29 return mk_c(c)->rcfm();
30 }
31
reset_rcf_cancel(Z3_context c)32 static void reset_rcf_cancel(Z3_context c) {
33 // no-op
34 }
35
from_rcnumeral(rcnumeral a)36 static Z3_rcf_num from_rcnumeral(rcnumeral a) {
37 return reinterpret_cast<Z3_rcf_num>(a.c_ptr());
38 }
39
to_rcnumeral(Z3_rcf_num a)40 static rcnumeral to_rcnumeral(Z3_rcf_num a) {
41 return rcnumeral::mk(a);
42 }
43
44 extern "C" {
45
Z3_rcf_del(Z3_context c,Z3_rcf_num a)46 void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a) {
47 Z3_TRY;
48 LOG_Z3_rcf_del(c, a);
49 RESET_ERROR_CODE();
50 rcnumeral _a = to_rcnumeral(a);
51 rcfm(c).del(_a);
52 Z3_CATCH;
53 }
54
Z3_rcf_mk_rational(Z3_context c,Z3_string val)55 Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val) {
56 Z3_TRY;
57 LOG_Z3_rcf_mk_rational(c, val);
58 RESET_ERROR_CODE();
59 reset_rcf_cancel(c);
60 scoped_mpq q(rcfm(c).qm());
61 rcfm(c).qm().set(q, val);
62 rcnumeral r;
63 rcfm(c).set(r, q);
64 RETURN_Z3(from_rcnumeral(r));
65 Z3_CATCH_RETURN(nullptr);
66 }
67
Z3_rcf_mk_small_int(Z3_context c,int val)68 Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val) {
69 Z3_TRY;
70 LOG_Z3_rcf_mk_small_int(c, val);
71 RESET_ERROR_CODE();
72 reset_rcf_cancel(c);
73 rcnumeral r;
74 rcfm(c).set(r, val);
75 RETURN_Z3(from_rcnumeral(r));
76 Z3_CATCH_RETURN(nullptr);
77 }
78
Z3_rcf_mk_pi(Z3_context c)79 Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c) {
80 Z3_TRY;
81 LOG_Z3_rcf_mk_pi(c);
82 RESET_ERROR_CODE();
83 reset_rcf_cancel(c);
84 rcnumeral r;
85 rcfm(c).mk_pi(r);
86 RETURN_Z3(from_rcnumeral(r));
87 Z3_CATCH_RETURN(nullptr);
88 }
89
Z3_rcf_mk_e(Z3_context c)90 Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c) {
91 Z3_TRY;
92 LOG_Z3_rcf_mk_e(c);
93 RESET_ERROR_CODE();
94 reset_rcf_cancel(c);
95 rcnumeral r;
96 rcfm(c).mk_e(r);
97 RETURN_Z3(from_rcnumeral(r));
98 Z3_CATCH_RETURN(nullptr);
99 }
100
Z3_rcf_mk_infinitesimal(Z3_context c)101 Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c) {
102 Z3_TRY;
103 LOG_Z3_rcf_mk_infinitesimal(c);
104 RESET_ERROR_CODE();
105 reset_rcf_cancel(c);
106 rcnumeral r;
107 rcfm(c).mk_infinitesimal(r);
108 RETURN_Z3(from_rcnumeral(r));
109 Z3_CATCH_RETURN(nullptr);
110 }
111
Z3_rcf_mk_roots(Z3_context c,unsigned n,Z3_rcf_num const a[],Z3_rcf_num roots[])112 unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]) {
113 Z3_TRY;
114 LOG_Z3_rcf_mk_roots(c, n, a, roots);
115 RESET_ERROR_CODE();
116 reset_rcf_cancel(c);
117 rcnumeral_vector av;
118 unsigned rz = 0;
119 for (unsigned i = 0; i < n; i++) {
120 if (!rcfm(c).is_zero(to_rcnumeral(a[i])))
121 rz = i + 1;
122 av.push_back(to_rcnumeral(a[i]));
123 }
124 if (rz == 0) {
125 // it is the zero polynomial
126 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
127 return 0;
128 }
129 av.shrink(rz);
130 rcnumeral_vector rs;
131 rcfm(c).isolate_roots(av.size(), av.c_ptr(), rs);
132 unsigned num_roots = rs.size();
133 for (unsigned i = 0; i < num_roots; i++) {
134 roots[i] = from_rcnumeral(rs[i]);
135 }
136 RETURN_Z3_rcf_mk_roots num_roots;
137 Z3_CATCH_RETURN(0);
138 }
139
Z3_rcf_add(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)140 Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
141 Z3_TRY;
142 LOG_Z3_rcf_add(c, a, b);
143 RESET_ERROR_CODE();
144 reset_rcf_cancel(c);
145 rcnumeral r;
146 rcfm(c).add(to_rcnumeral(a), to_rcnumeral(b), r);
147 RETURN_Z3(from_rcnumeral(r));
148 Z3_CATCH_RETURN(nullptr);
149 }
150
Z3_rcf_sub(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)151 Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
152 Z3_TRY;
153 LOG_Z3_rcf_sub(c, a, b);
154 RESET_ERROR_CODE();
155 reset_rcf_cancel(c);
156 rcnumeral r;
157 rcfm(c).sub(to_rcnumeral(a), to_rcnumeral(b), r);
158 RETURN_Z3(from_rcnumeral(r));
159 Z3_CATCH_RETURN(nullptr);
160 }
161
Z3_rcf_mul(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)162 Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
163 Z3_TRY;
164 LOG_Z3_rcf_mul(c, a, b);
165 RESET_ERROR_CODE();
166 reset_rcf_cancel(c);
167 rcnumeral r;
168 rcfm(c).mul(to_rcnumeral(a), to_rcnumeral(b), r);
169 RETURN_Z3(from_rcnumeral(r));
170 Z3_CATCH_RETURN(nullptr);
171 }
172
Z3_rcf_div(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)173 Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
174 Z3_TRY;
175 LOG_Z3_rcf_div(c, a, b);
176 RESET_ERROR_CODE();
177 reset_rcf_cancel(c);
178 rcnumeral r;
179 rcfm(c).div(to_rcnumeral(a), to_rcnumeral(b), r);
180 RETURN_Z3(from_rcnumeral(r));
181 Z3_CATCH_RETURN(nullptr);
182 }
183
Z3_rcf_neg(Z3_context c,Z3_rcf_num a)184 Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a) {
185 Z3_TRY;
186 LOG_Z3_rcf_neg(c, a);
187 RESET_ERROR_CODE();
188 reset_rcf_cancel(c);
189 rcnumeral r;
190 rcfm(c).neg(to_rcnumeral(a), r);
191 RETURN_Z3(from_rcnumeral(r));
192 Z3_CATCH_RETURN(nullptr);
193 }
194
Z3_rcf_inv(Z3_context c,Z3_rcf_num a)195 Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a) {
196 Z3_TRY;
197 LOG_Z3_rcf_inv(c, a);
198 RESET_ERROR_CODE();
199 reset_rcf_cancel(c);
200 rcnumeral r;
201 rcfm(c).inv(to_rcnumeral(a), r);
202 RETURN_Z3(from_rcnumeral(r));
203 Z3_CATCH_RETURN(nullptr);
204 }
205
Z3_rcf_power(Z3_context c,Z3_rcf_num a,unsigned k)206 Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k) {
207 Z3_TRY;
208 LOG_Z3_rcf_power(c, a, k);
209 RESET_ERROR_CODE();
210 reset_rcf_cancel(c);
211 rcnumeral r;
212 rcfm(c).power(to_rcnumeral(a), k, r);
213 RETURN_Z3(from_rcnumeral(r));
214 Z3_CATCH_RETURN(nullptr);
215 }
216
Z3_rcf_lt(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)217 bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
218 Z3_TRY;
219 LOG_Z3_rcf_lt(c, a, b);
220 RESET_ERROR_CODE();
221 reset_rcf_cancel(c);
222 return rcfm(c).lt(to_rcnumeral(a), to_rcnumeral(b));
223 Z3_CATCH_RETURN(false);
224 }
225
Z3_rcf_gt(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)226 bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
227 Z3_TRY;
228 LOG_Z3_rcf_gt(c, a, b);
229 RESET_ERROR_CODE();
230 reset_rcf_cancel(c);
231 return rcfm(c).gt(to_rcnumeral(a), to_rcnumeral(b));
232 Z3_CATCH_RETURN(false);
233 }
234
Z3_rcf_le(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)235 bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
236 Z3_TRY;
237 LOG_Z3_rcf_le(c, a, b);
238 RESET_ERROR_CODE();
239 reset_rcf_cancel(c);
240 return rcfm(c).le(to_rcnumeral(a), to_rcnumeral(b));
241 Z3_CATCH_RETURN(false);
242 }
243
Z3_rcf_ge(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)244 bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
245 Z3_TRY;
246 LOG_Z3_rcf_ge(c, a, b);
247 RESET_ERROR_CODE();
248 reset_rcf_cancel(c);
249 return rcfm(c).ge(to_rcnumeral(a), to_rcnumeral(b));
250 Z3_CATCH_RETURN(false);
251 }
252
Z3_rcf_eq(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)253 bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
254 Z3_TRY;
255 LOG_Z3_rcf_eq(c, a, b);
256 RESET_ERROR_CODE();
257 reset_rcf_cancel(c);
258 return rcfm(c).eq(to_rcnumeral(a), to_rcnumeral(b));
259 Z3_CATCH_RETURN(false);
260 }
261
Z3_rcf_neq(Z3_context c,Z3_rcf_num a,Z3_rcf_num b)262 bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
263 Z3_TRY;
264 LOG_Z3_rcf_neq(c, a, b);
265 RESET_ERROR_CODE();
266 reset_rcf_cancel(c);
267 return rcfm(c).neq(to_rcnumeral(a), to_rcnumeral(b));
268 Z3_CATCH_RETURN(false);
269 }
270
Z3_rcf_num_to_string(Z3_context c,Z3_rcf_num a,bool compact,bool html)271 Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html) {
272 Z3_TRY;
273 LOG_Z3_rcf_num_to_string(c, a, compact, html);
274 RESET_ERROR_CODE();
275 reset_rcf_cancel(c);
276 std::ostringstream buffer;
277 rcfm(c).display(buffer, to_rcnumeral(a), compact, html);
278 return mk_c(c)->mk_external_string(buffer.str());
279 Z3_CATCH_RETURN("");
280 }
281
Z3_rcf_num_to_decimal_string(Z3_context c,Z3_rcf_num a,unsigned prec)282 Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec) {
283 Z3_TRY;
284 LOG_Z3_rcf_num_to_decimal_string(c, a, prec);
285 RESET_ERROR_CODE();
286 reset_rcf_cancel(c);
287 std::ostringstream buffer;
288 rcfm(c).display_decimal(buffer, to_rcnumeral(a), prec);
289 return mk_c(c)->mk_external_string(buffer.str());
290 Z3_CATCH_RETURN("");
291 }
292
Z3_rcf_get_numerator_denominator(Z3_context c,Z3_rcf_num a,Z3_rcf_num * n,Z3_rcf_num * d)293 void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d) {
294 Z3_TRY;
295 LOG_Z3_rcf_get_numerator_denominator(c, a, n, d);
296 RESET_ERROR_CODE();
297 reset_rcf_cancel(c);
298 rcnumeral _n, _d;
299 rcfm(c).clean_denominators(to_rcnumeral(a), _n, _d);
300 *n = from_rcnumeral(_n);
301 *d = from_rcnumeral(_d);
302 RETURN_Z3_rcf_get_numerator_denominator;
303 Z3_CATCH;
304 }
305
306 };
307