Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef _Z3_ALGEBRAIC_H_
00022 #define _Z3_ALGEBRAIC_H_
00023
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif // __cplusplus
00027
00034
00039
00045 Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a);
00046
00053 Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a);
00054
00061 Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a);
00062
00069 Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a);
00070
00077 int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a);
00078
00087 Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00088
00097 Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00098
00107 Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00108
00118 Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00119
00128 Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k);
00129
00137 Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k);
00138
00146 Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00147
00155 Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00156
00164 Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00165
00173 Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00174
00182 Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00183
00191 Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
00192
00202 Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
00203
00212 int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
00213
00216
00217 #ifdef __cplusplus
00218 };
00219 #endif // __cplusplus
00220
00221 #endif