1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
z3_rcf.h
Abstract:
Additional APIs for handling elements of the Z3 real closed field that contains:
- transcendental extensions
- infinitesimal extensions
- algebraic extensions
Author:
Leonardo de Moura (leonardo) 2012-01-05
Notes:
--*/
#pragma once
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/** \defgroup capi C API */
/**@{*/
/** @name Real Closed Fields */
/**@{*/
/**
\brief Delete a RCF numeral created using the RCF API.
def_API('Z3_rcf_del', VOID, (_in(CONTEXT), _in(RCF_NUM)))
*/
void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a);
/**
\brief Return a RCF rational using the given string.
def_API('Z3_rcf_mk_rational', RCF_NUM, (_in(CONTEXT), _in(STRING)))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val);
/**
\brief Return a RCF small integer.
def_API('Z3_rcf_mk_small_int', RCF_NUM, (_in(CONTEXT), _in(INT)))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val);
/**
\brief Return Pi
def_API('Z3_rcf_mk_pi', RCF_NUM, (_in(CONTEXT),))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c);
/**
\brief Return e (Euler's constant)
def_API('Z3_rcf_mk_e', RCF_NUM, (_in(CONTEXT),))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c);
/**
\brief Return a new infinitesimal that is smaller than all elements in the Z3 field.
def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT),))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c);
/**
\brief Store in roots the roots of the polynomial \ccode{a[n-1]*x^{n-1} + ... + a[0]}.
The output vector \c roots must have size \c n.
It returns the number of roots of the polynomial.
\pre The input polynomial is not the zero polynomial.
def_API('Z3_rcf_mk_roots', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, RCF_NUM), _out_array(1, RCF_NUM)))
*/
unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
/**
\brief Return the value \ccode{a + b}.
def_API('Z3_rcf_add', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value \ccode{a - b}.
def_API('Z3_rcf_sub', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value \ccode{a * b}.
def_API('Z3_rcf_mul', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value \ccode{a / b}.
def_API('Z3_rcf_div', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value \ccode{-a}.
def_API('Z3_rcf_neg', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a);
/**
\brief Return the value \ccode{1/a}.
def_API('Z3_rcf_inv', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a);
/**
\brief Return the value \ccode{a^k}.
def_API('Z3_rcf_power', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k);
/**
\brief Return \c true if \ccode{a < b}.
def_API('Z3_rcf_lt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if \ccode{a > b}.
def_API('Z3_rcf_gt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if \ccode{a <= b}.
def_API('Z3_rcf_le', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if \ccode{a >= b}.
def_API('Z3_rcf_ge', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if \ccode{a == b}.
def_API('Z3_rcf_eq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if \ccode{a != b}.
def_API('Z3_rcf_neq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Convert the RCF numeral into a string.
def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL), _in(BOOL)))
*/
Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html);
/**
\brief Convert the RCF numeral into a string in decimal notation.
def_API('Z3_rcf_num_to_decimal_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec);
/**
\brief Extract the "numerator" and "denominator" of the given RCF numeral.
We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions.
def_API('Z3_rcf_get_numerator_denominator', VOID, (_in(CONTEXT), _in(RCF_NUM), _out(RCF_NUM), _out(RCF_NUM)))
*/
void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
/**
\brief Return \c true if \c a represents a rational number.
def_API('Z3_rcf_is_rational', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_is_rational(Z3_context c, Z3_rcf_num a);
/**
\brief Return \c true if \c a represents an algebraic number.
def_API('Z3_rcf_is_algebraic', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_is_algebraic(Z3_context c, Z3_rcf_num a);
/**
\brief Return \c true if \c a represents an infinitesimal.
def_API('Z3_rcf_is_infinitesimal', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_is_infinitesimal(Z3_context c, Z3_rcf_num a);
/**
\brief Return \c true if \c a represents a transcendental number.
def_API('Z3_rcf_is_transcendental', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_is_transcendental(Z3_context c, Z3_rcf_num a);
/**
\brief Return the index of a field extension.
def_API('Z3_rcf_extension_index', UINT, (_in(CONTEXT), _in(RCF_NUM)))
*/
unsigned Z3_API Z3_rcf_extension_index(Z3_context c, Z3_rcf_num a);
/**
\brief Return the name of a transcendental.
\pre Z3_rcf_is_transcendtal(ctx, a);
def_API('Z3_rcf_transcendental_name', SYMBOL, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_symbol Z3_API Z3_rcf_transcendental_name(Z3_context c, Z3_rcf_num a);
/**
\brief Return the name of an infinitesimal.
\pre Z3_rcf_is_infinitesimal(ctx, a);
def_API('Z3_rcf_infinitesimal_name', SYMBOL, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_symbol Z3_API Z3_rcf_infinitesimal_name(Z3_context c, Z3_rcf_num a);
/**
\brief Return the number of coefficients in an algebraic number.
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_num_coefficients', UINT, (_in(CONTEXT), _in(RCF_NUM)))
*/
unsigned Z3_API Z3_rcf_num_coefficients(Z3_context c, Z3_rcf_num a);
/**
\brief Extract a coefficient from an algebraic number.
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_coefficient', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
Z3_rcf_num Z3_API Z3_rcf_coefficient(Z3_context c, Z3_rcf_num a, unsigned i);
/**
\brief Extract an interval from an algebraic number.
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_interval', INT, (_in(CONTEXT), _in(RCF_NUM), _out(BOOL), _out(BOOL), _out(RCF_NUM), _out(BOOL), _out(BOOL), _out(RCF_NUM)))
*/
int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, bool * lower_is_inf, bool * lower_is_open, Z3_rcf_num * lower, bool * upper_is_inf, bool * upper_is_open, Z3_rcf_num * upper);
/**
\brief Return the number of sign conditions of an algebraic number.
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_num_sign_conditions', UINT, (_in(CONTEXT), _in(RCF_NUM)))
*/
unsigned Z3_API Z3_rcf_num_sign_conditions(Z3_context c, Z3_rcf_num a);
/**
\brief Extract the sign of a sign condition from an algebraic number.
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_sign_condition_sign', INT, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
int Z3_API Z3_rcf_sign_condition_sign(Z3_context c, Z3_rcf_num a, unsigned i);
/**
\brief Return the number of sign condition polynomial coefficients of an algebraic number.
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_num_sign_condition_coefficients', UINT, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
unsigned Z3_API Z3_rcf_num_sign_condition_coefficients(Z3_context c, Z3_rcf_num a, unsigned i);
/**
\brief Extract the j-th polynomial coefficient of the i-th sign condition.
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_sign_condition_coefficient', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT), _in(UINT)))
*/
Z3_rcf_num Z3_API Z3_rcf_sign_condition_coefficient(Z3_context c, Z3_rcf_num a, unsigned i, unsigned j);
/**@}*/
/**@}*/
#ifdef __cplusplus
}
#endif // __cplusplus