Expand description
Ring Tactic: Polynomial Equality by Normalization
This module implements the ring decision procedure, which proves polynomial
equalities by converting terms to canonical polynomial form and comparing them.
§Algorithm
The ring tactic works in three steps:
- Reification: Convert Syntax terms to internal polynomial representation
- Normalization: Expand and combine like terms into canonical form
- Comparison: Check if normalized forms are structurally equal
§Supported Operations
- Addition (
add) - Subtraction (
sub) - Multiplication (
mul)
Division and modulo are not polynomial operations and are rejected.
§Canonical Form
Polynomials are stored as a map from monomials to coefficients. Monomials are maps from variable indices to exponents. BTreeMap ensures deterministic ordering for canonical comparison.
Structs§
- Monomial
- A monomial is a product of variables with their powers.
- Polynomial
- A polynomial is a sum of monomials with integer coefficients.
Enums§
- Reify
Error - Error during reification of a term to polynomial form.
Functions§
- reify
- Reify a Syntax term into a polynomial representation.