Go to the source code of this file.
Functions | |
Real Closed Fields | |
void Z3_API | Z3_rcf_del (Z3_context c, Z3_rcf_num a) |
Delete a RCF numeral created using the RCF API. More... | |
Z3_rcf_num Z3_API | Z3_rcf_mk_rational (Z3_context c, Z3_string val) |
Return a RCF rational using the given string. More... | |
Z3_rcf_num Z3_API | Z3_rcf_mk_small_int (Z3_context c, int val) |
Return a RCF small integer. More... | |
Z3_rcf_num Z3_API | Z3_rcf_mk_pi (Z3_context c) |
Return Pi. More... | |
Z3_rcf_num Z3_API | Z3_rcf_mk_e (Z3_context c) |
Return e (Euler's constant) More... | |
Z3_rcf_num Z3_API | Z3_rcf_mk_infinitesimal (Z3_context c) |
Return a new infinitesimal that is smaller than all elements in the Z3 field. More... | |
unsigned Z3_API | Z3_rcf_mk_roots (Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]) |
Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0] . The output vector roots must have size n . It returns the number of roots of the polynomial. More... | |
Z3_rcf_num Z3_API | Z3_rcf_add (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return the value a + b . More... | |
Z3_rcf_num Z3_API | Z3_rcf_sub (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return the value a - b . More... | |
Z3_rcf_num Z3_API | Z3_rcf_mul (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return the value a * b . More... | |
Z3_rcf_num Z3_API | Z3_rcf_div (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return the value a / b . More... | |
Z3_rcf_num Z3_API | Z3_rcf_neg (Z3_context c, Z3_rcf_num a) |
Return the value -a . More... | |
Z3_rcf_num Z3_API | Z3_rcf_inv (Z3_context c, Z3_rcf_num a) |
Return the value 1/a . More... | |
Z3_rcf_num Z3_API | Z3_rcf_power (Z3_context c, Z3_rcf_num a, unsigned k) |
Return the value a^k . More... | |
bool Z3_API | Z3_rcf_lt (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return true if a < b . More... | |
bool Z3_API | Z3_rcf_gt (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return true if a > b . More... | |
bool Z3_API | Z3_rcf_le (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return true if a <= b . More... | |
bool Z3_API | Z3_rcf_ge (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return true if a >= b . More... | |
bool Z3_API | Z3_rcf_eq (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return true if a == b . More... | |
bool Z3_API | Z3_rcf_neq (Z3_context c, Z3_rcf_num a, Z3_rcf_num b) |
Return true if a != b . More... | |
Z3_string Z3_API | Z3_rcf_num_to_string (Z3_context c, Z3_rcf_num a, bool compact, bool html) |
Convert the RCF numeral into a string. More... | |
Z3_string Z3_API | Z3_rcf_num_to_decimal_string (Z3_context c, Z3_rcf_num a, unsigned prec) |
Convert the RCF numeral into a string in decimal notation. More... | |
void Z3_API | Z3_rcf_get_numerator_denominator (Z3_context c, Z3_rcf_num a, Z3_rcf_num *n, Z3_rcf_num *d) |
Extract the "numerator" and "denominator" of the given RCF numeral. We have that a = n/d , moreover n and d are not represented using rational functions. More... | |
Z3_rcf_num Z3_API Z3_rcf_add | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return the value a + b
.
void Z3_API Z3_rcf_del | ( | Z3_context | c, |
Z3_rcf_num | a | ||
) |
Delete a RCF numeral created using the RCF API.
Z3_rcf_num Z3_API Z3_rcf_div | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return the value a / b
.
bool Z3_API Z3_rcf_eq | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return true
if a == b
.
bool Z3_API Z3_rcf_ge | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return true
if a >= b
.
void Z3_API Z3_rcf_get_numerator_denominator | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num * | n, | ||
Z3_rcf_num * | d | ||
) |
Extract the "numerator" and "denominator" of the given RCF numeral. We have that a = n/d
, moreover n
and d
are not represented using rational functions.
bool Z3_API Z3_rcf_gt | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return true
if a > b
.
Z3_rcf_num Z3_API Z3_rcf_inv | ( | Z3_context | c, |
Z3_rcf_num | a | ||
) |
Return the value 1/a
.
bool Z3_API Z3_rcf_le | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return true
if a <= b
.
bool Z3_API Z3_rcf_lt | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return true
if a < b
.
Z3_rcf_num Z3_API Z3_rcf_mk_e | ( | Z3_context | c | ) |
Return e (Euler's constant)
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal | ( | Z3_context | c | ) |
Return a new infinitesimal that is smaller than all elements in the Z3 field.
Z3_rcf_num Z3_API Z3_rcf_mk_pi | ( | Z3_context | c | ) |
Return Pi.
Z3_rcf_num Z3_API Z3_rcf_mk_rational | ( | Z3_context | c, |
Z3_string | val | ||
) |
Return a RCF rational using the given string.
unsigned Z3_API Z3_rcf_mk_roots | ( | Z3_context | c, |
unsigned | n, | ||
Z3_rcf_num const | a[], | ||
Z3_rcf_num | roots[] | ||
) |
Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]
. The output vector roots
must have size n
. It returns the number of roots of the polynomial.
Z3_rcf_num Z3_API Z3_rcf_mk_small_int | ( | Z3_context | c, |
int | val | ||
) |
Return a RCF small integer.
Z3_rcf_num Z3_API Z3_rcf_mul | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return the value a * b
.
Z3_rcf_num Z3_API Z3_rcf_neg | ( | Z3_context | c, |
Z3_rcf_num | a | ||
) |
Return the value -a
.
bool Z3_API Z3_rcf_neq | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return true
if a != b
.
Z3_string Z3_API Z3_rcf_num_to_decimal_string | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
unsigned | prec | ||
) |
Convert the RCF numeral into a string in decimal notation.
Z3_string Z3_API Z3_rcf_num_to_string | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
bool | compact, | ||
bool | html | ||
) |
Convert the RCF numeral into a string.
Z3_rcf_num Z3_API Z3_rcf_power | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
unsigned | k | ||
) |
Return the value a^k
.
Z3_rcf_num Z3_API Z3_rcf_sub | ( | Z3_context | c, |
Z3_rcf_num | a, | ||
Z3_rcf_num | b | ||
) |
Return the value a - b
.