21 #ifndef _Z3_ALGEBRAIC_H_
22 #define _Z3_ALGEBRAIC_H_
219 #endif // __cplusplus
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.
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)