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 #pragma once
22 
23 #ifdef __cplusplus
24 extern "C" {
25 #endif // __cplusplus
26 
37  bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a);
38 
45  bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a);
46 
53  bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a);
54 
61  bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a);
62 
69  int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a);
70 
79  Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b);
80 
89  Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b);
90 
99  Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b);
100 
110  Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b);
111 
120  Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k);
121 
129  Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k);
130 
138  bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
139 
147  bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
148 
156  bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
157 
165  bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
166 
174  bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
175 
183  bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
184 
194  Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
195 
204  int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
205 
212  Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a);
213 
220  unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a);
221 
225 #ifdef __cplusplus
226 }
227 #endif // __cplusplus
228 
Z3_algebraic_is_pos
bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a)
Return true if a is positive, and false otherwise.
Z3_algebraic_roots
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_algebraic_add
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a + b.
Z3_algebraic_eq
bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a == b, and false otherwise.
Z3_algebraic_gt
bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a > b, and false otherwise.
Z3_algebraic_neq
bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a != b, and false otherwise.
Z3_algebraic_ge
bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a >= b, and false otherwise.
Z3_algebraic_get_poly
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
Z3_algebraic_get_i
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
Z3_algebraic_is_neg
bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a)
Return true if a is negative, and false otherwise.
Z3_algebraic_div
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a / b.
Z3_algebraic_eval
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], ....
Z3_algebraic_lt
bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a < b, and false otherwise.
Z3_algebraic_mul
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a * b.
Z3_algebraic_is_value
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_algebraic_power
Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k)
Return the a^k.
Z3_algebraic_sign
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_algebraic_is_zero
bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a)
Return true if a is zero, and false otherwise.
Z3_algebraic_root
Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k)
Return the a^(1/k)
Z3_algebraic_sub
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b)
Return the value a - b.
Z3_algebraic_le
bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b)
Return true if a <= b, and false otherwise.
Microsoft.Z3.Z3_context
System.IntPtr Z3_context
Definition: Context.cs:29
Microsoft.Z3.Z3_ast_vector
System.IntPtr Z3_ast_vector
Definition: NativeContext.cs:29
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28
Generated on Sat Jan 14 2023 14:44:08 for Z3 by doxygen 1.9.1