Z3
z3_algebraic.h
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 z3_algebraic.h
7
8Abstract:
9
10 Additional APIs for handling Z3 algebraic numbers encoded as
11 Z3_ASTs
12
13Author:
14
15 Leonardo de Moura (leonardo) 2012-12-07
16
17Notes:
18
19--*/
20
21#ifndef Z3_ALGEBRAIC_H_
22#define Z3_ALGEBRAIC_H_
23
24#ifdef __cplusplus
25extern "C" {
26#endif // __cplusplus
27
30
38 bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a);
39
46 bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a);
47
54 bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a);
55
62 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 bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
140
148 bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
149
157 bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
158
166 bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
167
175 bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
176
184 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
bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a)
Return true if a is positive, and false otherwise.
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_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a + b.
bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a == b, and false otherwise.
bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a > b, and false otherwise.
bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a != b, and false otherwise.
bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a >= b, and false otherwise.
bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a)
Return true if a is negative, and false otherwise.
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a / b.
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], ....
bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a < b, and false otherwise.
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a * b.
bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a)
Return true if a can be used as value in the Z3 real algebraic number package.
Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k)
Return the a^k.
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.
bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a)
Return true if a is zero, and false otherwise.
Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k)
Return the a^(1/k)
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a - b.
bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a <= b, and false otherwise.