Z3
z3_rcf.h File Reference

Go to the source code of this file.

Functions

Real Closed Fields API
void Z3_API Z3_rcf_del (__in Z3_context c, __in Z3_rcf_num a)
 Delete a RCF numeral created using the RCF API. More...
 
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. More...
 
Z3_rcf_num Z3_API Z3_rcf_mk_small_int (__in Z3_context c, __in int val)
 Return a RCF small integer. More...
 
Z3_rcf_num Z3_API Z3_rcf_mk_pi (__in Z3_context c)
 Return Pi. More...
 
Z3_rcf_num Z3_API Z3_rcf_mk_e (__in Z3_context c)
 Return e (Euler's constant) More...
 
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. More...
 
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 have size n. It returns the number of roots of the polynomial. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
Z3_rcf_num Z3_API Z3_rcf_neg (__in Z3_context c, __in Z3_rcf_num a)
 Return the value -a. More...
 
Z3_rcf_num Z3_API Z3_rcf_inv (__in Z3_context c, __in Z3_rcf_num a)
 Return the value 1/a. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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, moreover n and d are not represented using rational functions. More...