Go to the source code of this file.
Functions | |
Algebraic Numbers | |
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. More... | |
bool Z3_API | Z3_algebraic_is_pos (Z3_context c, Z3_ast a) |
Return true if a is positive, and false otherwise. More... | |
bool Z3_API | Z3_algebraic_is_neg (Z3_context c, Z3_ast a) |
Return true if a is negative, and false otherwise. More... | |
bool Z3_API | Z3_algebraic_is_zero (Z3_context c, Z3_ast a) |
Return true if a is zero, and false otherwise. More... | |
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. More... | |
Z3_ast Z3_API | Z3_algebraic_add (Z3_context c, Z3_ast a, Z3_ast b) |
Return the value a + b. More... | |
Z3_ast Z3_API | Z3_algebraic_sub (Z3_context c, Z3_ast a, Z3_ast b) |
Return the value a - b. More... | |
Z3_ast Z3_API | Z3_algebraic_mul (Z3_context c, Z3_ast a, Z3_ast b) |
Return the value a * b. More... | |
Z3_ast Z3_API | Z3_algebraic_div (Z3_context c, Z3_ast a, Z3_ast b) |
Return the value a / b. More... | |
Z3_ast Z3_API | Z3_algebraic_root (Z3_context c, Z3_ast a, unsigned k) |
Return the a^(1/k) More... | |
Z3_ast Z3_API | Z3_algebraic_power (Z3_context c, Z3_ast a, unsigned k) |
Return the a^k. More... | |
bool Z3_API | Z3_algebraic_lt (Z3_context c, Z3_ast a, Z3_ast b) |
Return true if a < b, and false otherwise. More... | |
bool Z3_API | Z3_algebraic_gt (Z3_context c, Z3_ast a, Z3_ast b) |
Return true if a > b, and false otherwise. More... | |
bool Z3_API | Z3_algebraic_le (Z3_context c, Z3_ast a, Z3_ast b) |
Return true if a <= b, and false otherwise. More... | |
bool Z3_API | Z3_algebraic_ge (Z3_context c, Z3_ast a, Z3_ast b) |
Return true if a >= b, and false otherwise. More... | |
bool Z3_API | Z3_algebraic_eq (Z3_context c, Z3_ast a, Z3_ast b) |
Return true if a == b, and false otherwise. More... | |
bool Z3_API | Z3_algebraic_neq (Z3_context c, Z3_ast a, Z3_ast b) |
Return true if a != b, and false otherwise. More... | |
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 polynomial p(a[0], ..., a[n-1], x_n). More... | |
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], ..., a[n-1]). More... | |
Z3_ast_vector Z3_API | Z3_algebraic_get_poly (Z3_context c, Z3_ast a) |
Return the coefficients of the defining polynomial. More... | |
unsigned Z3_API | Z3_algebraic_get_i (Z3_context c, Z3_ast a) |
Return which root of the polynomial the algebraic number represents. More... | |
Z3_ast Z3_API Z3_algebraic_add | ( | Z3_context | c, |
Z3_ast | a, | ||
Z3_ast | b | ||
) |
Return the value a + b.
Z3_ast Z3_API Z3_algebraic_div | ( | 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.
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], ..., a[n-1]).
bool Z3_API Z3_algebraic_ge | ( | Z3_context | c, |
Z3_ast | a, | ||
Z3_ast | b | ||
) |
Return true
if a >= b, and false
otherwise.
unsigned Z3_API Z3_algebraic_get_i | ( | Z3_context | c, |
Z3_ast | a | ||
) |
Return which root of the polynomial the algebraic number represents.
Referenced by expr::algebraic_i(), and AlgebraicNumRef::index().
Z3_ast_vector Z3_API Z3_algebraic_get_poly | ( | Z3_context | c, |
Z3_ast | a | ||
) |
Return the coefficients of the defining polynomial.
Referenced by expr::algebraic_poly(), and AlgebraicNumRef::poly().
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_is_neg | ( | Z3_context | c, |
Z3_ast | a | ||
) |
Return true
if a
is negative, and false
otherwise.
bool Z3_API Z3_algebraic_is_pos | ( | Z3_context | c, |
Z3_ast | a | ||
) |
Return true
if a
is positive, and false
otherwise.
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.
bool Z3_API Z3_algebraic_is_zero | ( | Z3_context | c, |
Z3_ast | a | ||
) |
Return true
if a
is zero, and false
otherwise.
bool Z3_API Z3_algebraic_le | ( | Z3_context | c, |
Z3_ast | a, | ||
Z3_ast | b | ||
) |
Return true
if a <= b, and false
otherwise.
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_neq | ( | Z3_context | c, |
Z3_ast | a, | ||
Z3_ast | b | ||
) |
Return true
if a != b, and false
otherwise.
Z3_ast Z3_API Z3_algebraic_power | ( | Z3_context | c, |
Z3_ast | a, | ||
unsigned | k | ||
) |
Return the a^k.
Z3_ast Z3_API Z3_algebraic_root | ( | Z3_context | c, |
Z3_ast | a, | ||
unsigned | k | ||
) |
Return the a^(1/k)
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 polynomial p(a[0], ..., a[n-1], x_n).
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_ast Z3_API Z3_algebraic_sub | ( | Z3_context | c, |
Z3_ast | a, | ||
Z3_ast | b | ||
) |
Return the value a - b.