module Mvp: sig
.. end
Multi-variate polynomials
include Linear.Vector
val pp : (Format.formatter -> int -> unit) -> Format.formatter -> t -> unit
val compare : t -> t -> int
val mul : t -> t -> t
val sub : t -> t -> t
val one : t
val scalar : QQ.t -> t
val of_dim : Polynomial.Monomial.dim -> t
val of_vec : ?const:int -> Linear.QQVector.t -> t
Convert a rational vector to a linear polynomial, where each dimension
corresponds to a variable except the designated const
dimension, which
is treated at a constant 1.
val split_linear : ?const:int -> t -> Linear.QQVector.t * t
Write a polynomial as a sum t + p
, where t
is a linear term and p
is a polynomial in which every monomial has degree >= 2
val vec_of : ?const:int -> t -> Linear.QQVector.t option
Convert a linear polynomial to a vector, where each dimension
corresponds to a variable except the designated const
dimension, which
is treated at a constant 1. Return None
if the polynomial is
not linear.
val term_of : 'a Syntax.context ->
(Polynomial.Monomial.dim -> 'a Syntax.term) -> t -> 'a Syntax.term
val exp : t -> int -> t
Exponentiation by a positive integer
val substitute : (Polynomial.Monomial.dim -> t) -> t -> t
Generalization of polynomial composition -- substitute each dimension
for a multivariate polynomial
val div_monomial : t -> Polynomial.Monomial.t -> t option
Divide a polynomial by a monomial
val dimensions : t -> int BatEnum.t
Enumerate the set of dimensions that appear in a polynomial