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 
30 
38  Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a);
39 
46  Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a);
47 
54  Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a);
55 
62  Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a);
63 
70  int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a);
71 
80  Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b);
81 
90  Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b);
91 
100  Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b);
101 
111  Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b);
112 
121  Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k);
122 
130  Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k);
131 
139  Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
140 
148  Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
149 
157  Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
158 
166  Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
167 
175  Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
176 
184  Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
185 
195  Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
196 
205  int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
206 
209 
210 #ifdef __cplusplus
211 }
212 #endif // __cplusplus
213 
214 #endif
Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, 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_ge(Z3_context c, Z3_ast a, Z3_ast b)
Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a * b.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:84
Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k)
Return the a^(1/k)
Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a)
Return the Z3_TRUE if a is positive, and Z3_FALSE otherwise.
Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b)
Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, 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_gt(Z3_context c, Z3_ast a, Z3_ast b)
Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a + b.
Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b)
Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b)
Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, 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_eq(Z3_context c, Z3_ast a, Z3_ast b)
Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k)
Return the a^k.
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a - b.
Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a)
Return the Z3_TRUE if a is negative, and Z3_FALSE otherwise.
Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a)
Return the Z3_TRUE if a is zero, and Z3_FALSE otherwise.
int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a)
Return 1 if a is positive, 0 if a is zero, and -1 if a is negative.
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a / b.