Z3
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. 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...
 

Function Documentation

◆ Z3_rcf_add()

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_del()

void Z3_API Z3_rcf_del ( Z3_context  c,
Z3_rcf_num  a 
)

Delete a RCF numeral created using the RCF API.

◆ Z3_rcf_div()

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_eq()

bool Z3_API Z3_rcf_eq ( Z3_context  c,
Z3_rcf_num  a,
Z3_rcf_num  b 
)

Return true if a == b.

◆ Z3_rcf_ge()

bool Z3_API Z3_rcf_ge ( Z3_context  c,
Z3_rcf_num  a,
Z3_rcf_num  b 
)

Return true if a >= b.

◆ Z3_rcf_get_numerator_denominator()

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.

◆ Z3_rcf_gt()

bool Z3_API Z3_rcf_gt ( Z3_context  c,
Z3_rcf_num  a,
Z3_rcf_num  b 
)

Return true if a > b.

◆ Z3_rcf_inv()

Z3_rcf_num Z3_API Z3_rcf_inv ( Z3_context  c,
Z3_rcf_num  a 
)

Return the value 1/a.

◆ Z3_rcf_le()

bool Z3_API Z3_rcf_le ( Z3_context  c,
Z3_rcf_num  a,
Z3_rcf_num  b 
)

Return true if a <= b.

◆ Z3_rcf_lt()

bool Z3_API Z3_rcf_lt ( Z3_context  c,
Z3_rcf_num  a,
Z3_rcf_num  b 
)

Return true if a < b.

◆ Z3_rcf_mk_e()

Z3_rcf_num Z3_API Z3_rcf_mk_e ( Z3_context  c)

Return e (Euler's constant)

◆ Z3_rcf_mk_infinitesimal()

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_mk_pi()

Z3_rcf_num Z3_API Z3_rcf_mk_pi ( Z3_context  c)

Return Pi.

◆ Z3_rcf_mk_rational()

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_mk_roots()

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.

Precondition
The input polynomial is not the zero polynomial.

◆ Z3_rcf_mk_small_int()

Z3_rcf_num Z3_API Z3_rcf_mk_small_int ( Z3_context  c,
int  val 
)

Return a RCF small integer.

◆ Z3_rcf_mul()

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_neg()

Z3_rcf_num Z3_API Z3_rcf_neg ( Z3_context  c,
Z3_rcf_num  a 
)

Return the value -a.

◆ Z3_rcf_neq()

bool Z3_API Z3_rcf_neq ( Z3_context  c,
Z3_rcf_num  a,
Z3_rcf_num  b 
)

Return true if a != b.

◆ Z3_rcf_num_to_decimal_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.

◆ Z3_rcf_num_to_string()

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_power()

Z3_rcf_num Z3_API Z3_rcf_power ( Z3_context  c,
Z3_rcf_num  a,
unsigned  k 
)

Return the value a^k.

◆ Z3_rcf_sub()

Z3_rcf_num Z3_API Z3_rcf_sub ( Z3_context  c,
Z3_rcf_num  a,
Z3_rcf_num  b 
)

Return the value a - b.