module Rewrite: sig .. end
Rewrite systems for multi-variate polynomials. A polynomial rewrite system
consists of a set of polynomial rewrite rules m1 -> p1, ..., mn -> pn
where each mi is a monomial, each pi is a polynomial, and such that
mi is greater than any monomial in pi in some admissible order. An
admissible order is a total order on monomial such that for all m, n,
p, we have:
1. m <= n implies mp <= np
2. m <= mp
type
val pp : (Format.formatter -> int -> unit) ->
Format.formatter -> t -> unit
val mk_rewrite : (Polynomial.Monomial.t -> Polynomial.Monomial.t -> [ `Eq | `Gt | `Lt ]) ->
Polynomial.Mvp.t list -> t
Given an admissible order and a list of zero polynomials, orient the
polynomials into a rewrite system. This generalizes Gauss-Jordan
elimination, but (unlike Groebner basis computation) does not saturate
the rewrite system with implied equations. Thus, it can only be used as
a semi-test for membership in the ideal generated by the input
polynomials.
val reduce_rewrite : t -> t
val grobner_basis : t -> t
Saturate a polynomial rewrite system with implied equalities
val reduce : t -> Polynomial.Mvp.t -> Polynomial.Mvp.t
Reduce a multi-variate polynomial using the given rewrite rules until
no more rewrite rules apply
val preduce : t ->
Polynomial.Mvp.t -> Polynomial.Mvp.t * Polynomial.Mvp.t list
Reduce a multi-variate polynomial using the given rewrite rules until no
more rewrite rules apply. Return both the reduced polynomial and the
polynomials used during reduction.
val add_saturate : t -> Polynomial.Mvp.t -> t
Add a new zero-polynomial to a rewrite system and saturate
val generators : t -> Polynomial.Mvp.t list