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 compare_op : op -> op -> int
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
module WithProof : sig ... end

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

module BoundWithProof : sig ... end