Z3 |

z3_algebraic.h File Reference

Go to the source code of this file.

## Functions
Algebraic Numbers
bool Z3_API | Z3_algebraic_is_value (Z3_context c, Z3_ast a)
| Return `true` if `a` can be used as value in the Z3 real algebraic number package. More...
bool Z3_API | Z3_algebraic_is_pos (Z3_context c, Z3_ast a)
| Return `true` if `a` is positive, and `false` otherwise. More...
bool Z3_API | Z3_algebraic_is_neg (Z3_context c, Z3_ast a)
| Return `true` if `a` is negative, and `false` otherwise. More...
bool Z3_API | Z3_algebraic_is_zero (Z3_context c, Z3_ast a)
| Return `true` if `a` is zero, and `false` otherwise. More...
int Z3_API | Z3_algebraic_sign (Z3_context c, Z3_ast a)
| Return 1 if `a` is positive, 0 if `a` is zero, and -1 if `a` is negative. More...
Z3_ast Z3_API | Z3_algebraic_add (Z3_context c, Z3_ast a, Z3_ast b)
| Return the value a + b. More...
Z3_ast Z3_API | Z3_algebraic_sub (Z3_context c, Z3_ast a, Z3_ast b)
| Return the value a - b. More...
Z3_ast Z3_API | Z3_algebraic_mul (Z3_context c, Z3_ast a, Z3_ast b)
| Return the value a * b. More...
Z3_ast Z3_API | Z3_algebraic_div (Z3_context c, Z3_ast a, Z3_ast b)
| Return the value a / b. More...
Z3_ast Z3_API | Z3_algebraic_root (Z3_context c, Z3_ast a, unsigned k)
| Return the a^(1/k) More...
Z3_ast Z3_API | Z3_algebraic_power (Z3_context c, Z3_ast a, unsigned k)
| Return the a^k. More...
bool Z3_API | Z3_algebraic_lt (Z3_context c, Z3_ast a, Z3_ast b)
| Return `true` if a < b, and `false` otherwise. More...
bool Z3_API | Z3_algebraic_gt (Z3_context c, Z3_ast a, Z3_ast b)
| Return `true` if a > b, and `false` otherwise. More...
bool Z3_API | Z3_algebraic_le (Z3_context c, Z3_ast a, Z3_ast b)
| Return `true` if a <= b, and `false` otherwise. More...
bool Z3_API | Z3_algebraic_ge (Z3_context c, Z3_ast a, Z3_ast b)
| Return `true` if a >= b, and `false` otherwise. More...
bool Z3_API | Z3_algebraic_eq (Z3_context c, Z3_ast a, Z3_ast b)
| Return `true` if a == b, and `false` otherwise. More...
bool Z3_API | Z3_algebraic_neq (Z3_context c, Z3_ast a, Z3_ast b)
| Return `true` if a != b, and `false` otherwise. More...
Z3_ast_vector Z3_API | Z3_algebraic_roots (Z3_context c, Z3_ast p, unsigned n, Z3_ast a[])
| Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial p(a[0], ..., a[n-1], x_n). More...
int Z3_API | Z3_algebraic_eval (Z3_context c, Z3_ast p, unsigned n, Z3_ast a[])
| Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a[0], ..., a[n-1]). More...
Z3_ast_vector Z3_API | Z3_algebraic_get_poly (Z3_context c, Z3_ast a)
| Return the coefficients of the defining polynomial. More...
unsigned Z3_API | Z3_algebraic_get_i (Z3_context c, Z3_ast a)
| Return which root of the polynomial the algebraic number represents. More...

## Function Documentation

## ◆ Z3_algebraic_add()

Z3_ast Z3_API Z3_algebraic_add | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return the value a + b.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

Postcondition
  Z3_algebraic_is_value(c, result)

## ◆ Z3_algebraic_div()

Z3_ast Z3_API Z3_algebraic_div | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return the value a / b.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)
  !Z3_algebraic_is_zero(c, b)

Postcondition
  Z3_algebraic_is_value(c, result)

## ◆ Z3_algebraic_eq()

bool Z3_API Z3_algebraic_eq | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return `true` if a == b, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

## ◆ Z3_algebraic_eval()

int Z3_API Z3_algebraic_eval | ( | Z3_context | c,
|  | Z3_ast | p,
|  | unsigned | n,
|  | Z3_ast | a[]
| ) |  |

Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a[0], ..., a[n-1]).

Precondition
  p is a Z3 expression that contains only arithmetic terms and free variables.
  forall i in [0, n) Z3_algebraic_is_value(c, a[i])

