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