Module Micromega_plugin.Polynomial
module Mc = Micromega
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
module LinPoly : sig ... end
module ProofFormat : sig ... end
module WithProof : sig ... end
module WithProof
constructs polynomials packed with the proof that their sign is correct.