Simplex (coq-core.Micromega

type profile_info = {

number_of_successes : int;

number_of_failures : int;

success_pivots : int;

failure_pivots : int;

average_pivots : int;

maximum_pivots : int;

}

val get_profile_info : unit -> profile_info

Simplex interface

val optimise : 
  Vect.t ->
  Polynomial.cstr list ->
  (NumCompat.Q.t option * NumCompat.Q.t option) option

val find_point : Polynomial.cstr list -> Vect.t option

val find_unsat_certificate : Polynomial.cstr list -> Vect.t option

val integer_solver : 
  (Polynomial.cstr * Polynomial.ProofFormat.prf_rule) list ->
  Polynomial.ProofFormat.proof option