## ◆ Z3_algebraic_ge()

bool Z3_API Z3_algebraic_ge | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return `true` if a >= b, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

## ◆ Z3_algebraic_get_i()

unsigned Z3_API Z3_algebraic_get_i | ( | Z3_context | c,
|  | Z3_ast | a
| ) |  |

Return which root of the polynomial the algebraic number represents.

Precondition
  Z3_algebraic_is_value(c, a)

Referenced by expr::algebraic_i(), and AlgebraicNumRef::index().

## ◆ Z3_algebraic_get_poly()

Z3_ast_vector Z3_API Z3_algebraic_get_poly | ( | Z3_context | c,
|  | Z3_ast | a
| ) |  |

Return the coefficients of the defining polynomial.

Precondition
  Z3_algebraic_is_value(c, a)

Referenced by expr::algebraic_poly(), and AlgebraicNumRef::poly().

## ◆ Z3_algebraic_gt()

bool Z3_API Z3_algebraic_gt | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return `true` if a > b, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

## ◆ Z3_algebraic_is_neg()

bool Z3_API Z3_algebraic_is_neg | ( | Z3_context | c,
|  | Z3_ast | a
| ) |  |

Return `true` if `a` is negative, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)

## ◆ Z3_algebraic_is_pos()

bool Z3_API Z3_algebraic_is_pos | ( | Z3_context | c,
|  | Z3_ast | a
| ) |  |

Return `true` if `a` is positive, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)

## ◆ Z3_algebraic_is_value()

bool Z3_API Z3_algebraic_is_value | ( | Z3_context | c,
|  | Z3_ast | a
| ) |  |

Return `true` if `a` can be used as value in the Z3 real algebraic number package.

## ◆ Z3_algebraic_is_zero()

bool Z3_API Z3_algebraic_is_zero | ( | Z3_context | c,
|  | Z3_ast | a
| ) |  |

Return `true` if `a` is zero, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)

## ◆ Z3_algebraic_le()

bool Z3_API Z3_algebraic_le | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return `true` if a <= b, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

## ◆ Z3_algebraic_lt()

bool Z3_API Z3_algebraic_lt | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return `true` if a < b, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

## ◆ Z3_algebraic_mul()

Z3_ast Z3_API Z3_algebraic_mul | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return the value a * b.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

Postcondition
  Z3_algebraic_is_value(c, result)

## ◆ Z3_algebraic_neq()

bool Z3_API Z3_algebraic_neq | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return `true` if a != b, and `false` otherwise.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

## ◆ Z3_algebraic_power()

Z3_ast Z3_API Z3_algebraic_power | ( | Z3_context | c,
|  | Z3_ast | a,
|  | unsigned | k
| ) |  |

Return the a^k.

Precondition
  Z3_algebraic_is_value(c, a)

Postcondition
  Z3_algebraic_is_value(c, result)

## ◆ Z3_algebraic_root()

Z3_ast Z3_API Z3_algebraic_root | ( | Z3_context | c,
|  | Z3_ast | a,
|  | unsigned | k
| ) |  |

Return the a^(1/k)

Precondition
  Z3_algebraic_is_value(c, a)
  k is even => !Z3_algebraic_is_neg(c, a)

Postcondition
  Z3_algebraic_is_value(c, result)

## ◆ Z3_algebraic_roots()

Z3_ast_vector Z3_API Z3_algebraic_roots | ( | Z3_context | c,
|  | Z3_ast | p,
|  | unsigned | n,
|  | Z3_ast | a[]
| ) |  |

Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial p(a[0], ..., a[n-1], x_n).

Precondition
  p is a Z3 expression that contains only arithmetic terms and free variables.
  forall i in [0, n) Z3_algebraic_is_value(c, a[i])

Postcondition
  forall r in result Z3_algebraic_is_value(c, result)

## ◆ Z3_algebraic_sign()

int Z3_API Z3_algebraic_sign | ( | Z3_context | c,
|  | Z3_ast | a
| ) |  |

Return 1 if `a` is positive, 0 if `a` is zero, and -1 if `a` is negative.

Precondition
  Z3_algebraic_is_value(c, a)

## ◆ Z3_algebraic_sub()

Z3_ast Z3_API Z3_algebraic_sub | ( | Z3_context | c,
|  | Z3_ast | a,
|  | Z3_ast | b
| ) |  |

Return the value a - b.

Precondition
  Z3_algebraic_is_value(c, a)
  Z3_algebraic_is_value(c, b)

Postcondition
  Z3_algebraic_is_value(c, result)