sig
  type t
  val pp :
    (Format.formatter -> int -> unit) ->
    Format.formatter -> Polynomial.Rewrite.t -> unit
  val mk_rewrite :
    (Polynomial.Monomial.t -> Polynomial.Monomial.t -> [ `Eq | `Gt | `Lt ]) ->
    Polynomial.Mvp.t list -> Polynomial.Rewrite.t
  val reduce_rewrite : Polynomial.Rewrite.t -> Polynomial.Rewrite.t
  val grobner_basis : Polynomial.Rewrite.t -> Polynomial.Rewrite.t
  val reduce : Polynomial.Rewrite.t -> Polynomial.Mvp.t -> Polynomial.Mvp.t
  val preduce :
    Polynomial.Rewrite.t ->
    Polynomial.Mvp.t -> Polynomial.Mvp.t * Polynomial.Mvp.t list
  val add_saturate :
    Polynomial.Rewrite.t -> Polynomial.Mvp.t -> Polynomial.Rewrite.t
  val generators : Polynomial.Rewrite.t -> Polynomial.Mvp.t list
end