Micromega_plugin.Certificate
module Mc = Micromega
type zres = (Mc.zArithProof, int * Mc.z list) res
val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
q_cert_of_pos prf
converts a Sos proof into a rational Coq proof
val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz
z_cert_of_pos prf
converts a Sos proof into an integer Coq proof
lia depth sys
generates an unsat proof for the linear constraints in sys
.
nlia depth sys
generates an unsat proof for the non-linear constraints in sys
. The solver is incomplete -- the problem is undecidable
linear_prover_with_cert depth sys
generates an unsat proof for the linear constraints in sys
. Over the rationals, the solver is complete.