Z3
z3_algebraic.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  z3_algebraic.h
7 
8 Abstract:
9 
10  Additional APIs for handling Z3 algebraic numbers encoded as
11  Z3_ASTs
12 
13 Author:
14 
15  Leonardo de Moura (leonardo) 2012-12-07
16 
17 Notes:
18 
19 --*/
20 
21 #ifndef _Z3_ALGEBRAIC_H_
22 #define _Z3_ALGEBRAIC_H_
23 
24 #ifdef __cplusplus
25 extern "C" {
26 #endif // __cplusplus
27 
34 
39 
45  Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a);
46 
53  Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a);
54 
61  Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a);
62 
69  Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a);
70 
77  int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a);
78 
87  Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
88 
97  Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
98 
107  Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
108 
118  Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
119 
128  Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k);
129 
137  Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k);
138 
146  Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
147 
155  Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
156 
164  Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
165 
173  Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
174 
182  Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
183 
191  Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
192 
202  Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
203 
212  int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
213 
216 
217 #ifdef __cplusplus
218 };
219 #endif // __cplusplus
220 
221 #endif
Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a)
Return Z3_TRUE if can be used as value in the Z3 real algebraic number package.
Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k)
Return the a^k.
Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[])
Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polyno...
Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:102
Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a)
Return the Z3_TRUE if a is positive, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a - b.
Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a / b.
Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a)
Return 1 if a is positive, 0 if a is zero, and -1 if a is negative.
Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a)
Return the Z3_TRUE if a is zero, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a + b.
Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
Return the value a * b.
int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[])
Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a[0], ..., a[n-1]).
Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a)
Return the Z3_TRUE if a is negative, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k)
Return the a^(1/k)