use_simplex is bound to the Coq option Simplex. If set, use the Simplex method, otherwise use Fourier

q_cert_of_pos prf converts a Sos proof into a rational Coq proof

z_cert_of_pos prf converts a Sos proof into an integer Coq proof

lia enum depth sys generates an unsat proof for the linear constraints in sys. If the Simplex option is set, any failure to find a proof should be considered as a bug.

nlia enum 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.

nlinear depth sys generates an unsat proof for the non-linear constraints in sys. The solver is incompete -- the problem is decidable.