Z3
z3_rcf.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6  z3_rcf.h
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 #ifndef _Z3_RCF_H_
23 #define _Z3_RCF_H_
24 
25 #ifdef __cplusplus
26 extern "C" {
27 #endif // __cplusplus
28 
35 
40 
45  void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a);
46 
51  Z3_rcf_num Z3_API Z3_rcf_mk_rational(__in Z3_context c, __in Z3_string val);
52 
57  Z3_rcf_num Z3_API Z3_rcf_mk_small_int(__in Z3_context c, __in int val);
58 
63  Z3_rcf_num Z3_API Z3_rcf_mk_pi(__in Z3_context c);
64 
69  Z3_rcf_num Z3_API Z3_rcf_mk_e(__in Z3_context c);
70 
76 
85  unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) Z3_rcf_num roots[]);
86 
91  Z3_rcf_num Z3_API Z3_rcf_add(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
92 
97  Z3_rcf_num Z3_API Z3_rcf_sub(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
98 
103  Z3_rcf_num Z3_API Z3_rcf_mul(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
104 
109  Z3_rcf_num Z3_API Z3_rcf_div(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
110 
115  Z3_rcf_num Z3_API Z3_rcf_neg(__in Z3_context c, __in Z3_rcf_num a);
116 
121  Z3_rcf_num Z3_API Z3_rcf_inv(__in Z3_context c, __in Z3_rcf_num a);
122 
127  Z3_rcf_num Z3_API Z3_rcf_power(__in Z3_context c, __in Z3_rcf_num a, __in unsigned k);
128 
133  Z3_bool Z3_API Z3_rcf_lt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
134 
139  Z3_bool Z3_API Z3_rcf_gt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
140 
145  Z3_bool Z3_API Z3_rcf_le(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
146 
151  Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
152 
157  Z3_bool Z3_API Z3_rcf_eq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
158 
163  Z3_bool Z3_API Z3_rcf_neq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
164 
169  Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html);
170 
175  Z3_string Z3_API Z3_rcf_num_to_decimal_string(__in Z3_context c, __in Z3_rcf_num a, __in unsigned prec);
176 
182  void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num * n, __out Z3_rcf_num * d);
183 
186 
187 #ifdef __cplusplus
188 };
189 #endif // __cplusplus
190 
191 #endif
unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) Z3_rcf_num roots[])
Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]. The output vector roots must ...
Z3_bool Z3_API Z3_rcf_le(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a <= b.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:102
Z3_rcf_num Z3_API Z3_rcf_mk_pi(__in Z3_context c)
Return Pi.
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c)
Return a new infinitesimal that is smaller than all elements in the Z3 field.
Z3_rcf_num Z3_API Z3_rcf_add(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a + b.
Z3_rcf_num Z3_API Z3_rcf_mk_rational(__in Z3_context c, __in Z3_string val)
Return a RCF rational using the given string.
Z3_bool Z3_API Z3_rcf_eq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a == b.
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(__in Z3_context c, __in int val)
Return a RCF small integer.
Z3_rcf_num Z3_API Z3_rcf_sub(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a - b.
Z3_bool Z3_API Z3_rcf_neq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a != b.
Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a >= b.
Z3_bool Z3_API Z3_rcf_lt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a < b.
Z3_rcf_num Z3_API Z3_rcf_power(__in Z3_context c, __in Z3_rcf_num a, __in unsigned k)
Return the value a^k.
void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num *n, __out Z3_rcf_num *d)
Extract the "numerator" and "denominator" of the given RCF numeral. We have that a = n/d...
Z3_rcf_num Z3_API Z3_rcf_neg(__in Z3_context c, __in Z3_rcf_num a)
Return the value -a.
Z3_bool Z3_API Z3_rcf_gt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a > b.
Z3_string Z3_API Z3_rcf_num_to_decimal_string(__in Z3_context c, __in Z3_rcf_num a, __in unsigned prec)
Convert the RCF numeral into a string in decimal notation.
Z3_rcf_num Z3_API Z3_rcf_mul(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a * b.
Z3_rcf_num Z3_API Z3_rcf_mk_e(__in Z3_context c)
Return e (Euler's constant)
void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a)
Delete a RCF numeral created using the RCF API.
Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html)
Convert the RCF numeral into a string.
Z3_rcf_num Z3_API Z3_rcf_inv(__in Z3_context c, __in Z3_rcf_num a)
Return the value 1/a.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:111
Z3_rcf_num Z3_API Z3_rcf_div(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a / b.