Module `Micromega_plugin.Polynomial`

module Mc = Micromega

val max_nb_cstr : int Stdlib.ref

type var = int

module Monomial : sig ... end

module MonMap : sig ... end

module Poly : sig ... end

type cstr = { coeffs : Vect.t; op : op; cst : NumCompat.Q.t; }
and op = | Eq | Ge | Gt

val eval_op : op -> NumCompat.Q.t -> NumCompat.Q.t -> bool

val opAdd : op -> op -> op

val is_strict : cstr -> bool

is_strict c

returns: whether the constraint is strict i.e. c.op = Gt

exception Strict

module LinPoly : sig ... end

module ProofFormat : sig ... end

val output_cstr : Stdlib.out_channel -> cstr -> unit
val opMult : op -> op -> op

module WithProof : sig ... end: module WithProof constructs polynomials packed with the proof that their sign is correct.