Z3
 
Loading...
Searching...
No Matches
z3_rcf.h File Reference

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.
 
Z3_rcf_num Z3_API Z3_rcf_mk_rational (Z3_context c, Z3_string val)
 Return a RCF rational using the given string.
 
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_mk_pi (Z3_context c)
 Return Pi.
 
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.
 
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_add (Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
 Return the value a + b.
 
Z3_rcf_num Z3_API Z3_rcf_sub (Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
 Return the value a - b.
 
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_div (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.
 
Z3_rcf_num Z3_API Z3_rcf_inv (Z3_context c, Z3_rcf_num a)
 Return the value 1/a.
 
Z3_rcf_num Z3_API Z3_rcf_power (Z3_context c, Z3_rcf_num a, unsigned k)
 Return the value a^k.
 
bool Z3_API Z3_rcf_lt (Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
 Return true if a < b.
 
bool Z3_API Z3_rcf_gt (Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
 Return true if a > b.
 
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_ge (Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
 Return true if 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_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_string (Z3_context c, Z3_rcf_num a, bool compact, bool html)
 Convert the RCF numeral into a string.
 
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.
 
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_is_rational (Z3_context c, Z3_rcf_num a)
 Return true if a represents a rational number.
 
bool Z3_API Z3_rcf_is_algebraic (Z3_context c, Z3_rcf_num a)
 Return true if a represents an algebraic number.
 
bool Z3_API Z3_rcf_is_infinitesimal (Z3_context c, Z3_rcf_num a)
 Return true if a represents an infinitesimal.
 
bool Z3_API Z3_rcf_is_transcendental (Z3_context c, Z3_rcf_num a)
 Return true if a represents a transcendental number.
 
unsigned Z3_API Z3_rcf_extension_index (Z3_context c, Z3_rcf_num a)
 Return the index of a field extension.
 
Z3_symbol Z3_API Z3_rcf_transcendental_name (Z3_context c, Z3_rcf_num a)
 Return the name of a transcendental.
 
Z3_symbol Z3_API Z3_rcf_infinitesimal_name (Z3_context c, Z3_rcf_num a)
 Return the name of an infinitesimal.
 
unsigned Z3_API Z3_rcf_num_coefficients (Z3_context c, Z3_rcf_num a)
 Return the number of coefficients in an algebraic number.
 
Z3_rcf_num Z3_API Z3_rcf_coefficient (Z3_context c, Z3_rcf_num a, unsigned i)
 Extract a coefficient from an algebraic number.
 
int Z3_API Z3_rcf_interval (Z3_context c, Z3_rcf_num a, int *lower_is_inf, int *lower_is_open, Z3_rcf_num *lower, int *upper_is_inf, int *upper_is_open, Z3_rcf_num *upper)
 Extract an interval from an algebraic number.
 
unsigned Z3_API Z3_rcf_num_sign_conditions (Z3_context c, Z3_rcf_num a)
 Return the number of sign conditions of an algebraic number.
 
int Z3_API Z3_rcf_sign_condition_sign (Z3_context c, Z3_rcf_num a, unsigned i)
 Extract the sign of a sign condition from an algebraic number.
 
unsigned Z3_API Z3_rcf_num_sign_condition_coefficients (Z3_context c, Z3_rcf_num a, unsigned i)
 Return the number of sign condition polynomial coefficients of an algebraic number.
 
Z3_rcf_num Z3_API Z3_rcf_sign_condition_coefficient (Z3_context c, Z3_rcf_num a, unsigned i, unsigned j)
 Extract the j-th polynomial coefficient of the i-th sign condition.