Z3
z3_algebraic.h File Reference

Go to the source code of this file.

Functions

Algebraic Numbers API
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
Z3_ast Z3_API Z3_algebraic_add (__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
 Return the value a + b. More...
 
Z3_ast Z3_API Z3_algebraic_sub (__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
 Return the value a - b. More...
 
Z3_ast Z3_API Z3_algebraic_mul (__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
 Return the value a * b. More...
 
Z3_ast Z3_API Z3_algebraic_div (__in Z3_context c, __in Z3_ast a, __in Z3_ast b)
 Return the value a / b. More...
 
Z3_ast Z3_API Z3_algebraic_root (__in Z3_context c, __in Z3_ast a, __in unsigned k)
 Return the a^(1/k) More...
 
Z3_ast Z3_API Z3_algebraic_power (__in Z3_context c, __in Z3_ast a, __in unsigned k)
 Return the a^k. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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 polynomial p(a[0], ..., a[n-1], x_n). More...
 
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]). More...