Module `Polynomial.LinPoly`

type t = Vect.t

module MonT : sig ... end

val linpol_of_pol : Poly.t -> t: linpol_of_pol p linearise the polynomial p

val var : var -> t

var x

returns: 1.y where y is the variable index of the monomial x^1.

val coq_poly_of_linpol : (NumCompat.Q.t -> 'a) -> t -> 'a Mc.pExpr

coq_poly_of_linpol c p

parameter p: is a multi-variate polynomial.

parameter c: maps a rational to a Coq polynomial coefficient.

returns: the coq expression corresponding to polynomial p.

val of_monomial : Monomial.t -> t: of_monomial m @returns 1.x where x is the variable (index) for monomial m

val of_vect : Vect.t -> t: of_vect v @returns a1.x1 + ... + an.xn This is not the identity because xi is the variable index of xi^1

val variables : t -> Micromega_plugin.Mutils.ISet.t

variables p

returns: the set of variables of the polynomial p interpreted as a multi-variate polynomial

val is_variable : t -> var option

is_variable p

returns: Some x if p = a.x for a >= 0

val is_linear : t -> bool

is_linear p

returns: whether the multi-variate polynomial is linear.

val is_linear_for : var -> t -> bool

is_linear_for x p

returns: true if the polynomial is linear in x i.e can be written c*x+r where c is a constant and r is independent from x

val constant : NumCompat.Q.t -> t

constant c

returns: the constant polynomial c

val search_linear : (NumCompat.Q.t -> bool) -> t -> var option

val search_all_linear : (NumCompat.Q.t -> bool) -> t -> var list

search_all_linear pred p

returns: all the variables x such p = a.x + b such that p is linear in x i.e x does not occur in b and a is a constant such that pred a

val get_bound : t -> Vect.Bound.t option

val product : t -> t -> t

product p q

returns: the product of the polynomial p*q

val factorise : var -> t -> t * t

factorise x p

returns: a,b such that p = a.x + b and x does not occur in b

val collect_square : t -> Monomial.t MonMap.t

collect_square p

returns: a mapping m such that ms = s^2 for every s^2 that is a monomial of p

val monomials : t -> Micromega_plugin.Mutils.ISet.t

monomials p

returns: the set of monomials.

val degree : t -> int

degree p

returns: return the maximum degree

val pp_var : Stdlib.out_channel -> var -> unit: pp_var o v pretty-prints a monomial indexed by v.

val pp : Stdlib.out_channel -> t -> unit: pp o p pretty-prints a polynomial.

val pp_goal : string -> Stdlib.out_channel -> (t * op) list -> unit: pp_goal typ o l pretty-prints the list of constraints as a Coq goal.