Skip to content

feat: Add algebraic number polynomial and root-index extraction APIs #541

@toolCHAINZ

Description

@toolCHAINZ

Summary

For algebraic numbers (real roots of polynomials with rational coefficients), extract the
defining polynomial and the index of the root among the polynomial's real roots. Complements
the existing algebraic.rs which has arithmetic operations and comparisons but no way to
recover the underlying polynomial representation.

Z3 APIs

  • Z3_algebraic_get_poly — extract the minimal polynomial whose root this algebraic number is
  • Z3_algebraic_get_i — get the index of this root among the real roots of its polynomial
    (ordered from least to greatest)

Notes

  • Both APIs are only meaningful on algebraic (non-rational) values; the high-level API should
    return Option or Result for inputs that are rational
  • get_poly returns coefficients as a Vec<Real> (rational constants); the wrapper should
    expose this as a Vec<ast::Real>
  • Together these two APIs allow fully reconstructing an algebraic number from its canonical
    representation, useful for interoperability with other CAS tools

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions