189 #endif // __cplusplus
unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) 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 ...
Z3_bool Z3_API Z3_rcf_le(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a <= b.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Z3_rcf_num Z3_API Z3_rcf_mk_pi(__in Z3_context c)
Return Pi.
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c)
Return a new infinitesimal that is smaller than all elements in the Z3 field.
Z3_rcf_num Z3_API Z3_rcf_add(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a + b.
Z3_rcf_num Z3_API Z3_rcf_mk_rational(__in Z3_context c, __in Z3_string val)
Return a RCF rational using the given string.
Z3_bool Z3_API Z3_rcf_eq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a == b.
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(__in Z3_context c, __in int val)
Return a RCF small integer.
Z3_rcf_num Z3_API Z3_rcf_sub(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a - b.
Z3_bool Z3_API Z3_rcf_neq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a != b.
Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a >= b.
Z3_bool Z3_API Z3_rcf_lt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a < b.
Z3_rcf_num Z3_API Z3_rcf_power(__in Z3_context c, __in Z3_rcf_num a, __in unsigned k)
Return the value a^k.
void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num *n, __out Z3_rcf_num *d)
Extract the "numerator" and "denominator" of the given RCF numeral. We have that a = n/d...
Z3_rcf_num Z3_API Z3_rcf_neg(__in Z3_context c, __in Z3_rcf_num a)
Return the value -a.
Z3_bool Z3_API Z3_rcf_gt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return Z3_TRUE if a > b.
Z3_string Z3_API Z3_rcf_num_to_decimal_string(__in Z3_context c, __in Z3_rcf_num a, __in unsigned prec)
Convert the RCF numeral into a string in decimal notation.
Z3_rcf_num Z3_API Z3_rcf_mul(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a * b.
Z3_rcf_num Z3_API Z3_rcf_mk_e(__in Z3_context c)
Return e (Euler's constant)
void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a)
Delete a RCF numeral created using the RCF API.
Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html)
Convert the RCF numeral into a string.
Z3_rcf_num Z3_API Z3_rcf_inv(__in Z3_context c, __in Z3_rcf_num a)
Return the value 1/a.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Z3_rcf_num Z3_API Z3_rcf_div(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b)
Return the value a / b.